CoqGym
trepplein
Our great sponsors
CoqGym | trepplein | |
---|---|---|
2 | 2 | |
370 | 26 | |
2.4% | - | |
3.6 | 0.0 | |
10 months ago | about 2 years ago | |
Coq | Scala | |
GNU Lesser General Public License v3.0 only | Apache License 2.0 |
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.
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.
trepplein
-
Automated Theorem Provers?
The default kernel used is fairly large, since it does some optimisations for interactivity. However there are 3 independent checkers for Lean's output format, https://github.com/gebner/trepplein, https://github.com/leanprover/lean/tree/master/src/checker and https://github.com/leanprover/tc . They're all fairly small, with leanchecker being less than 1000 loc.
-
Formalising Mathematics: An Introduction
Lean allows for third party type checkers. There are relatively small alternative type checkers for Lean, e.g. [1].
Lean's power lies in its elaborator that breaks down complex tactic-based proofs to a core proof language. This elaboration process can be extended with custom tactics, making it way more powerful than metamath.
[1] https://github.com/gebner/trepplein/tree/master/src/main/sca...
What are some alternatives?
lean - Lean Theorem Prover
hott3 - HoTT in Lean 3
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.
scala - Scala 2 compiler and standard library. Bugs at https://github.com/scala/bug; Scala 3 at https://github.com/scala/scala3
mathlib - Lean 3's obsolete mathematical components library: please use mathlib4
holbert - A graphical interactive proof assistant designed for education
lean-chat
Play - The Community Maintained High Velocity Web Framework For Java and Scala.
symmetric_project
Lila - ♞ lichess.org: the forever free, adless and open source chess server ♞ [Moved to: https://github.com/lichess-org/lila]
cedar-spec - Definitional implementation of Cedar language and utilities for DRT
FStar - A Proof-oriented Programming Language