Summary: morphic-symplexis is a software framework for Systems Verification of categories, Theories and Meta Theories in Lean, Rocq (formerly Coq), C# and F#. It is primarily focused on Formal Verification of Classical Mathematics and Metamathematics, but it is envisaged to also include Verification of Continuous and Hybrid Systems in the future.
Table of Contents
To download this repository, there are currently two mains options:
Clone the repository using either GitHub Desktop or the command line (terminal) :
git clone https://github.com/morphic-symplexis/morphic-symplexis.git
Download the repository as a ZIP file, as described here
You can choose whichever best suits your needs.
Note: If you do not have Git on Windows, then you can download it here.
Coming soon
This framework was implemented using Lean 4, Rocq (formerly Coq), C# and F# (via .NET Core 6.0.428). The morphic-symplexis framework is fully Open-Source, as it does not rely on any Closed-Source language, framework, library, etc.
The main components of this software framework are the following:
Any Operating System from the following list that can run .NET Core 6.0:
- All major Linux distributions (after 2016)
- macOS Catalina (version 10.15) or later
- MS Windows 10 or later
Minimum hardware requirements:
- Any CPU (no GPU necessary)
- 2GB RAM
See Acknowledgements.
See References.