All Packages
The math library of Lean 4
- Homepage
 - Repository
 - 2491
 - v4.25.0-rc2
 
A Lean companion to Analysis I
- Homepage
 - Repository
 - 1270
 - v4.20.0
 
LLMs as Copilots for Theorem Proving in Lean
- Homepage
 - Repository
 - 1178
 - v4.25.0-rc2
 
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
- Homepage
 - Repository
 - 731
 - v4.24.0
 
A collection of formalized statements of conjectures in Lean.
- Homepage
 - Repository
 - 653
 - 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
 - 439
 - 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
 - 425
 - v4.21.0
 
A project to digitalise results from physics into Lean.
- Homepage
 - Repository
 - 378
 - v4.24.0
 
The "batteries included" extended library for the Lean programming language and theorem prover
- Repository
 - 337
 - v4.25.0-rc2
 
White-box automation for Lean 4
- Repository
 - 308
 - v4.25.0-rc2
 
An introduction to theorem proving in Lean for the impatient.
- Repository
 - 281
 - v4.22.0
 
konne88/
v0.1.0functorio No description provided.
- Repository
 - 275
 - v4.20.1
 
No description provided.
- Homepage
 - Repository
 - 265
 - v4.22.0
 
Natural Number Game
- Homepage
 - Repository
 - 238
 - v4.23.0
 
Tactics for discharging Lean goals into SMT solvers.
- Repository
 - 237
 - v4.24.0
 
Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.
- Homepage
 - Repository
 - 235
 - v4.5.0
 
Lean documentation authoring tool
- Repository
 - 231
 - v4.25.0-rc2
 
Catalog Of Math Problems Formalized In Lean
- Homepage
 - Repository
 - 204
 - v4.25.0-rc2