aneris
math-comp
| aneris | math-comp | |
|---|---|---|
| 1 | 2 | |
| 34 | 630 | |
| - | 0.6% | |
| 8.4 | 9.4 | |
| 8 days ago | 4 days ago | |
| Coq | Rocq Prover | |
| MIT License | GNU General Public License v3.0 or later |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
aneris
math-comp
-
Fermat's Last Theorem – how it's going
> shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps?
This is essentially exactly what Mathlib[1] is, which is Lean's database of mathematics, and which large portions of the FLT project will likely continually contribute into.
(Other theorem provers have similar libraries, e.g. Coq's is called math-comp: https://math-comp.github.io/ )
[1]: https://github.com/leanprover-community/mathlib4/
- Which proof assistant is the best to formalize real analysis/probability/statistics?
What are some alternatives?
verdi-raft - An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
UniMath - This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
proofs - My personal repository of formally verified mathematics.
analysis - Mathematical Components compliant Analysis Library
toychain - A minimalistic blockchain consensus implemented and verified in Coq
rupicola - Gallina to Bedrock2 compilation toolkit