All Packages
The math library of Lean 4
- Homepage
- Repository
- 3678
- v4.33.0-rc1
A Lean companion to Analysis I
- Homepage
- Repository
- 1827
- v4.29.0-rc8
ulfjack/
v0.1.0ryu Converts floating point numbers to decimal strings
- Repository
- 1347
LLMs as Copilots for Theorem Proving in Lean
- Homepage
- Repository
- 1303
- v4.32.1
A collection of formalized statements of conjectures in Lean.
- Homepage
- Repository
- 1142
- v4.27.0
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
- Homepage
- Repository
- 951
- v4.32.0-rc1
A project to digitalise results from physics into Lean.
- Homepage
- Repository
- 655
- v4.31.0
leanprover/
v0.1.0cslib The Lean Computer Science Library (CSLib)
- Homepage
- Repository
- 633
- v4.33.0-rc1
The user home repository for the Mathematics in Lean tutorial.
- Repository
- 566
- v4.30.0
A project to map out the relations between different equational theories of Magmas.
- Homepage
- Repository
- 544
- v4.29.1
Lean theorem proving interface which feels like pen-and-paper proofs.
- Homepage
- Repository
- 537
- v4.29.0-rc8
Scientific computing in Lean 4
- Homepage
- Repository
- 521
- v4.15.0-rc1
The "batteries included" extended library for the Lean programming language and theorem prover
- Repository
- 409
- v4.33.0-rc1
An introduction to theorem proving in Lean for the impatient.
- Repository
- 395
- v4.27.0
White-box automation for Lean 4
- Repository
- 390
- v4.33.0-rc1
Lean documentation authoring tool
- Homepage
- Repository
- 366
- v4.33.0-rc1
Natural Number Game
- Homepage
- Repository
- 351
- v4.31.0
Blueprint for the PNT+ Project
- Homepage
- Repository
- 329
- v4.32.0
Formally Verified Arguments of Knowledge in Lean
- Homepage
- Repository
- 318
- v4.31.0
Tactics for discharging Lean goals into SMT solvers.
- Repository
- 302
- v4.32.0