LeanCopilot
set.mm
| LeanCopilot | set.mm | |
|---|---|---|
| 5 | 2 | |
| 814 | 232 | |
| 21.3% | 1.7% | |
| 9.7 | 9.9 | |
| 5 days ago | 5 days ago | |
| C++ | HTML | |
| MIT License | Creative Commons Zero v1.0 Universal |
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.
LeanCopilot
-
New Foundations is consistent – a difficult mathematical proof proved using Lean
Then it's time to update your LLM reading!
https://leandojo.org/
- LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
- LLMs as Copilots for Theorem Proving in Lean
set.mm
-
New Foundations is consistent – a difficult mathematical proof proved using Lean
Correct. The good news that Elements still works otherwise, you just need to add the missing axiom.
But many other "proofs" have been found to be false. The book "Metamath: A Computer Language for Mathematical Proofs" (by Norm Megill and yours truly) is available at: https://us.metamath.org/downloads/metamath.pdf - see section 1.2.2, "Trusting the Mathematician". We list just a few of the many examples of proofs that weren't.
Sure, there can be bugs in programs, but there are ways to counter such bugs that give FAR more confidence than can be afforded to humans. Lean's approach is to have a small kernel, and then review the kernel. Metamath is even more serious; the Metamath approach is to have an extremely small language, and then re-implement it many times (so that a bug is unlikely to be reproduced in all implementations). The most popular Metamath database is "set.mm", which uses classical logical logic and ZFC. Every change is verified by 5 different verifiers in 5 different programming languages originally developed by 5 different people:
* metamath.exe aka Cmetamath (the original C verifier by Norman Megill)
* checkmm (a C++ verifier by Eric Schmidt)
* smetamath-rs (smm3) (a Rust verifier by Stefan O'Rear)
* mmj2 (a Java verifier by Mel L. O'Cat and Mario Carneiro)
* mmverify.py (a Python verifier by Raph Levien)
For more on these verifiers, see: https://github.com/metamath/set.mm/blob/develop/verifiers.md
- Formalizing 100 Theorems
What are some alternatives?
openpose - OpenPose: Real-time multi-person keypoint detection library for body, face, hands, and foot estimation
LeanDojoChatGPT - ChatGPT plugin for theorem proving in Lean
distributed-llama - Run LLMs on weak devices or make powerful devices even more powerful by distributing the workload and dividing the RAM usage.