All Packages
The math library of Lean 4
- Homepage
- Repository
- 2951
- v4.29.0-rc2
A Lean companion to Analysis I
- Homepage
- Repository
- 1544
- v4.20.0
ulfjack/
v0.1.0ryu Converts floating point numbers to decimal strings
- Repository
- 1317
LLMs as Copilots for Theorem Proving in Lean
- Homepage
- Repository
- 1227
- v4.29.0-rc2
A collection of formalized statements of conjectures in Lean.
- Homepage
- Repository
- 839
- v4.27.0
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
- Homepage
- Repository
- 821
- v4.28.0
A project to digitalise results from physics into Lean.
- Homepage
- Repository
- 498
- v4.28.0
Lean theorem proving interface which feels like pen-and-paper proofs.
- Repository
- 491
- v4.29.0-rc2
A project to map out the relations between different equational theories of Magmas.
- Homepage
- Repository
- 483
- v4.20.1
The user home repository for the Mathematics in Lean tutorial.
- Repository
- 473
- v4.21.0
Scientific computing in Lean 4
- Homepage
- Repository
- 471
- v4.15.0-rc1
leanprover/
v0.1.0cslib The Lean Computer Science Library (CSLib)
- Homepage
- Repository
- 391
- v4.29.0-rc2
The "batteries included" extended library for the Lean programming language and theorem prover
- Repository
- 361
- v4.29.0-rc2
White-box automation for Lean 4
- Repository
- 342
- v4.29.0-rc2
An introduction to theorem proving in Lean for the impatient.
- Repository
- 337
- v4.27.0
konne88/
v0.1.0functorio No description provided.
- Repository
- 290
- v4.20.1
Natural Number Game
- Homepage
- Repository
- 289
- v4.23.0
No description provided.
- Homepage
- Repository
- 275
- v4.22.0
Blueprint for the PNT+ Project
- Homepage
- Repository
- 270
- v4.28.0
Tactics for discharging Lean goals into SMT solvers.
- Repository
- 263
- v4.27.0