CoqGym
| symmetric_project | CoqGym | |
|---|---|---|
| 1 | 2 | |
| 78 | 370 | |
| - | 0.8% | |
| 9.1 | 3.6 | |
| 6 months ago | 11 months ago | |
| Lean | Coq | |
| - | GNU Lesser General Public License v3.0 only |
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.
symmetric_project
-
Lean4 helped Terence Tao discover a small bug in his recent paper
You can even follow his progress on GitHub here:
https://github.com/teorth/symmetric_project/
CoqGym
- Lean4 helped Terence Tao discover a small bug in his recent paper
-
Discussion Thread
This has been an active area of research for a few years. See for example https://arxiv.org/abs/1905.09381. It's still immature as a field, and most results are essentially "we got basic stuff down but it hasn't gotten powerful enough to prove anything truly challenging" but it definitely exists and is being developed.
What are some alternatives?
cedar-spec - Definitional implementation of Cedar language and utilities for DRT
lean - Lean Theorem Prover
dafny - Dafny is a verification-aware programming language
coq - Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Idris2 - A purely functional programming language with first class types
trepplein - Lean type-checker written in Scala.
idris2-pack-db
mathlib - Lean 3's obsolete mathematical components library: please use mathlib4
CodeContracts - Source code for the CodeContracts tools for .NET
lean-chat
FStar - A Proof-oriented Programming Language