All Packages
- The math library of Lean 4 - Homepage
- Repository
- 2466
- v4.25.0-rc2
 
- A Lean companion to Analysis I - Homepage
- Repository
- 1256
- v4.20.0
 
- LLMs as Copilots for Theorem Proving in Lean - Homepage
- Repository
- 1172
- v4.25.0-rc2
 
- Ongoing Lean formalisation of the proof of Fermat's Last Theorem - Homepage
- Repository
- 724
- v4.24.0
 
- A collection of formalized statements of conjectures in Lean. - Homepage
- Repository
- 652
- v4.17.0
 
- Lean theorem proving interface which feels like pen-and-paper proofs. - Repository
- 462
- v4.25.0-rc2
 
- A project to map out the relations between different equational theories of Magmas. - Homepage
- Repository
- 436
- v4.20.1
 
- Scientific computing in Lean 4 - Homepage
- Repository
- 433
- v4.15.0-rc1
 
- The user home repository for the Mathematics in Lean tutorial. - Repository
- 423
- v4.21.0
 
- A project to digitalise results from physics into Lean. - Homepage
- Repository
- 371
- v4.24.0
 
- The "batteries included" extended library for the Lean programming language and theorem prover - Repository
- 336
- v4.25.0-rc2
 
- White-box automation for Lean 4 - Repository
- 307
- v4.25.0-rc2
 
- An introduction to theorem proving in Lean for the impatient. - Repository
- 279
- v4.22.0
 
- konne88/v0.1.0- functorio - No description provided. - Repository
- 272
- v4.20.1
 
- No description provided. - Homepage
- Repository
- 264
- v4.22.0
 
- Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024. - Homepage
- Repository
- 235
- v4.5.0
 
- Natural Number Game - Homepage
- Repository
- 234
- v4.23.0
 
- Tactics for discharging Lean goals into SMT solvers. - Repository
- 233
- v4.23.0
 
- Lean documentation authoring tool - Repository
- 228
- v4.25.0-rc2
 
- Catalog Of Math Problems Formalized In Lean - Homepage
- Repository
- 200
- v4.25.0-rc2