All Packages
The math library of Lean 4
- Homepage
- Repository
- 4102
- v4.34.0-rc2
A Lean companion to Analysis I
- Homepage
- Repository
- 1899
- v4.29.0-rc8
Lean certificates accompanying Navier-Stokes and Euler results
- Repository
- 1774
- v4.34.0-rc2
ulfjack/
v0.1.0ryu Converts floating point numbers to decimal strings
- Repository
- 1350
LLMs as Copilots for Theorem Proving in Lean
- Homepage
- Repository
- 1322
- v4.34.0-rc1
A collection of formalized statements of conjectures in Lean.
- Homepage
- Repository
- 1258
- v4.33.1
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
- Homepage
- Repository
- 1023
- v4.34.0-rc2
A project to digitalise results from physics into Lean.
- Homepage
- Repository
- 735
- v4.33.0
leanprover/
v0.1.0cslib The Lean Computer Science Library (CSLib)
- Homepage
- Repository
- 697
- v4.34.0-rc2
The user home repository for the Mathematics in Lean tutorial.
- Repository
- 584
- v4.30.0
A project to map out the relations between different equational theories of Magmas.
- Homepage
- Repository
- 554
- v4.29.1
Lean theorem proving interface which feels like pen-and-paper proofs.
- Homepage
- Repository
- 545
- v4.29.0-rc8
Scientific computing in Lean 4
- Homepage
- Repository
- 528
- v4.15.0-rc1
The "batteries included" extended library for the Lean programming language and theorem prover
- Repository
- 418
- v4.34.0-rc2
An introduction to theorem proving in Lean for the impatient.
- Repository
- 407
- v4.27.0
White-box automation for Lean 4
- Repository
- 403
- v4.34.0-rc2
Lean documentation authoring tool
- Homepage
- Repository
- 381
- v4.34.0-rc2
Natural Number Game
- Homepage
- Repository
- 371
- v4.31.0
Blueprint for the PNT+ Project
- Homepage
- Repository
- 343
- v4.32.2
Formally Verified Arguments of Knowledge in Lean
- Homepage
- Repository
- 334
- v4.33.1