All Packages
The math library of Lean 4
- Homepage
- Repository
- 2433
- v4.24.0-rc1
A Lean companion to Analysis I
- Homepage
- Repository
- 1224
- v4.20.0
LLMs as Copilots for Theorem Proving in Lean
- Homepage
- Repository
- 1168
- v4.24.0-rc1
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
- Homepage
- Repository
- 716
- v4.24.0-rc1
A collection of formalized statements of conjectures in Lean.
- Homepage
- Repository
- 643
- v4.17.0
Lean theorem proving interface which feels like pen-and-paper proofs.
- Repository
- 460
- v4.24.0-rc1
A project to map out the relations between different equational theories of Magmas.
- Homepage
- Repository
- 430
- v4.20.1
Scientific computing in Lean 4
- Homepage
- Repository
- 429
- v4.15.0-rc1
The user home repository for the Mathematics in Lean tutorial.
- Repository
- 419
- v4.21.0
A project to digitalise results from physics into Lean.
- Homepage
- Repository
- 363
- v4.23.0
The "batteries included" extended library for the Lean programming language and theorem prover
- Repository
- 332
- v4.24.0-rc1
White-box automation for Lean 4
- Repository
- 303
- v4.24.0-rc1
An introduction to theorem proving in Lean for the impatient.
- Repository
- 272
- v4.22.0
konne88/
v0.1.0functorio No description provided.
- Repository
- 267
- v4.20.1
No description provided.
- Homepage
- Repository
- 258
- v4.22.0
Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.
- Homepage
- Repository
- 230
- v4.5.0
Natural Number Game
- Homepage
- Repository
- 228
- v4.23.0
Tactics for discharging Lean goals into SMT solvers.
- Repository
- 228
- v4.23.0
Lean documentation authoring tool
- Repository
- 225
- v4.24.0-rc1
Catalog Of Math Problems Formalized In Lean
- Homepage
- Repository
- 199
- v4.24.0-rc1