All Packages
leanprover-community/mathlib
The math library of Lean 4
- Homepage
- Repository
- 2306
- v4.23.0-rc2
lean-dojo/LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
- Homepage
- Repository
- 1154
- v4.23.0-rc2
teorth/analysis
A Lean companion to Analysis I
- Homepage
- Repository
- 1145
- v4.20.0
ImperialCollegeLondon/FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
- Homepage
- Repository
- 661
- v4.23.0-rc2
google-deepmind/formal_conjectures
A collection of formalized statements of conjectures in Lean.
- Homepage
- Repository
- 601
- v4.17.0
Paper-Proof/paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
- Repository
- 441
- v4.23.0-rc2
lecopivo/scilean
Scientific computing in Lean 4
- Homepage
- Repository
- 425
- v4.15.0-rc1
teorth/equational_theories
A project to map out the relations between different equational theories of Magmas.
- Homepage
- Repository
- 412
- v4.20.1
leanprover-community/mil
The user home repository for the Mathematics in Lean tutorial.
- Repository
- 405
- v4.21.0
HEPLean/PhysLean
A project to digitalise results from physics into Lean.
- Homepage
- Repository
- 326
- v4.22.0
leanprover-community/batteries
The "batteries included" extended library for the Lean programming language and theorem prover
- Repository
- 325
- v4.23.0-rc2
leanprover-community/aesop
White-box automation for Lean 4
- Repository
- 294
- v4.23.0-rc2
leanprover-community/lean4-metaprogramming-book
No description provided.
- Homepage
- Repository
- 258
- v4.22.0
PatrickMassot/glimpseOfLean
An introduction to theorem proving in Lean for the impatient.
- Repository
- 240
- v4.22.0
konne88/functorio
No description provided.
- Repository
- 228
- v4.20.1
ImperialCollegeLondon/formalising-mathematics-2024
Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.
- Homepage
- Repository
- 225
- v4.5.0
ufmg-smite/smt
Tactics for discharging Lean goals into SMT solvers.
- Repository
- 217
- v4.21.0
leanprover/verso
Lean documentation authoring tool
- Repository
- 210
- v4.23.0-rc2
leanprover-community/Game
Natural Number Game
- Homepage
- Repository
- 206
- v4.22.0
dwrensha/compfiles
Catalog Of Math Problems Formalized In Lean
- Homepage
- Repository
- 191
- v4.23.0-rc2