All Packages
leanprover-community/mathlib
The math library of Lean 4
- Homepage
- Repository
- 1208
- v4.10.0-rc2
lean-dojo/LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
- Homepage
- Repository
- 864
- v4.10.0-rc2
Paper-Proof/examples
Lean theorem proving interface which feels like pen-and-paper proofs.
- Repository
- 325
- v4.10.0-rc2
lecopivo/scilean
Scientific computing in Lean 4
- Repository
- 255
- v4.9.1
leanprover-community/batteries
The "batteries included" extended library for the Lean programming language and theorem prover
- Repository
- 222
- v4.10.0-rc2
leanprover-community/lean4-metaprogramming-book
No description provided.
- Homepage
- Repository
- 204
- v4.7.0
leanprover-community/aesop
White-box automation for Lean 4
- Repository
- 160
- v4.10.0-rc2
ImperialCollegeLondon/FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
- Repository
- 153
- v4.10.0-rc2
wellecks/ntptutorial
Tutorial on neural theorem proving
- Repository
- 146
- v4.10.0-rc2
AlexKontorovich/PrimeNumberTheoremAnd
blueprint for prime number theorem and more
- Repository
- 120
- v4.8.0
teorth/PFR
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
- Homepage
- Repository
- 119
- v4.8.0
kmill/render
A simple raytracer written in Lean 4
- Repository
- 116
- v4.10.0-rc2
lurk-lab/yatima
A zero-knowledge Lean4 compiler and kernel
- Repository
- 110
- nightly-2023-01-10
wellecks/llmstep
llmstep: [L]LM proofstep suggestions in Lean 4.
- Repository
- 104
- v4.1.0
leanprover-community/proofwidgets
Helper toolkit for creating your own Lean 4 UserWidgets
- Repository
- 94
- v4.10.0-rc2
leanprover-community/Game
Natural Number Game
- Homepage
- Repository
- 89
- v4.7.0
ImperialCollegeLondon/formalising-mathematics-2024
Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.
- Homepage
- Repository
- 89
- v4.5.0
ufmg-smite/smt
Tactics for discharging Lean goals into SMT solvers.
- Repository
- 84
- v4.10.0-rc2
google-deepmind/debate
Formalizing stochastic doubly-efficient debate
- Repository
- 84
- v4.2.0-rc4
PatrickMassot/glimpseOfLean
An introduction to theorem proving in Lean for the impatient.
- Repository
- 79
- v4.10.0-rc2