All Packages
leanprover-community/mathlib
The math library of Lean 4
- Homepage
- Repository
- 1638
- v4.15.0-rc1
lean-dojo/LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
- Homepage
- Repository
- 1012
- v4.15.0-rc1
Paper-Proof/paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
- Repository
- 373
- v4.15.0-rc1
lecopivo/scilean
Scientific computing in Lean 4
- Homepage
- Repository
- 350
- v4.14.0-rc3
ImperialCollegeLondon/FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
- Repository
- 308
- v4.15.0-rc1
teorth/equational_theories
A project to map out the relations between different equational theories of Magmas.
- Homepage
- Repository
- 277
- v4.14.0-rc3
leanprover-community/batteries
The "batteries included" extended library for the Lean programming language and theorem prover
- Repository
- 263
- v4.15.0-rc1
leanprover-community/lean4-metaprogramming-book
No description provided.
- Homepage
- Repository
- 231
- v4.15.0-rc1
leanprover-community/aesop
White-box automation for Lean 4
- Repository
- 221
- v4.15.0-rc1
wellecks/ntptutorial
Tutorial on neural theorem proving
- Repository
- 163
- v4.15.0-rc1
ufmg-smite/smt
Tactics for discharging Lean goals into SMT solvers.
- Repository
- 151
- v4.15.0-rc1
teorth/PFR
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
- Homepage
- Repository
- 141
- v4.15.0-rc1
AlexKontorovich/PrimeNumberTheoremAnd
blueprint for prime number theorem and more
- Repository
- 140
- v4.15.0-rc1
ImperialCollegeLondon/formalising-mathematics-2024
Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.
- Homepage
- Repository
- 133
- v4.5.0
cmu-l3/llmlean
LLMs + Lean, on your laptop or in the cloud
- Repository
- 128
- v4.15.0-rc1
kmill/render
A simple raytracer written in Lean 4
- Repository
- 128
- v4.15.0-rc1
leanprover/verso
Lean documentation authoring tool
- Repository
- 128
- v4.15.0-rc1
argumentcomputer/yatima
A zero-knowledge Lean4 compiler and kernel
- Repository
- 126
- nightly-2023-01-10
leanprover-community/Game
Natural Number Game
- Homepage
- Repository
- 123
- v4.7.0
wellecks/llmstep
llmstep: [L]LM proofstep suggestions in Lean 4.
- Repository
- 121
- v4.1.0