diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index ccf282523a..35f47d97f5 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -9,6 +9,7 @@ projects: - Jujian Zhang source: arxiv: "2602.03716" + github_repo: axiommath/fel-polynomial status: verified main_declarations: - fels_conjecture diff --git a/candidates/README.md b/candidates/README.md index 60390106fe..5899ebaef0 100644 --- a/candidates/README.md +++ b/candidates/README.md @@ -23,511 +23,513 @@ Tracking which Lean packages we are considering for inclusion in ≥ 250 lines of `.lean` code in the local clone, and `include=true` in `decisions.jsonl` (repos with no verdict are kept regardless). The LOC column counts every `.lean` file under the clone outside - `.lake`/`.git`/`build` directories. Pass - `--min-stars=0 --min-loc=0 --decisions /dev/null` to disable all + `.lake`/`.git`/`build` directories. The In Pool column shows ✓ for + candidates already imported into lean-pool — it's joined from the + `source.github_repo` field of each project in `LeanPool/projects.yml`. + Pass `--min-stars=0 --min-loc=0 --decisions /dev/null` to disable all three filters and render the full list. Do not edit the autogenerated section by hand. -| Stars | Package | Description | License | Lean | LOC | Updated | Build | -| ---: | --- | --- | --- | --- | ---: | --- | :---: | -| 1335 | [ulfjack/ryu](https://github.com/ulfjack/ryu) | Converts floating point numbers to decimal strings | Apache-2.0 | v4.27.0-rc1 | 578 | 2026-04-29 | ✗ | -| 947 | [google-deepmind/formal_conjectures](https://github.com/google-deepmind/formal-conjectures) | A collection of formalized statements of conjectures in Lean. | Apache-2.0 | v4.27.0 | 66,093 | 2026-04-29 | ✗ | -| 874 | [ImperialCollegeLondon/FLT](https://github.com/ImperialCollegeLondon/FLT) | Ongoing Lean formalisation of the proof of Fermat's Last Theorem | Apache-2.0 | v4.30.0-rc2 | 29,512 | 2026-04-29 | ✓ | -| 555 | [leanprover-community/Physlib](https://github.com/leanprover-community/physlib) | A project to digitalise results from physics into Lean. | Apache-2.0 | v4.29.1 | 165,860 | 2026-04-29 | ✗ | -| 516 | [teorth/equational_theories](https://github.com/teorth/equational_theories) | A project to map out the relations between different equational theories of Magmas. | Apache-2.0 | v4.29.1 | 163,668 | 2026-04-29 | ✗ | -| 496 | [lecopivo/scilean](https://github.com/lecopivo/SciLean) | Scientific computing in Lean 4 | Apache-2.0 | v4.28.0-rc1 | 86,155 | 2026-04-28 | ✗ | -| 376 | [leanprover-community/batteries](https://github.com/leanprover-community/batteries) | The "batteries included" extended library for the Lean programming language and theorem prover | Apache-2.0 | v4.30.0-rc2 | 32,053 | 2026-04-29 | ✓ | -| 315 | [math-inc/strongpnt](https://github.com/math-inc/strongpnt) | | | v4.21.0 | 28,407 | 2026-05-07 | – | -| 292 | [AlexKontorovich/PrimeNumberTheoremAnd](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd) | Blueprint for the PNT+ Project | Apache-2.0 | v4.28.0 | 67,777 | 2026-04-29 | ✗ | -| 231 | [opencompl/SSA](https://github.com/opencompl/lean-mlir) | A minimal development of SSA theory | | nightly-2025-12-01 | 616,463 | 2026-04-29 | ✗ | -| 228 | [verse-lab/veil](https://github.com/verse-lab/veil) | A verifier for automated and interactive proofs about transition systems. | Apache-2.0 | v4.24.0 | 12,878 | 2026-04-23 | ✗ | -| 226 | [FormalizedFormalLogic/Foundation](https://github.com/FormalizedFormalLogic/Foundation) | Formalization of Mathematical Logic | Apache-2.0 | v4.29.0 | 100,587 | 2026-04-28 | ✗ | -| 216 | [teorth/PFR](https://github.com/teorth/pfr) | Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results) | Apache-2.0 | v4.29.0 | 21,704 | 2026-04-20 | ✗ | -| 189 | [Verified-zkEVM/Arklib](https://github.com/Verified-zkEVM/ArkLib) | Formally Verified Arguments of Knowledge in Lean | Apache-2.0 | v4.29.0 | 63,240 | 2026-04-28 | ✗ | -| 182 | [digama0/lean4lean](https://github.com/digama0/lean4lean) | Lean 4 kernel / 'external checker' written in Lean 4 | Apache-2.0 | v4.29.0 | 20,191 | 2026-04-28 | ✗ | -| 176 | [leanprover-community/iris-lean](https://github.com/leanprover-community/iris-lean) | Lean 4 port of Iris, a higher-order concurrent separation logic framework | Apache-2.0 | | 40,315 | 2026-04-29 | ✗ | -| 134 | [Verified-zkEVM/Clean](https://github.com/Verified-zkEVM/clean) | Lean circuit DSL | MIT | v4.28.0 | 36,952 | 2026-04-29 | ✗ | -| 128 | [eric-wieser/matrix_cookbook](https://github.com/eric-wieser/lean-matrix-cookbook) | The matrix cookbook, proved in the Lean theorem prover | MIT | v4.22.0-rc4 | 3,033 | 2026-04-04 | ✗ | -| 128 | [loganrjmurphy/lib](https://github.com/loganrjmurphy/LeanEuclid) | LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean. | MIT | v4.19.0 | 9,719 | 2026-04-25 | ✗ | -| 126 | [Timeroot/quantumInfo](https://github.com/Timeroot/Lean-QuantumInfo) | Quantum information theory in Lean 4 | MIT | v4.28.0 | 38,108 | 2026-04-22 | ✗ | -| 117 | [google-deepmind/debate](https://github.com/google-deepmind/debate) | Formalizing stochastic doubly-efficient debate | Apache-2.0 | v4.8.0 | 3,106 | 2026-04-09 | ✗ | -| 101 | [leanprover/lnsym](https://github.com/leanprover/LNSym) | Armv8 Native Code Symbolic Simulator in Lean | Apache-2.0 | nightly-2024-10-07 | 44,728 | 2026-04-19 | ✗ | -| 98 | [optsuite/optlib](https://github.com/optsuite/optlib) | | Apache-2.0 | v4.13.0 | 17,275 | 2026-04-28 | ✗ | -| 97 | [leanprover/sampcert](https://github.com/leanprover/SampCert) | SampCert : Verified Differential Privacy | Apache-2.0 | v4.29.0 | 18,503 | 2026-04-29 | ✗ | -| 96 | [teorth/symmetric_project](https://github.com/teorth/symmetric_project) | | | v4.2.0-rc1 | 5,317 | 2026-04-11 | – | -| 95 | [emilyriehl/InfinityCosmos](https://github.com/emilyriehl/infinity-cosmos) | A blueprint for a formalization of infinity-cosmos theory in Lean. | Apache-2.0 | v4.26.0-rc2 | 4,678 | 2026-04-25 | ✗ | -| 95 | [pandaman64/lean-regex](https://github.com/pandaman64/lean-regex) | | Apache-2.0 | | 13,621 | 2026-04-12 | ✗ | -| 91 | [Verified-zkEVM/VCVio](https://github.com/Verified-zkEVM/VCV-io) | Formalized Cryptography Proofs in Lean 4 | Apache-2.0 | v4.29.0 | 154,770 | 2026-04-29 | ✗ | -| 90 | [fpvandoorn/carleson](https://github.com/fpvandoorn/carleson) | A formalized proof of Carleson's theorem in Lean | Apache-2.0 | v4.30.0-rc2 | 45,245 | 2026-04-29 | ✗ | -| 87 | [morph-labs/lean-abc-true-almost-always](https://github.com/morph-labs/lean-abc-true-almost-always) | | | v4.20.0 | 3,602 | 2026-04-26 | – | -| 85 | [thefundamentaltheor3m/SpherePacking](https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean) | A Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8. | Apache-2.0 | v4.29.0 | 23,020 | 2026-04-29 | ✗ | -| 84 | [rzrn/GroundZero](https://github.com/rzrn/ground_zero) | Ground Zero: Lean 4 HoTT Library | Apache-2.0 | 4.28.0 | 19,200 | 2026-04-26 | ✗ | -| 83 | [leanprover-community/ConNF](https://github.com/leanprover-community/con-nf) | A formal consistency proof of Quine's set theory New Foundations | Apache-2.0 | v4.21.0-rc3 | 41,728 | 2026-04-01 | ✗ | -| 82 | [mo271/FormalBook](https://github.com/mo271/FormalBook) | Formalizing "Proofs from THE BOOK" | Apache-2.0 | v4.27.0-rc1 | 9,514 | 2026-04-08 | ✗ | -| 79 | [YuanheZ/lean-stat-learning-theory](https://github.com/YuanheZ/lean-stat-learning-theory) | [ICML2026] The first comprehensive Lean 4 formalization of statistical learning theory, featuring Gaussian Lipschitz co… | | v4.27.0-rc1 | 34,893 | 2026-05-08 | – | -| 78 | [fgdorais/Parser](https://github.com/fgdorais/lean4-parser) | Parser Combinator Library for Lean 4 | Apache-2.0 | v4.30.0-rc2 | 2,445 | 2026-04-21 | ✓ | -| 77 | [risc0/risc0-lean4](https://github.com/risc0/risc0-lean4) | A model of the RISC Zero zkVM and ecosystem in the Lean 4 Theorem Prover | Apache-2.0 | nightly-2022-12-23 | 6,497 | 2026-03-13 | ✗ | -| 76 | [teorth/estimate_tools](https://github.com/teorth/estimate_tools) | | | v4.20.0-rc5 | 3,794 | 2026-04-19 | – | -| 76 | [YaelDillies/LeanCamCombi](https://github.com/YaelDillies/cam-combi) | Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Com… | Apache-2.0 | v4.29.0 | 1,346 | 2026-04-14 | ✗ | -| 71 | [verified-optimization/CvxLean](https://github.com/verified-optimization/CvxLean) | Convex optimization modeling in Lean 4 | Apache-2.0 | v4.8.0-rc1 | 21,208 | 2026-04-28 | ✗ | -| 70 | [NethermindEth/evmyul](https://github.com/NethermindEth/EVMYulLean) | Executable formal model of the EVM and Yul in Lean 4. | Apache-2.0 | v4.22.0 | 11,339 | 2026-03-29 | ✗ | -| 68 | [starkware-libs/verification](https://github.com/starkware-libs/formal-proofs) | | Apache-2.0 | v4.13.0-rc3 | 66,896 | 2026-04-06 | ✗ | -| 67 | [sinhp/hottlean](https://github.com/sinhp/HoTTLean) | | Apache-2.0 | v4.25.0-rc2 | 39,375 | 2026-04-26 | ✗ | -| 66 | [harmonic-ai/IMO2025](https://github.com/harmonic-ai/IMO2025) | | | v4.20.0-rc5 | 5,302 | 2026-04-14 | – | -| 66 | [math-inc/Sphere-Packing-Lean](https://github.com/math-inc/Sphere-Packing-Lean) | A Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8 a… | Apache-2.0 | v4.28.0 | 180,661 | 2026-05-08 | – | -| 63 | [siddhartha-gadgil/saturn](https://github.com/siddhartha-gadgil/Saturn) | Experiments with SAT solvers with proofs in Lean 4 | MIT | v4.8.0 | 3,549 | 2025-12-19 | ✗ | -| 62 | [leanprover-community/flt-regular](https://github.com/leanprover-community/flt-regular) | Fermat's Last Theorem for regular primes | Apache-2.0 | v4.30.0-rc2 | 5,199 | 2026-04-26 | ✓ | -| 61 | [BoltonBailey/formalSnarksProject](https://github.com/BoltonBailey/formal-snarks-project) | A formal verification of Linear PCP SNARKs. | MIT | v4.10.0-rc2 | 6,219 | 2026-04-07 | ✗ | -| 60 | [Verilean/sparkle](https://github.com/Verilean/sparkle) | A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis. | Apache-2.0 | v4.28.0 | 89,950 | 2026-04-26 | ✓ | -| 59 | [vihdzp/CombinatorialGames](https://github.com/vihdzp/combinatorial-games) | Combinatorial game library in Lean 4 | Apache-2.0 | v4.30.0-rc2 | 17,744 | 2026-04-19 | ✗ | -| 53 | [joehendrix/lean-crypto](https://github.com/joehendrix/lean-crypto) | Cryptographic routines for the Lean 4 language | Apache-2.0 | nightly-2023-04-20 | 3,812 | 2026-04-14 | ✗ | -| 52 | [verse-lab/splean](https://github.com/verse-lab/splean) | Separation Logic Proofs in Lean | Apache-2.0 | v4.11.0 | 8,743 | 2026-04-06 | – | -| 49 | [reilabs/proven-zk](https://github.com/reilabs/proven-zk) | A support library for working with zero knowledge cryptography in Lean 4. | Apache-2.0 | v4.21.0 | 1,249 | 2026-03-12 | ✗ | -| 49 | [Timeroot/computableReal](https://github.com/Timeroot/ComputableReal) | computable implementation of real numbers in Lean4 | Apache-2.0 | v4.17.0-rc1 | 3,816 | 2026-04-17 | ✗ | -| 48 | [ShangtongZhang/RL-Theory](https://github.com/ShangtongZhang/rl-theory-in-lean) | Towards Formalizing RL Theory | MIT | v4.28.0-rc1 | 10,208 | 2026-04-24 | ✗ | -| 47 | [lean-dojo/problems](https://github.com/lean-dojo/LeanMillenniumPrizeProblems) | Formalization of the Millennium Problems in Lean 4 | Apache-2.0 | v4.26.0 | 5,558 | 2026-04-02 | ✗ | -| 47 | [leanprover-community/SphereEversion](https://github.com/leanprover-community/sphere-eversion) | Formalization of the existence of sphere eversions | Apache-2.0 | v4.28.0 | 14,641 | 2026-03-30 | ✗ | -| 47 | [RemyDegenne/BrownianMotion](https://github.com/RemyDegenne/brownian-motion) | Construction of a Brownian Motion in Lean | Apache-2.0 | v4.30.0-rc1 | 16,875 | 2026-04-22 | ✗ | -| 45 | [opencompl/veir](https://github.com/opencompl/veir) | Verified Intermediate Representation | | nightly-2026-05-07 | 41,325 | 2026-05-09 | – | -| 44 | [Ivan-Sergeyev/Seymour](https://github.com/Ivan-Sergeyev/seymour) | This project is about formally verifying Seymour's decomposition theorem for regular matroids. | Apache-2.0 | v4.18.0 | 9,042 | 2026-04-09 | ✗ | -| 42 | [argumentcomputer/Wasm.lean](https://github.com/argumentcomputer/Wasm.lean) | A WebAssembly implementation in Lean4 | MIT | nightly-2023-01-10 | 4,616 | 2026-04-16 | ✗ | -| 41 | [lengyijun/goldbach_tm](https://github.com/lengyijun/goldbach_tm) | Goldbach conjecture = 25-state turing machine | | v4.14.0-rc2 | 2,961 | 2026-04-25 | – | -| 41 | [riccardobrasca/FLT3](https://github.com/riccardobrasca/flt3) | Proof in Lean of Fermat Last Theorem for exponent 3 | Apache-2.0 | v4.9.0-rc3 | 914 | 2026-02-26 | ✗ | -| 40 | [AxiomMath/FelConjecture](https://github.com/AxiomMath/fel-polynomial) | Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups" | MIT | v4.26.0 | 2,710 | 2026-04-07 | ✗ | -| 39 | [leanprover/TensorLib](https://github.com/leanprover/TensorLib) | A verified tensor library in Lean | Apache-2.0 | v4.23.0 | 5,347 | 2026-04-15 | ✗ | -| 38 | [astrainfinita/algorithm](https://github.com/astrainfinita/Algorithm) | Verified efficient algorithms in Lean4. | Apache-2.0 | v4.27.0-rc1 | 5,490 | 2026-04-21 | ✗ | -| 38 | [Verified-zkEVM/CompPoly](https://github.com/Verified-zkEVM/CompPoly) | A computable model of Polynomials in Lean. | Apache-2.0 | v4.29.1 | 36,432 | 2026-04-29 | ✗ | -| 37 | [alerad/leancert](https://github.com/alerad/leancert) | Verified interval arithmetic for Lean 4 — prove bounds on exp, sin, cos, find roots, all machine-checked | Apache-2.0 | v4.28.0 | 75,256 | 2026-04-21 | – | -| 37 | [project-numina/lib](https://github.com/project-numina/LeanGeo) | Solving Competition Geometry Problems in Lean | MIT | v4.15.0 | 12,011 | 2026-04-25 | ✗ | -| 37 | [sgraf812/mpl](https://github.com/sgraf812/mpl) | A prototype for a monadic program logic in Lean that has since been upstreamed into the Lean 4 repo | Apache-2.0 | v4.21.0-rc3 #leanprover/lean4:nightly-2025-06-03 | 8,412 | 2025-10-18 | – | -| 35 | [argumentcomputer/Megaparsec.lean](https://github.com/argumentcomputer/Megaparsec.lean) | Lean 4 port of Megaparsec | MIT | v4.0.0 | 2,291 | 2026-03-08 | ✗ | -| 34 | [WuProver/groebner](https://github.com/WuProver/groebner_proj) | Formalization of Gröbner basis theory in Lean4 (WIP) | Apache-2.0 | v4.29.0-rc8 | 8,098 | 2026-04-14 | ✗ | -| 33 | [model-checking/rust-lean-models](https://github.com/model-checking/rust-lean-models) | Lean models of Rust libraries | Apache-2.0 | v4.11.0 | 6,315 | 2026-04-23 | ✗ | -| 33 | [optpku/ReasBook](https://github.com/optpku/ReasBook) | ReasBook main branch mirror for self-hosted CI | Apache-2.0 | | 275,519 | 2026-04-28 | – | -| 33 | [vihdzp/Rubik](https://github.com/vihdzp/rubik-lean4) | Lean 4 formalization of Rubik's cubes | Apache-2.0 | v4.17.0-rc1 | 3,801 | 2026-04-13 | ✗ | -| 32 | [haskell-spec/haskell-spec](https://github.com/haskell-spec/haskell-spec) | Formal specification of the Haskell Language Report | MIT | v4.22.0-rc4 | 4,076 | 2026-03-04 | ✓ | -| 32 | [JamesGallicchio/leancolls](https://github.com/JamesGallicchio/LeanColls) | WIP collections library for Lean 4 | Apache-2.0 | v4.13.0 | 3,756 | 2025-05-08 | ✗ | -| 32 | [marcusrossel/VerifiedCompiler](https://github.com/marcusrossel/verified-compiler) | A toy example of a verified compiler. | MIT | v4.29.0 | 347 | 2026-04-07 | ✓ | -| 31 | [opencompl/sail-riscv-lean](https://github.com/opencompl/sail-riscv-lean) | | | v4.29.0 | 170,174 | 2026-05-09 | – | -| 30 | [jjdishere/EG](https://github.com/jjdishere/EG) | Formalizing Euclidean Geometry in Lean | | v4.5.0-rc1 | 32,660 | 2025-12-30 | – | -| 30 | [T-Brick/wasm](https://github.com/T-Brick/lean-wasm) | Formalising the WASM spec in Lean | GPL-3.0 | v4.25.0 | 7,005 | 2026-03-18 | ✗ | -| 29 | [girving/ray](https://github.com/girving/ray) | Formalizing results about the Mandelbrot set in Lean | Apache-2.0 | v4.27.0-rc1 | 22,971 | 2026-02-17 | ✗ | -| 29 | [scottnarmstrong/DeGiorgi](https://github.com/scottnarmstrong/DeGiorgi) | Lean 4 formalization of De Giorgi-Nash-Moser theory | Apache-2.0 | v4.29.0-rc6 | 56,283 | 2026-05-06 | – | -| 28 | [GaloisInc/zkLeanEcosystem](https://github.com/GaloisInc/zkLean) | zkLean is a domain specific language (DSL) in Lean for specifying zero-knowledge statements | BSD-3-Clause | v4.25.2 | 4,048 | 2026-04-27 | ✓ | -| 28 | [sinhp/Poly](https://github.com/sinhp/Poly) | A Lean4 Formalization of Polynomial Functors | | v4.27.0-rc1 | 6,453 | 2026-04-26 | – | -| 27 | [MixedMatched/formalizing-game-theory](https://github.com/MixedMatched/formalizing-game-theory) | Example formalization of Game Theoretic concepts in Lean | | v4.17.0-rc1 | 1,304 | 2026-03-11 | – | -| 26 | [lean-machines-central/lean-machines](https://github.com/lean-machines-central/lean-machines) | a Lean4 framework for the modeling and refinement of stateful systems | Apache-2.0 | v4.23.0-rc2 | 11,277 | 2026-03-30 | ✗ | -| 26 | [merely-true/merely-true](https://github.com/merely-true/merely-true) | | Apache-2.0 | v4.29.0 | 11,252 | 2026-04-22 | – | -| 25 | [girving/interval](https://github.com/girving/interval) | Conservative floating point interval arithmetic in Lean | Apache-2.0 | v4.27.0-rc1 | 15,731 | 2026-03-25 | ✗ | -| 25 | [mortarsanjaya/IMOSLLean4](https://github.com/mortarsanjaya/IMOSLLean4) | Formalization of IMO shortlist problems in Lean 4 | Apache-2.0 | v4.30.0-rc2 | 38,524 | 2026-04-26 | ✓ | -| 24 | [opencompl/C-parsing-for-Lean4](https://github.com/opencompl/C-parsing-for-Lean4) | A parser for ANSI C, in Lean4. | | Kha/lean4:vcustom-tokens | 2,682 | 2026-04-01 | – | -| 23 | [ATOMSLab/LeanLJ](https://github.com/ATOMSLab/LeanLJ) | Lennard Jones in Lean | Apache-2.0 | v4.16.0-rc2 | 1,167 | 2026-04-29 | ✗ | -| 23 | [digama0/mm-lean4](https://github.com/digama0/mm-lean4) | Lean 4 Metamath verifier | | v4.26.0-rc2 | 1,334 | 2026-02-20 | – | -| 23 | [FormalSAT/trestle](https://github.com/FormalSAT/trestle) | | Apache-2.0 | v4.21.0 | 28,852 | 2026-03-25 | ✗ | -| 23 | [math-inc/Erdos1196](https://github.com/math-inc/Erdos1196) | | Apache-2.0 | v4.30.0-rc1 | 4,035 | 2026-05-09 | – | -| 22 | [opencompl/fp-lean](https://github.com/opencompl/fp-lean) | Floating Point Semantics Mechanization for Lean | Apache-2.0 | nightly-2026-01-14 | 17,616 | 2026-04-29 | ✗ | -| 22 | [PeterKementzey/Graph](https://github.com/PeterKementzey/graph-library-for-lean4) | | MIT | v4.12.0 | 1,606 | 2026-01-02 | ✓ | -| 22 | [VCA-EPFL/graphiti](https://github.com/VCA-EPFL/graphiti) | Verified graph rewriting (for dataflow circuits). | Apache-2.0 | v4.30.0-rc2 | 39,197 | 2026-04-29 | ✓ | -| 22 | [YaelDillies/APAP](https://github.com/YaelDillies/apap) | Formalisation of the Kelley-Meka bound on Roth numbers | Apache-2.0 | v4.30.0-rc2 | 6,953 | 2026-04-27 | ✗ | -| 21 | [frenzymath/Anderson-Conjecture](https://github.com/frenzymath/Anderson-Conjecture) | | Apache-2.0 | v4.29.0-rc8 | 19,482 | 2026-05-07 | – | -| 21 | [logical-intelligence/Putnam](https://github.com/logical-intelligence/proofs) | | MIT | v4.26.0-rc2 | 8,857 | 2026-03-17 | ✗ | -| 21 | [Luka-O/polya-enumeration-theorem](https://github.com/Luka-O/polya-enumeration-theorem) | A Lean 4 formalization of Pólya enumeration theorem. | MIT | v4.14.0-rc2 | 1,419 | 2025-09-11 | ✗ | -| 20 | [b-mehta/ABCExceptions](https://github.com/b-mehta/ABC-Exceptions) | Exceptions to the ABC conjecture in Lean | Apache-2.0 | v4.21.0-rc3 | 3,353 | 2026-04-03 | ✗ | -| 20 | [bergmannjg/Regex](https://github.com/bergmannjg/regex) | A PCRE2 compatible regular expression engine written in Lean 4. | MIT | v4.29.0 | 13,692 | 2026-04-27 | ✗ | -| 20 | [ctchou/AutomataTheory](https://github.com/ctchou/AutomataTheory) | Automata theory in Lean | Apache-2.0 | v4.24.0-rc1 | 5,258 | 2026-04-17 | ✗ | -| 20 | [JulsDE/MRiscX](https://github.com/JulsDE/MRiscX) | A certified RISC-V Interpreter with Hoare-logic in Lean | Apache-2.0 | v4.29.0 | 7,350 | 2026-04-29 | ✗ | -| 20 | [provables/sequencelib](https://github.com/provables/sequencelib) | A platform for formalizing OEIS sequences in Lean 4 | CC-BY-SA-4.0 | v4.28.0 | 857,034 | 2026-05-08 | – | -| 19 | [math-inc/KakeyaFiniteFields](https://github.com/math-inc/KakeyaFiniteFields) | A complete Lean 4 formalization of the Kakeya set problem over finite fields | | v4.26.0-rc2 | 315 | 2026-04-13 | – | -| 19 | [quangvdao/Zklib](https://github.com/quangvdao/ZKLib-deprecated) | deprecated, use Verified-zkEVM repository instead | Apache-2.0 | | | 2025-04-14 | ✗ | -| 18 | [codyroux/traat](https://github.com/codyroux/traat-lean) | Lean formalization of selected lemmas from "Term Rewriting and All That" | MIT | v4.30.0-rc1 | 3,897 | 2026-04-20 | ✓ | -| 18 | [katydid/regexderiv](https://github.com/katydid/regex-deriv-lean) | Proofs written in Lean4 for the core katydid validation algorithm | Apache-2.0 | v4.22.0 | 7,622 | 2026-02-19 | ✗ | -| 18 | [verse-lab/Lentil](https://github.com/verse-lab/Lentil) | (at least a useful portion of) Temporal Logic of Actions, a.k.a. TLA in Lean 4 | Apache-2.0 | v4.27.0 | 1,696 | 2026-04-22 | – | -| 17 | [658060/topos](https://github.com/658060/topos) | Topos theory in Lean 4 | | v4.15.0 | 1,571 | 2026-02-20 | – | -| 17 | [auto-res/FoML](https://github.com/auto-res/lean-rademacher) | Lean Formalization of Generalization Error Bound by Rademacher Complexity | MIT | v4.27.0-rc1 | 8,490 | 2026-04-28 | ✗ | -| 17 | [dwrensha/rupert](https://github.com/dwrensha/Rupert.lean) | Formalization of the Rupert Problem for convex polyhedra. | Apache-2.0 | v4.28.0 | 1,713 | 2026-04-05 | ✗ | -| 17 | [ElifUskuplu/stlc](https://github.com/ElifUskuplu/Stlc_deBruijn) | Simply Typed Lambda Calculus with de Bruijn indices | MIT | v4.16.0-rc2 | 2,806 | 2026-03-03 | ✗ | -| 17 | [kovach/etch](https://github.com/kovach/etch) | | Apache-2.0 | v4.7.0 | 11,504 | 2026-04-11 | ✗ | -| 17 | [leanprover-community/add-combi](https://github.com/leanprover-community/add-combi) | The sublibrary of Mathlib dedicated to additive combinatorics | Apache-2.0 | v4.30.0-rc2 | 1,474 | 2026-05-07 | – | -| 17 | [mrdouglasny/OSforGFF](https://github.com/mrdouglasny/OSforGFF) | A Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms | Apache-2.0 | v4.29.0 | 31,054 | 2026-04-29 | ✗ | -| 17 | [UCSCFormalMethods/LeanLTL](https://github.com/UCSCFormalMethods/LeanLTL) | A unifying framework for linear temporal logics in Lean | | v4.17.0-rc1 | 4,408 | 2026-04-12 | – | -| 17 | [Vilin97/Clawristotle](https://github.com/Vilin97/Clawristotle) | OpenClaw-style theorem proving | | v4.24.0 | 10,760 | 2026-04-28 | – | -| 16 | [leodemoura/RadixExperiment](https://github.com/leodemoura/RadixExperiment) | | | v4.29.0-rc1 | 6,330 | 2026-04-29 | – | -| 16 | [m4lvin/pdl](https://github.com/m4lvin/lean4-pdl) | Tableaux for Propositional Dynamic Logic in Lean 4 (WORK IN PROGRESS) | Apache-2.0 | v4.28.0 | 24,200 | 2026-04-29 | ✗ | -| 16 | [NethermindEth/plonky3-example](https://github.com/NethermindEth/CertiPlonk) | A framework for extracting and formally verifying constraint systems from the Plonky3 zkDSL in Lean. | Apache-2.0 | v4.23.0-rc2 | 903 | 2026-04-20 | ✗ | -| 16 | [RemyDegenne/clt](https://github.com/RemyDegenne/CLT) | Central limit theorem in Lean | Apache-2.0 | v4.29.0-rc3 | 533 | 2026-03-19 | ✗ | -| 15 | [aetilley/banach-tarski](https://github.com/aetilley/banach-tarski) | A formalization of the Banach-Tarski theorem in Lean | Apache-2.0 | v4.25.0 | 8,799 | 2026-05-01 | – | -| 15 | [apnelson1/Matroid](https://github.com/apnelson1/Matroid) | | Apache-2.0 | v4.30.0-rc2 | 123,512 | 2026-04-29 | ✗ | -| 15 | [artie2000/real-closed-field](https://github.com/artie2000/real_closed_field) | Formalisation of the theory of real closed fields in Lean 4. | Apache-2.0 | v4.30.0-rc1 | 7,956 | 2026-04-22 | ✗ | -| 15 | [frenzymath/Archon-FirstProof-Results](https://github.com/frenzymath/Archon-FirstProof-Results) | | Apache-2.0 | v4.28.0 | 11,944 | 2026-04-11 | – | -| 15 | [jsm28/AM](https://github.com/jsm28/AperiodicMonotilesLean) | Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib) | Apache-2.0 | v4.30.0-rc2 | 2,817 | 2026-04-18 | ✓ | -| 15 | [Kha/do-supplement](https://github.com/Kha/do-supplement) | Supplement of the ICFP'22 paper "‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language" | | v4.15.0 | 1,289 | 2026-05-02 | – | -| 14 | [acmepjz/Iwasawalib](https://github.com/acmepjz/lean-iwasawa) | Formalization of Iwasawa Theory in LꓱꓯN (tentative) | Apache-2.0 | v4.30.0-rc1 | 9,535 | 2026-04-29 | ✓ | -| 14 | [ammkrn/timelib](https://github.com/ammkrn/timelib) | A date and time library for Lean 4 | Apache-2.0 | v4.19.0-rc2 | 5,639 | 2026-01-30 | ✗ | -| 14 | [andrejbauer/partial-combinatory-algebras](https://github.com/andrejbauer/partial-combinatory-algebras) | A Lean 4 formalization of partial combinatory algebras. | MIT | v4.15.0-rc1 | 1,270 | 2025-06-23 | ✗ | -| 14 | [FormalizedFormalLogic/arithmetization](https://github.com/FormalizedFormalLogic/Arithmetization) | Formalization of Arithmetization of Mathematics/Metamathematics | Apache-2.0 | v4.17.0-rc1 | 18,501 | 2026-04-08 | ✗ | -| 14 | [iasakura/lean-yjs](https://github.com/iasakura/lean-yjs) | Lean-Yjs: Formal Verification of Yjs Integration Algorithm | MIT | v4.26.0-rc2 | 13,241 | 2026-04-27 | ✗ | -| 14 | [jcreedcmu/Noperthedron](https://github.com/jcreedcmu/Noperthedron) | The Noperthedron does not have Rupert Property: a proof in Lean4 | Apache-2.0 | v4.30.0-rc2 | 13,792 | 2026-04-28 | ✓ | -| 14 | [sven-manthe/borel_det](https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean) | | Apache-2.0 | v4.28.0-rc1 | 8,277 | 2026-02-26 | ✗ | -| 13 | [AviCraimer/relational-calculus-library-lean4](https://github.com/AviCraimer/relational-calculus-library-lean4) | | | v4.12.0-rc1 | 1,947 | 2026-05-04 | – | -| 13 | [eshelyaron/bdd](https://github.com/eshelyaron/lean4-bdd) | Binary Decision Diagrams in Lean 4 | Apache-2.0 | v4.27.0 | 8,155 | 2026-03-17 | ✗ | -| 13 | [facebookresearch/algebraic-combinatorics](https://github.com/facebookresearch/algebraic-combinatorics) | Automatic textbook formalization of Grinberg Algebraic Combinatorics | | v4.28.0 | 130,245 | 2026-05-05 | – | -| 13 | [girving/ray-series](https://github.com/girving/series) | Power series arithmetic in Lean | Apache-2.0 | v4.26.0-rc2 | 3,808 | 2025-12-19 | ✗ | -| 13 | [kbuzzard/ClassFieldTheory](https://github.com/kbuzzard/ClassFieldTheory) | Github repository for the 2025 Clay Summer School on Formalizing Class Field Theory | Apache-2.0 | v4.29.0 | 12,246 | 2026-04-11 | ✗ | -| 13 | [knowsys/certifyingDatalog](https://github.com/knowsys/CertifyingDatalog) | A certified checker for Datalog entailments, written in Lean | Apache-2.0 | v4.29.0 | 6,124 | 2026-04-01 | ✗ | -| 13 | [NUS-Math-Formalization/coxeter](https://github.com/NUS-Math-Formalization/coxeter) | | | v4.7.0 | 8,290 | 2025-07-28 | – | -| 13 | [RemyDegenne/testing_lower_bounds](https://github.com/RemyDegenne/testing-lower-bounds) | Information theory and hypothesis testing, in Lean | Apache-2.0 | v4.13.0-rc3 | 13,201 | 2026-04-15 | ✗ | -| 12 | [ah1112/synthetic_euclid_4](https://github.com/ah1112/synthetic_euclid_4) | | Apache-2.0 | | 2,993 | 2026-02-16 | ✗ | -| 12 | [b-mehta/AharoniKorman](https://github.com/b-mehta/AharoniKorman) | Disproof of the Aharoni–Korman conjecture | Apache-2.0 | v4.16.0-rc2 | 1,288 | 2025-12-01 | ✗ | -| 12 | [Bergschaf/banach_tarski](https://github.com/Bergschaf/banach-tarski) | | Apache-2.0 | v4.10.0-rc2 | 1,624 | 2026-01-19 | ✗ | -| 12 | [fpvandoorn/bonnAnalysis](https://github.com/fpvandoorn/BonnAnalysis) | repository for the collaborative formalization seminar in Analysis in Bonn | Apache-2.0 | v4.10.0-rc1 | 5,604 | 2026-04-01 | ✗ | -| 12 | [kim-em/KnuthClaudeLean](https://github.com/kim-em/KnuthClaudeLean) | Lean 4 formalization of Knuth's 'Claude's Cycles' paper | | v4.28.0 | 1,818 | 2026-05-07 | – | -| 12 | [math-xmum/Brouwer](https://github.com/math-xmum/Brouwer) | This repo is about the proof of the Nash Equilibrium through Scarf and Brouwer by Mathlib. | MIT | v4.22.0 | 4,790 | 2026-05-04 | – | -| 12 | [mit-plv/lean4-itree](https://github.com/mit-plv/lean4-itree) | Coinductive Interaction Trees in Lean4 using QPFs | MIT | v4.29.0 | 1,123 | 2026-05-07 | – | -| 12 | [NethermindEth/risczero-fv](https://github.com/NethermindEth/risczero-fv) | | Apache-2.0 | nightly-2023-06-10 | 49,206 | 2026-03-29 | ✗ | -| 12 | [YaelDillies/Toric](https://github.com/YaelDillies/toric) | Formalisation of toric varieties in Lean 4 | Apache-2.0 | v4.30.0-rc1 | 3,591 | 2026-04-12 | ✗ | -| 12 | [YnirPaz/PCF](https://github.com/YnirPaz/PCF-Theory) | A formalization of PCF theory in lean | MIT | v4.18.0-rc1 | 1,193 | 2026-02-24 | ✗ | -| 11 | [AfonsoBitoque/LeanServer](https://github.com/AfonsoBitoque/LeanServer) | Verified HTTPS server in Lean 4 — TLS 1.3, HTTP/2, QUIC, WebSocket, gRPC — 914 machine-checked theorems, zero sorry. Pu… | Apache-2.0 | v4.27.0 | 38,581 | 2026-04-21 | ✗ | -| 11 | [amarmaduke/lean-subst](https://github.com/amarmaduke/lean-subst) | Lean4 library for substitution inspired by autosubst | MIT | v4.29.0 | 2,279 | 2026-04-22 | ✓ | -| 11 | [AxiomMath/Deadends](https://github.com/AxiomMath/dead-ends) | | MIT | v4.26.0 | 4,260 | 2026-04-02 | ✗ | -| 11 | [AxiomMath/lattice-triangle](https://github.com/AxiomMath/lattice-triangle) | Lean formalizations for the paper "On the paucity of lattice triangles" | MIT | v4.26.0 | 9,978 | 2026-04-07 | – | -| 11 | [ecyrbe/lean-units](https://github.com/ecyrbe/lean-units) | lean physical unit system, SI international | MIT | v4.24.0 | 4,166 | 2026-01-10 | ✗ | -| 11 | [GasStationManager/ArtificialAlgorithms](https://github.com/GasStationManager/ArtificialAlgorithms) | Verified algorithms in Lean, implemented and proved by AIs | Apache-2.0 | v4.27.0 | 26,419 | 2026-04-28 | ✗ | -| 11 | [imbrem/DeBruijnSSA](https://github.com/imbrem/debruijn-ssa) | A formalization of SSA in Lean 4 | 0BSD | v4.15.0-rc1 | 29,307 | 2025-12-14 | ✗ | -| 11 | [Izzimach/pteffects](https://github.com/Izzimach/EffSpec-lean) | Effect monads with specifications (DIjkstra Monads) in Lean 4 | MIT | v4.3.0 | 1,393 | 2025-06-19 | ✗ | -| 11 | [leanprover/leanbv](https://github.com/leanprover/leanbv) | | Apache-2.0 | | | 2024-06-03 | ✗ | -| 11 | [matthunz/circuitlib](https://github.com/matthunz/circuitlib) | A digital circuit verification library for Lean4 | Apache-2.0 | v4.30.0-rc1 | 2,359 | 2026-04-27 | – | -| 11 | [NyxFoundation/TopSingleLayer](https://github.com/NyxFoundation/tsl-formal-verification) | Formal Verification of Top Single Layer Encoding | MIT | v4.24.0-rc1 | 987 | 2026-03-25 | ✗ | -| 11 | [Verified-zkEVM/EvmAsm](https://github.com/Verified-zkEVM/evm-asm) | | MIT | v4.30.0-rc1 | 172,772 | 2026-04-29 | ✓ | -| 11 | [WuProver/MonomialOrderedPolynomial](https://github.com/WuProver/MonomialOrderedPolynomial) | Monomial ordered polynomial implementation in Lean4 | Apache-2.0 | v4.29.0-rc8 | 4,816 | 2026-04-10 | ✗ | -| 11 | [Zetetic-Dhruv/formal-learning-theory-kernel](https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel) | Lean4 kernel for synthetic formalization and discovery of statistical learning theory. First and complete formalization… | | v4.29.0-rc6 | 23,679 | 2026-04-29 | – | -| 11 | [znssong/SetTheory](https://github.com/znssong/SetTheory) | A formalization project of set theory and elementary embeddings in Lean 4. Includes a proof of Kunen's inconsistency th… | Apache-2.0 | v4.29.0-rc4 | 2,859 | 2026-04-20 | – | -| 10 | [Beneficial-AI-Foundation/Curve25519Dalek](https://github.com/Beneficial-AI-Foundation/curve25519-dalek-lean-verify) | Verifying curve25519-dalek using Lean | Apache-2.0 | v4.28.0-rc1 | 50,007 | 2026-04-29 | ✗ | -| 10 | [Brunn-Minkowski-in-Lean/BrunnMinkowski](https://github.com/Brunn-Minkowski-in-Lean/BrunnMinkowski) | | | v4.19.0-rc2 | 1,731 | 2026-02-11 | – | -| 10 | [calcu16/lean_complexity](https://github.com/calcu16/lean_complexity) | Complexity analysis in Lean | | v4.5.0-rc1 | 5,595 | 2025-02-04 | – | -| 10 | [DavePearce/LeanEVM](https://github.com/DavePearce/LeanEVM) | A toy implementation of the EVM in Lean4. | Apache-2.0 | v4.8.0-rc2 | 818 | 2024-05-29 | ✗ | -| 10 | [gdncc/cryptography](https://github.com/gdncc/Cryptography) | Lean 4 programming language and theorem prover cryptography experiments | MIT | v4.27.0 | 1,300 | 2026-02-13 | ✓ | -| 10 | [ianjauslin-rutgers/pythagoras4](https://github.com/ianjauslin-rutgers/pythagoras4) | Many proofs of the Pythagoras theorem - Lean 4 | | nightly-2023-05-16 | 2,118 | 2026-01-09 | – | -| 10 | [katydid/sadol](https://github.com/katydid/regex-deriv-reproving-agda-in-lean) | Symbolic and Automatic Differentiation of Languages in Lean | Apache-2.0 | v4.14.0 | 1,231 | 2025-05-09 | ✓ | -| 10 | [kebekus/VD](https://github.com/kebekus/ProjectVD) | Formalizing Value Distribution Theory | Apache-2.0 | v4.30.0-rc2 | 1,885 | 2026-04-29 | ✓ | -| 10 | [knowsys/FormaleSystemeInLean](https://github.com/knowsys/Formale-Systeme-in-LEAN) | LEAN4 formalization of the undergraduate lecture "Formale Systeme" at TU Dresden (WIP) | Apache-2.0 | v4.28.0 | 8,973 | 2026-03-26 | ✗ | -| 10 | [leanprover/LeroyCompilerVerificationCourse](https://github.com/leanprover/LeroyCompilerVerificationCourse) | | LGPL-2.1 | v4.23.0-rc2 | 3,189 | 2025-11-06 | ✗ | -| 10 | [NethermindEth/CompPoly](https://github.com/NethermindEth/CompPoly) | | Apache-2.0 | v4.22.0-rc2 | 1,296 | 2026-04-20 | ✗ | -| 10 | [NethermindEth/FVIntmax](https://github.com/NethermindEth/FVIntmax) | Formal verification of the Intmax protocol in Lean. | Apache-2.0 | v4.14.0-rc2 | 5,301 | 2026-03-17 | ✗ | -| 10 | [RemyDegenne/kolmogorov_extension4](https://github.com/RemyDegenne/kolmogorov_extension4) | Lean formalization of the Kolmogorov extension theorem | Apache-2.0 | v4.30.0-rc1 | 635 | 2026-04-08 | ✓ | -| 10 | [ruplet/formalization-of-bounded-arithmetic](https://github.com/ruplet/formalization-of-bounded-arithmetic) | | MIT | v4.22.0 | 6,612 | 2026-04-10 | – | -| 10 | [teorth/asymptotic](https://github.com/teorth/asymptotic) | | | v4.5.0-rc1 | 1,469 | 2026-03-15 | – | -| 10 | [urkud/DeRhamCohomology](https://github.com/urkud/DeRhamCohomology) | Formalization of de Rham cohomologies of a smooth manifold | | v4.21.0-rc2 | 2,159 | 2026-05-09 | – | -| 10 | [YaelDillies/AddCombi](https://github.com/YaelDillies/add-combi) | The (currently unofficial) sublibrary of Mathlib dedicated to additive combinatorics | Apache-2.0 | v4.30.0-rc2 | 1,474 | 2026-04-29 | ✗ | -| 10 | [YaelDillies/gibbs-measure](https://github.com/YaelDillies/gibbs-measure) | ASCI Summer Research Lean | Apache-2.0 | v4.29.0 | 1,298 | 2026-04-05 | – | -| 10 | [YellPika/quasi-borel-spaces](https://github.com/YellPika/quasi-borel-spaces) | A formalization of Quasi-Borel Spaces in Lean 4 | MIT | v4.28.0-rc1 | 8,626 | 2026-04-10 | ✗ | -| 9 | [ahhwuhu/Zeta3Irrational](https://github.com/ahhwuhu/zeta_3_irrational) | | Apache-2.0 | v4.18.0 | 4,157 | 2026-03-20 | ✗ | -| 9 | [AxiomMath/ramanujan-tau-misses-primes](https://github.com/AxiomMath/ramanujan-tau-misses-primes) | Lean formalizations for the paper "ABC implies that Ramanujan's Tau function misses almost all primes" | MIT | v4.26.0 | 5,772 | 2026-04-23 | – | -| 9 | [b-mehta/PrimeCert](https://github.com/b-mehta/PrimeCert) | Formal prime certificates in Lean 4 | MIT | v4.29.1 | 1,949 | 2026-04-29 | – | -| 9 | [Beneficial-AI-Foundation/FloatSpec](https://github.com/Beneficial-AI-Foundation/FloatSpec) | Formally Verified Float Implementation with lean4 | Apache-2.0 | v4.29.0 | 70,827 | 2026-04-24 | ✗ | -| 9 | [cameronfreer/exchangeability](https://github.com/cameronfreer/exchangeability) | Formalization of exchangeability and three proofs of de Finetti's theorem in Lean 4, following Probabilistic Symmetries… | Apache-2.0 | v4.27.0-rc1 | 43,823 | 2026-04-19 | ✗ | -| 9 | [goens/lost-pop-lean](https://github.com/goens/lost-pop-lean) | POP Memory Model in Lean | MIT | v4.30.0-rc2 | 5,784 | 2026-04-20 | ✓ | -| 9 | [Hagb/lean-groebner](https://github.com/Hagb/lean-groebner) | Lean4 formalization of Gröbner basis (WIP) | Apache-2.0 | nightly-2023-06-10 | 2,497 | 2025-07-28 | ✗ | -| 9 | [jthulhu/2ltt](https://github.com/jthulhu/2ltt) | | | v4.10.0-rc1 | 6,746 | 2026-05-01 | – | -| 9 | [LeanMachineLearning/LeanMachineLearning](https://github.com/LeanMachineLearning/LML) | The Lean Machine Learning Library | Apache-2.0 | v4.29.0 | 10,125 | 2026-04-27 | ✗ | -| 9 | [LieLean/Lie](https://github.com/LieLean/LowDimSolvClassification) | A classification theorem in Lean of solvable Lie algebras of dimension zero to three | Apache-2.0 | v4.19.0 | 5,595 | 2025-10-09 | ✗ | -| 9 | [madvorak/chomsky](https://github.com/madvorak/chomsky) | Port https://github.com/madvorak/grammars/ to Lean 4 | BSD-2-Clause | v4.18.0 | 5,760 | 2026-04-09 | ✗ | -| 9 | [madvorak/duality](https://github.com/madvorak/duality) | Duality theory in linear optimization and its extensions | Apache-2.0 | v4.18.0 | 2,582 | 2026-02-26 | ✗ | -| 9 | [madvorak/vcsp](https://github.com/madvorak/vcsp) | General-Valued Constraint Satisfaction Problems | Apache-2.0 | v4.18.0 | 1,050 | 2026-02-26 | ✗ | -| 9 | [MichaelStollBayreuth/EulerProducts](https://github.com/MichaelStollBayreuth/EulerProducts) | An attempt at formalizing facts on Euler products in Lean | GPL-2.0 | v4.24.0 | 472 | 2026-04-10 | ✗ | -| 9 | [oliver-butterley/SpectralThm](https://github.com/oliver-butterley/SpectralThm) | Ongoing project to formalise The Spectral Theorem in Lean prover | Apache-2.0 | v4.30.0-rc2 | 1,524 | 2026-04-16 | ✗ | -| 9 | [or4nge19/NeuralNetworks](https://github.com/or4nge19/NeuralNetworks) | Formalization of Neural Networks in Lean 4 | Apache-2.0 | v4.24.0-rc1 | 31,666 | 2026-02-12 | ✗ | -| 9 | [powdr-labs/leanr](https://github.com/powdr-labs/leanr) | | MIT | v4.30.0-rc1 | 3,810 | 2026-04-09 | ✓ | -| 9 | [SamuelSchlesinger/shannon-entropy](https://github.com/SamuelSchlesinger/shannon-1948-formalization) | A formalization of Shannon's seminal 1948 paper defining entropy. | MIT | v4.28.0 | 1,912 | 2026-04-11 | ✗ | -| 9 | [seewoo5/lean-poly-abc](https://github.com/seewoo5/lean-poly-abc) | Formalization of the proof of ABC conjecture for polynomials (Mason-Stothers theorem) in Lean 4 | | v4.9.0-rc2 | 1,290 | 2026-03-04 | – | -| 9 | [smorel394/TS1](https://github.com/smorel394/TS1) | | | nightly-2023-07-12 | 12,727 | 2023-09-01 | – | -| 9 | [staroperator/mathematical-logic-in-lean](https://github.com/staroperator/mathematical-logic-in-lean) | Mathematical Logic in Lean | | v4.23.0-rc2 | 13,956 | 2026-03-22 | – | -| 9 | [tannerduve/computability](https://github.com/tannerduve/computability) | A Lean formalization of the theory of oracle computability and Turing degrees via partial recursive functions | | v4.24.0 | 3,035 | 2026-02-05 | – | -| 8 | [alainchmt/RingOfIntegersProject](https://github.com/alainchmt/RingOfIntegersProject) | Certifying rings of integers in number fields with Lean | Apache-2.0 | v4.14.0-rc2 | 93,799 | 2026-03-20 | – | -| 8 | [chrisflav/proetale](https://github.com/chrisflav/proetale) | Proétale cohomology in Lean | Apache-2.0 | v4.30.0-rc2 | 10,400 | 2026-04-28 | ✓ | -| 8 | [Clap-lang/clap](https://github.com/Clap-lang/clap-lean) | Implementation of the Clap language for ZK Circuits in the Lean proof-assistant | Apache-2.0 | v4.29.0 | 59,183 | 2026-04-29 | ✗ | -| 8 | [FormalizedFormalLogic/incompleteness](https://github.com/FormalizedFormalLogic/Incompleteness) | Formalize Incompleness Theorem Related Results | Apache-2.0 | v4.16.0-rc2 | 2,514 | 2025-09-23 | ✗ | -| 8 | [FredRaj3/SemicircleLaw](https://github.com/FredRaj3/SemicircleLaw) | Formalization of Wigner's Semicircle Law in Lean | MIT | v4.24.0 | 3,174 | 2026-04-11 | ✗ | -| 8 | [GasStationManager/ArtificialTheorems](https://github.com/GasStationManager/ArtificialTheorems) | AI-assisted formalizations of machine learning theory | | v4.27.0 | 12,858 | 2026-04-30 | – | -| 8 | [joelriou/topcat-model-category](https://github.com/joelriou/topcat-model-category) | | | v4.25.0-rc2 | 42,295 | 2026-04-18 | – | -| 8 | [jonhanke/quadratic_forms_in_lean](https://github.com/jonhanke/quadratic_forms_in_lean) | | | v4.19.0-rc3 | 2,113 | 2025-09-07 | – | -| 8 | [josephmckinsey/flean](https://github.com/josephmckinsey/Flean) | Floating point numbers in lean. A replacement of Mathlib.Data.FP | Apache-2.0 | v4.27.0-rc1 | 2,587 | 2026-04-07 | ✗ | -| 8 | [lecopivo/leanblas](https://github.com/lecopivo/LeanBLAS) | Bindings and specification for BLAS | Apache-2.0 | v4.28.0-rc1 | 2,674 | 2026-02-12 | ✗ | -| 8 | [math-xmum/GameTheory](https://github.com/math-xmum/gametheory) | | Apache-2.0 | v4.24.0-rc1 | 11,547 | 2026-04-20 | ✗ | -| 8 | [Mathias-Stout/Many-sorted-model-theory](https://github.com/Mathias-Stout/Many-sorted-model-theory) | A lean repository for building many-sorted logic, with a view towards model theory of valued fields | Apache-2.0 | v4.30.0-rc2 | 24,442 | 2026-04-20 | – | -| 8 | [mtoohey31/tabular-types](https://github.com/mtoohey31/tabular-types) | Proofs for Extensible Data Types with Ad-Hoc Polymorphism | Apache-2.0 | v4.17.0 | 24,678 | 2026-01-13 | ✗ | -| 8 | [siddhartha-gadgil/Polylean](https://github.com/siddhartha-gadgil/Polylean) | | Apache-2.0 | v4.19.0-rc3 | 5,102 | 2025-06-02 | ✗ | -| 8 | [sivukhin/sqlite3-lean-proofs](https://github.com/sivukhin/sqlite3-lean-proofs) | | | v4.25.0 | 16,191 | 2026-04-25 | – | -| 8 | [Timeroot/CircuitComp](https://github.com/Timeroot/CircuitComp) | Circuit complexity in Lean | | v4.28.0 | 9,668 | 2026-04-23 | – | -| 8 | [vasnesterov/HadwigerNelson](https://github.com/vasnesterov/HadwigerNelson) | Hadwiger-Nelson Problem Formalization in Lean 4 | Apache-2.0 | nightly-2024-07-11 | 814 | 2024-12-09 | ✗ | -| 8 | [vihdzp/ordinal-notation](https://github.com/vihdzp/ordinal-notation) | Ordinal notations in Lean | | v4.16.0-rc2 | 6,161 | 2025-07-20 | – | -| 8 | [z-tech/sumcheck-lean4](https://github.com/z-tech/sumcheck-lean4) | | Apache-2.0 | v4.28.0 | 6,219 | 2026-05-05 | – | -| 7 | [adamtopaz/CopenhagenMasterclass2023](https://github.com/adamtopaz/CopenhagenMasterclass2023) | | | nightly-2023-06-10 | 5,349 | 2025-05-17 | – | -| 7 | [bkase/VerifiedGPU](https://github.com/bkase/verified-gpu) | | MIT | v4.25.0-rc2 | 3,755 | 2025-12-25 | ✓ | -| 7 | [CBirkbeck/LeanBridge](https://github.com/CBirkbeck/LeanBridge) | Link LMFDB and Lean | Apache-2.0 | v4.23.0 | 3,272 | 2026-03-23 | – | -| 7 | [fplaunchpad/sal](https://github.com/fplaunchpad/sal) | Multimodal verification of Replicated Data Types in Lean | MIT | v4.28.0 | 24,962 | 2026-04-29 | ✗ | -| 7 | [hanwenzhu/MillerRabin](https://github.com/hanwenzhu/miller-rabin) | Miller–Rabin primality test in Lean | Apache-2.0 | v4.22.0 | 1,289 | 2026-04-27 | ✗ | -| 7 | [haskell-spec/veriflex](https://github.com/haskell-spec/veriflex) | Verified lexer for Lean 4 | MIT | v4.21.0 | 1,226 | 2026-01-24 | – | -| 7 | [hawkrobe/linglib](https://github.com/hawkrobe/linglib) | A Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formali… | Apache-2.0 | v4.30.0-rc2 | 873,929 | 2026-04-29 | ✗ | -| 7 | [ISTA-PLV/Coinductive](https://github.com/ISTA-PLV/coinductive) | Co-inductive datatypes for Lean | BSD-3-Clause | v4.29.0 | 3,905 | 2026-04-29 | ✓ | -| 7 | [katjabercic/Lean-HoG](https://github.com/katjabercic/Lean-HoG) | | BSD-2-Clause | v4.6.0 | 4,793 | 2025-12-04 | – | -| 7 | [KunhongDu/HoTT-Model](https://github.com/KunhongDu/HoTT-Model) | | | v4.14.0-rc2 | 22,601 | 2026-02-12 | – | -| 7 | [kyoDralliam/model-theory-topos](https://github.com/kyoDralliam/model-theory-topos) | First order model theory inside a topos in Lean | | v4.22.0-rc3 | 9,409 | 2026-01-29 | – | -| 7 | [mkaratarakis/HopfieldNet](https://github.com/mkaratarakis/HopfieldNet) | | MIT | v4.27.0-rc1 | 149,180 | 2026-02-10 | ✗ | -| 7 | [mseri/BET](https://github.com/mseri/BET) | Project for "Machine-Checked Mathematics" at the Lorentz Center | Apache-2.0 | v4.30.0-rc2 | 5,086 | 2026-04-28 | ✓ | -| 7 | [objectionary/phi-calculus](https://github.com/objectionary/proof) | Proof of 𝜑-calculus confluence | MIT | v4.15.0-rc1 | 6,543 | 2026-04-29 | ✗ | -| 7 | [Paul-Lez/Stacks-project](https://github.com/Paul-Lez/Stacks-project) | Formalizing Fibered Categories and Stacks in Lean | | v4.24.0-rc1 | 6,119 | 2025-12-30 | – | -| 7 | [Rob23oba/lean4-no-axioms](https://github.com/Rob23oba/lean4-no-axioms) | Lean 4 without any axioms | | v4.27.0 | 7,738 | 2026-03-09 | – | -| 7 | [scholzhannah/CWComplexes](https://github.com/scholzhannah/CWComplexes) | In this repository I am collecting the code of my formalisation of CW complexes in Lean. | | v4.30.0-rc1 | 7,012 | 2026-04-17 | – | -| 7 | [T-Brick/controlflow](https://github.com/T-Brick/ControlFlow) | A control flow graph library for Lean | GPL-3.0 | v4.25.0 | 5,329 | 2025-11-17 | ✓ | -| 7 | [taeyool/lean-flag-algebras](https://github.com/taeyool/lean-flag-algebras) | | | v4.27.0 | 30,605 | 2026-05-09 | – | -| 7 | [Timeroot/lean-descartes-signs](https://github.com/Timeroot/lean-descartes-signs) | Lean 4 proof of Descartes' Rule of Signs | | v4.3.0-rc2 | 1,475 | 2025-09-04 | – | -| 7 | [weiran-sun/PDE](https://github.com/weiran-sun/pde) | PDE Lean formalization | Apache-2.0 | v4.27.0 | 3,335 | 2026-04-29 | ✗ | -| 7 | [Whysoserioushah/BrauerGroup_new](https://github.com/Whysoserioushah/BrauerGroup_new) | | Apache-2.0 | v4.26.0-rc2 | 14,855 | 2026-03-20 | – | -| 6 | [anoma/juvix-lean](https://github.com/anoma/juvix-lean) | Juvix Lean library for compiler run verification | MIT | v4.19.0-rc2 | 3,505 | 2025-11-04 | ✗ | -| 6 | [Antoine-dSG/frieze_patterns](https://github.com/Antoine-dSG/frieze_patterns) | A project to formalise Coxeter's frieze patterns | | v4.10.0-rc2 | 1,440 | 2025-03-18 | – | -| 6 | [bergmannjg/time](https://github.com/bergmannjg/time) | Port of the haskell time library to Lean 4 and verification of date calculations | MIT | v4.20.0 | 5,647 | 2025-06-10 | ✗ | -| 6 | [chrisflav/bruhat-tits](https://github.com/chrisflav/bruhat-tits) | A formalisation of the Bruhat-Tits tree in Lean4 | Apache-2.0 | v4.19.0 | 8,284 | 2026-02-17 | ✗ | -| 6 | [girving/render](https://github.com/girving/ray-render) | Verified renders of the Mandelbrot set | Apache-2.0 | v4.27.0-rc1 | 2,941 | 2025-12-31 | ✗ | -| 6 | [kkytola/VirasoroProject](https://github.com/kkytola/VirasoroProject) | Lean project on the Virasoro algebra (2-cohomology of the Witt algebra, definition of the Virasoro algebra, ...) | Apache-2.0 | v4.27.0-rc1 | 6,026 | 2026-04-05 | ✗ | -| 6 | [Koukyosyumei/runwai_project](https://github.com/Koukyosyumei/Runwai) | COMS 6998 (Fall 2025): Refinement-typed DSL for certified AIR constraints and lookups | Apache-2.0 | v4.24.0 | 5,873 | 2026-03-26 | ✓ | -| 6 | [mariainesdff/LocalClassFieldTheory](https://github.com/mariainesdff/LocalClassFieldTheory) | Formalization of local fields, and eventually LCFT | | v4.22.0-rc2 | 14,717 | 2026-03-10 | – | -| 6 | [mbkybky/module_localProperties](https://github.com/mbkybky/module_localProperties) | Formalizing local properties of modules in LEAN | | v4.30.0-rc2 | 2,148 | 2026-05-08 | – | -| 6 | [MichaelStollBayreuth/Weights](https://github.com/MichaelStollBayreuth/Weights) | Formalization in Lean4 of some results in "Minimization of hypersurfaces" by A.-S. Elsenhans and myself | GPL-2.0 | v4.24.0 | 1,845 | 2026-04-10 | ✗ | -| 6 | [Paul-Lez/PersistentDecomp](https://github.com/Paul-Lez/PersistentDecomp) | Formalizing the Structure Theorem for Persistence Modules | Apache-2.0 | v4.29.0 | 1,607 | 2026-04-08 | ✗ | -| 6 | [ro-gut/turan3](https://github.com/ro-gut/turan3) | Formalisation of (the 3rd) Turan's Theorem Proof from The Book (6th Edition) | | v4.24.0-rc1 | 2,836 | 2025-09-24 | – | -| 6 | [septract/denyguarantee-v3](https://github.com/septract/denyguarantee-v3) | | | v4.21.0 | 3,116 | 2026-01-11 | – | -| 6 | [Shreyas4991/DGAlgorithms](https://github.com/Shreyas4991/DGAlgorithms) | Distributed Graph Algorithms in Lean | Apache-2.0 | v4.28.0 | 3,658 | 2026-03-10 | ✗ | -| 6 | [ToposInstitute/lean-poly](https://github.com/ToposInstitute/lean-poly) | | | v4.3.0-rc1 | 797 | 2024-12-04 | – | -| 6 | [urkud/SardMoreira](https://github.com/urkud/SardMoreira) | Formalization of Moreira's version of Sard's Theorem | Apache-2.0 | v4.27.0-rc1 | 4,869 | 2025-12-27 | ✗ | -| 5 | [AdrienChampion/collChoSoWel](https://github.com/AdrienChampion/collChoSoWel) | | Apache-2.0 | nightly-2023-09-02 | 7,379 | 2026-01-31 | ✗ | -| 5 | [AlexeyMilovanov/kolmogorov-complexity-lean](https://github.com/AlexeyMilovanov/kolmogorov-complexity-lean) | Formalization of Algorithmic Information Theory in Lean 4 | | v4.29.0-rc8 | 2,046 | 2026-04-07 | – | -| 5 | [alexoltean61/hybrid_logic_lean](https://github.com/alexoltean61/hybrid_logic_lean) | | | nightly-2023-06-10 | 5,287 | 2025-09-18 | – | -| 5 | [alja123/hyperstabilityES](https://github.com/alja123/hyperstabilityES) | | | v4.8.0-rc1 | 35,993 | 2024-12-17 | – | -| 5 | [AntoineChambert-Loir/DividedPowers4](https://github.com/AntoineChambert-Loir/DividedPowers4) | DividedPowers in Lean / Mathlib 4 | | v4.30.0-rc1 | 70,762 | 2026-04-10 | – | -| 5 | [atlas-computing-org/bignum](https://github.com/atlas-computing-org/bignum) | port of s2n-bignum to Lean | Apache-2.0 | v4.30.0-rc2 | 4,637 | 2026-04-23 | ✓ | -| 5 | [ATOMSLab/DimensionalAnalysis](https://github.com/ATOMSLab/LeanDimensionalAnalysis) | Formally-verified dimensional analysis in Lean | Apache-2.0 | v4.23.0-rc2 | 1,052 | 2025-10-15 | ✗ | -| 5 | [BasisResearch/VerifiedJS](https://github.com/BasisResearch/VerifiedJS) | A vibe-slopped verified compiler maybe? | | v4.29.0-rc6 | 102,423 | 2026-04-19 | – | -| 5 | [dagurtomas/LeanCondensed](https://github.com/dagurtomas/LeanCondensed) | | Apache-2.0 | v4.28.0-rc1 | 1,876 | 2026-03-20 | ✗ | -| 5 | [Danelnov/Lambda-Calculus-Formalization](https://github.com/Danelnov/Lambda-Calculus-Formalization) | This formalization uses the De Bruijn indices, the objective is to formalize the Church-Rosser theorem | | v4.26.0-rc2 | 675 | 2026-01-29 | – | -| 5 | [dhyan-aranha/Monsky](https://github.com/dhyan-aranha/Monsky) | This is a repository on the formalization of Monsky's theorem by the UvA lean community. | Apache-2.0 | v4.16.0-rc2 | 8,137 | 2025-10-30 | – | -| 5 | [DhyeyMavani2003/chip-firing-with-lean](https://github.com/DhyeyMavani2003/chip-firing-with-lean) | A formalization of chip-firing games and the Riemann-Roch theorem for graphs using the Lean 4 theorem prover. | Apache-2.0 | v4.29.0 | 5,732 | 2026-04-03 | ✗ | -| 5 | [elazarg/GameTheory](https://github.com/elazarg/GameTheory) | | MIT | v4.29.0 | 51,502 | 2026-05-07 | – | -| 5 | [girving/aks](https://github.com/girving/aks) | Seiferas's simplified construction of the AKS O(log n) depth sorting network, formalised in Lean | Apache-2.0 | v4.29.0-rc4 | 36,974 | 2026-03-19 | – | -| 5 | [girving/bottcher](https://github.com/girving/bottcher) | Verified computation of the Mandelbrot set Böttcher series | Apache-2.0 | v4.26.0-rc2 | 373 | 2025-12-19 | ✗ | -| 5 | [lf-lang/reactor-model](https://github.com/lf-lang/reactor-model) | A Lean-based formalization of the Reactor model. | Apache-2.0 | v4.24.0-rc1 | 4,174 | 2025-10-08 | ✗ | -| 5 | [markusdemedeiros/Eileen](https://github.com/markusdemedeiros/Eileen) | Reimplementing some data structures from Iris in Lean | | v4.17.0-rc1 | 4,333 | 2025-09-09 | – | -| 5 | [MichaelStollBayreuth/Heights](https://github.com/MichaelStollBayreuth/Heights) | An attempt at formalizing the theory of heights in Lean | GPL-2.0 | v4.30.0-rc2 | 6,086 | 2026-04-28 | ✓ | -| 5 | [monsterkrampe/ExistentialRules](https://github.com/monsterkrampe/Existential-Rules-in-Lean) | This repo contains formalizations around Existential Rules (aka. Tuple-Generating Dependencies) with disjunctions and t… | Apache-2.0 | v4.29.0 | 17,493 | 2026-04-23 | ✗ | -| 5 | [or4nge19/MCMC](https://github.com/or4nge19/MCMC) | Formalization of Markov Chain Monte Carlo in Lean 4 | Apache-2.0 | v4.29.0 | 12,563 | 2026-04-29 | ✗ | -| 5 | [Parcly-Taxel/Redhill](https://github.com/Parcly-Taxel/Redhill) | A formalisation of the disproof of Ramaekers's conjecture | MIT | v4.30.0-rc2 | 3,455 | 2026-05-05 | – | -| 5 | [paulcadman/lean-effects](https://github.com/paulcadman/lean-effects) | | Apache-2.0 | v4.29.0 | 1,694 | 2026-04-04 | ✓ | -| 5 | [PierreSenellart/provenance](https://github.com/PierreSenellart/provenance-lean) | Lean4 formalization of some provenance notions | MIT | v4.26.0-rc2 | 7,675 | 2026-04-16 | ✗ | -| 5 | [RichardZandi/kleene2](https://github.com/RichardZandi/kleene2) | A lightweight Lean 4 library that formalizes the generalized Kleene Second Recursion Theorem and provides a reusable di… | | v4.20.0 | 387 | 2025-06-26 | – | -| 5 | [Rob23oba/dependent-computability](https://github.com/Rob23oba/dependent-computability) | Automatically proving computability for Lean functions | | leanprover/lean4-pr-releases:pr-release-8867-9a8a69e | 11,286 | 2026-05-06 | – | -| 5 | [SamuelSchlesinger/sensitivity](https://github.com/SamuelSchlesinger/sensitivity-conjecture) | Lean 4 formalization of the Sensitivity Conjecture (Huang 2019) | Apache-2.0 | v4.28.0 | 971 | 2026-03-03 | ✗ | -| 5 | [sinhp/leanFibredCategories](https://github.com/sinhp/LeanFibredCategories) | A Lean4 Formalization of Fibred Categories | Apache-2.0 | v4.4.0-rc1 | 3,574 | 2026-04-15 | ✗ | -| 5 | [smorel394/AbstractSimplicialComplex](https://github.com/smorel394/AbstractSimplicialComplex) | | | v4.0.0-rc4 | 4,552 | 2026-05-01 | – | -| 5 | [somombo/quicksort](https://github.com/somombo/formalized-quicksort) | Implementation and Formal Verification of the Quicksort Algorithm | Apache-2.0 | v4.14.0 | 2,168 | 2026-03-20 | ✗ | -| 5 | [VTrelat/ZFLean](https://github.com/VTrelat/ZFLean) | A practical framework for set-theoretical development in Lean | Apache-2.0 | v4.27.0 | 9,623 | 2026-04-01 | ✗ | -| 5 | [WuProver/lean_characteristic_set](https://github.com/WuProver/lean_characteristic_set) | Formalization of the Characteristic Set Method in Lean 4 | Apache-2.0 | v4.29.0-rc6 | 4,317 | 2026-03-26 | – | -| 5 | [znssong/Frucht](https://github.com/znssong/Frucht) | Formalization of Frucht's theorem in Lean | Apache-2.0 | v4.29.0-rc4 | 2,418 | 2026-03-21 | ✗ | -| 4 | [anlucia/chromatic_polynomial](https://github.com/anlucia/ChromaticPolynomial) | Chromatic polynomial in Lean4 | Apache-2.0 | v4.11.0-rc1 | 473 | 2025-03-24 | ✓ | -| 4 | [AtticusKuhn/Transition-System-Ranking-Function](https://github.com/AtticusKuhn/Transition-System-Ranking-Function) | | | v4.21.0-rc3 | 4,139 | 2026-01-12 | – | -| 4 | [AxiomMath/PartialRegularity](https://github.com/AxiomMath/partial-regularity) | Lean formalizations for the paper "Almost all primes are partially regular" | MIT | v4.26.0 | 4,274 | 2026-03-25 | ✗ | -| 4 | [bustercopley/lean-float](https://github.com/bustercopley/lean-float) | Lemmas on floating-point arithmetic, in Lean 4 | | v4.19.0-rc2 | 1,773 | 2025-08-05 | – | -| 4 | [CBirkbeck/ModularForms_Lean4](https://github.com/CBirkbeck/ModularForms_Lean4) | | | v4.5.0-rc1 | 11,539 | 2024-11-08 | – | -| 4 | [Command-Master/pseudorandom](https://github.com/Command-Master/lean-bourgain) | | Apache-2.0 | v4.7.0 | 7,322 | 2024-11-05 | ✗ | -| 4 | [Dominique-Lawson/lean_4](https://github.com/Dominique-Lawson/Directed-Topology-Lean-4) | | MIT | v4.6.0-rc1 | 6,721 | 2026-03-26 | ✓ | -| 4 | [doxtor6/MerLean_FormalQualBench](https://github.com/doxtor6/MerLean_FormalQualBench) | | | v4.28.0-rc1 | 10,415 | 2026-05-08 | – | -| 4 | [fgdorais/extra](https://github.com/fgdorais/extra4) | Supplements to the Lean 4 Standard Library | Apache-2.0 | v4.29.0-rc3 | 4,647 | 2026-04-18 | ✗ | -| 4 | [FLDutchmann/selbergSieve](https://github.com/FLDutchmann/selberg-sieve4) | A formalisation of the Selberg sieve in Lean 4 | Apache-2.0 | v4.7.0-rc2 | 3,534 | 2026-04-08 | ✗ | -| 4 | [FordUniver/thebook.lean](https://github.com/FordUniver/thebook.lean) | Proofs from THE BOOK written up in lean | | v4.17.0-rc1 | 1,072 | 2025-12-30 | – | -| 4 | [hgoldstein95/palamedes](https://github.com/hgoldstein95/palamedes-lean) | | MIT | v4.24.0 | 6,291 | 2026-04-09 | ✗ | -| 4 | [hojonathanho/isoperimetric](https://github.com/hojonathanho/isoperimetric) | Lean 4 proofs of the isoperimetric inequality, Brunn-Minkowski inequality, and Prékopa-Leindler inequality | Apache-2.0 | v4.26.0-rc2 | 1,157 | 2026-04-25 | – | -| 4 | [imbrem/discretion](https://github.com/imbrem/discretion) | Utilities for formalizing programming languages in Lean 4, along with other tidbits | 0BSD | v4.20.0-rc5 | 27,354 | 2025-07-02 | ✗ | -| 4 | [input-output-hk/CardanoLedgerApi](https://github.com/input-output-hk/CardanoLedgerApiBlaster) | Cardano Ledger Api providing the necessary types and predicates to prove Plutus smart contracts with Blaster | Apache-2.0 | v4.24.0 | 7,037 | 2026-04-27 | ✗ | -| 4 | [ionathanch/CBPV](https://github.com/ionathanch/CBPV) | Lean 4 mechanization of assorted CBPV metatheory. | Zlib | v4.28.0 | 4,756 | 2026-04-01 | ✗ | -| 4 | [JobPetrovcic/ArtinWedderburn](https://github.com/JobPetrovcic/ArtinWedderburn) | A formalized proof of Artin-Wedderburn theorem in Lean4 | MIT | v4.14.0-rc2 | 2,768 | 2025-07-14 | ✗ | -| 4 | [JoeyEremondi/lean-cwf](https://github.com/JoeyEremondi/lean-cwf) | A basic Categories with Families library for Lean | BSD-3-Clause | | 5,346 | 2025-02-18 | – | -| 4 | [jrr6/lean-tables](https://github.com/jrr6/lean-tables) | A dependently-typed tables library, written in Lean 4, based on the Brown Benchmark for Table Types (B2T2). | | v4.14.0 | 8,097 | 2026-03-26 | – | -| 4 | [juanjomadrigal/denotational-lean](https://github.com/juanjomadrigal/denotational-lean) | | | v4.24.0 | 1,048 | 2025-12-03 | – | -| 4 | [kim-em/lean-finmap](https://github.com/kim-em/lean-finmap) | | Apache-2.0 | nightly-2025-08-19 | 1,103 | 2025-10-01 | ✗ | -| 4 | [lexzaiello/Dcc](https://github.com/lexzaiello/DCC) | The dependently-typed combinator calculus (DCC). | GPL-3.0 | v4.26.0 | 2,203 | 2026-04-29 | ✗ | -| 4 | [lindy-labs/corelib_verification](https://github.com/lindy-labs/corelib_verification) | | GPL-3.0 | v4.20.0-rc5 | 4,729 | 2025-06-11 | ✗ | -| 4 | [Linyxus/capless](https://github.com/Linyxus/capless-lean) | | MIT | v4.21.0-rc3 | 11,441 | 2026-01-29 | ✗ | -| 4 | [mariovagomarzal/HigherCategoryTheory](https://github.com/mariovagomarzal/higher_category_theory) | A formal verification project based on the work by Enric Cosme Llópez on "Higher-order categories". | Apache-2.0 | v4.28.0 | 2,864 | 2026-04-25 | ✗ | -| 4 | [markusdemedeiros/Metrology](https://github.com/markusdemedeiros/Metrology) | | | v4.29.0 | 37,035 | 2026-05-08 | – | -| 4 | [mbkybky/KoszulComplex](https://github.com/mbkybky/KoszulComplex) | | | v4.28.0-rc1 | 429 | 2026-03-16 | – | -| 4 | [MichaelStollBayreuth/LegendreQF](https://github.com/MichaelStollBayreuth/LegendreQF) | Lean code formalizing a proof of Legendre's theorem on diagonal ternary quadratic forms | GPL-2.0 | v4.24.0 | 1,888 | 2025-11-01 | – | -| 4 | [pandaman64/QuickSortInLean](https://github.com/pandaman64/QuickSortInLean) | | | v4.8.0-rc2 | 1,041 | 2024-08-08 | – | -| 4 | [pandaman64/Tables](https://github.com/pandaman64/Tables) | | | v4.30.0-rc2 | 4,908 | 2026-05-02 | – | -| 4 | [parabamoghv/Symm](https://github.com/parabamoghv/DashedMonoids) | Formalization of a new data structure: Dashed-Monoids | GPL-3.0 | v4.7.0 | 6,139 | 2026-02-01 | ✗ | -| 4 | [Rickerd1234/RelationalAlgebra](https://github.com/Rickerd1234/RelationalAlgebra) | University Master Thesis | Apache-2.0 | v4.24.0 | 6,315 | 2026-03-08 | ✗ | -| 4 | [roos-j/BooleanFun](https://github.com/roos-j/lean-booleanfun) | Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier anal… | Apache-2.0 | v4.16.0-rc2 | 1,517 | 2026-03-03 | ✗ | -| 4 | [rupakm/leslie](https://github.com/rupakm/leslie) | | Apache-2.0 | v4.27.0 | 103,563 | 2026-04-29 | ✗ | -| 4 | [samuelborza/IsTranscendentalPi](https://github.com/samuelborza/IsTranscendentalPi) | Formalization in Lean of the transcendence of π. | Apache-2.0 | v4.30.0-rc2 | 1,755 | 2026-04-27 | – | -| 4 | [samvang/StoneDualityInLean](https://github.com/samvang/StoneDualityInLean) | | | v4.8.0-rc1 | 1,079 | 2025-11-27 | – | -| 4 | [Shreyas4991/Algolean](https://github.com/Shreyas4991/Algolean) | Algorithms and Complexity Library using the lightweight query combinator framework called "Prog" | Apache-2.0 | v4.29.0 | 4,840 | 2026-04-21 | ✗ | -| 4 | [sinianluoye/LeanOfRudinAnalysis](https://github.com/sinianluoye/LeanOfRudinAnalysis) | Lean code about Rudin's 《Principles of Mathematical Analysis》 | | v4.22.0-rc4 | 8,438 | 2026-02-21 | – | -| 4 | [sterraf/ChainBounding](https://github.com/sterraf/ChainBounding) | Formalization of a simpler proof of Zorn's Lemma | Apache-2.0 | v4.8.0-rc1 | 441 | 2025-07-03 | – | -| 4 | [T-Brick/numbers](https://github.com/T-Brick/Numbers) | Arbitrary Bit-Length Integers in Lean | GPL-3.0 | v4.25.0 | 676 | 2025-11-14 | ✓ | -| 4 | [thejohncrafter/Catlib4](https://github.com/thejohncrafter/Catlib4) | Lean 4 library heavily focused on category theory and theoretical computer science | | nightly-2023-04-20 | 3,045 | 2024-11-25 | – | -| 4 | [Timeroot/Z80Emu](https://github.com/Timeroot/Z80Emu) | Z80 Emulator in Lean with verified program demos | | v4.28.0 | 7,523 | 2026-04-30 | – | -| 4 | [uw-math-ai/FormalizingGMT](https://github.com/uw-math-ai/FormalizingGMT) | | | v4.26.0-rc2 | 3,141 | 2026-04-30 | – | -| 4 | [vbeffara/rMT4](https://github.com/vbeffara/RMT4) | The Riemann mapping theorem | Apache-2.0 | v4.26.0 | 1,988 | 2026-01-10 | ✗ | -| 4 | [wupr/order-p-q](https://github.com/wupr/order-p-q) | Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers. | Apache-2.0 | v4.15.0 | 924 | 2026-01-19 | ✗ | -| 4 | [xyzw12345/CohenMacaulay](https://github.com/xyzw12345/CohenMacaulay) | | | v4.19.0-rc2 | 2,083 | 2025-05-01 | – | -| 4 | [YaelDillies/MiscYD](https://github.com/YaelDillies/misc-yd) | Miscellaneous projects I am working on in Lean | Apache-2.0 | v4.29.0 | 3,384 | 2026-04-14 | ✗ | -| 3 | [adri326/rubin-lean4](https://github.com/adri326/rubin-lean4) | Proof of Rubin's theorem, written in Lean 4 | | v4.5.0-rc1 | 9,198 | 2024-03-29 | – | -| 3 | [Aksenov239/lean-fun](https://github.com/Aksenov239/lean-fun) | | | v4.27.0-rc1 | 1,883 | 2026-05-05 | – | -| 3 | [Akwardbro/RamificationGroup](https://github.com/Akwardbro/RamificationGroup) | Formalizing Ramification Group in LEAN | | v4.29.0-rc2 | 16,430 | 2026-03-01 | – | -| 3 | [AlexKontorovich/CoveringSpacesProject](https://github.com/AlexKontorovich/CoveringSpacesProject) | | Apache-2.0 | v4.29.0-rc8 | 6,174 | 2026-04-15 | ✗ | -| 3 | [AlexLoitzl/pumping_cfg](https://github.com/AlexLoitzl/pumping_cfg) | | Apache-2.0 | v4.15.0-rc1 | 3,944 | 2025-11-22 | ✗ | -| 3 | [AntoineChambert-Loir/Jordan4](https://github.com/AntoineChambert-Loir/Jordan4) | | | v4.16.0 | 13,660 | 2025-09-13 | – | -| 3 | [aroheebhoja/vizing](https://github.com/aroheebhoja/vizing) | Lean4 formalization of Vizing's theorem using the Misra and Gries edge contraction algorithm | | v4.21.0-rc3 | 3,752 | 2026-03-27 | – | -| 3 | [Arthur742Ramos/Metatheory](https://github.com/Arthur742Ramos/Metatheory) | | MIT | v4.24.0 | 61,416 | 2026-04-24 | ✓ | -| 3 | [atrieu/cryptolib](https://github.com/atrieu/lean-cryptolib) | | Apache-2.0 | v4.17.0-rc1 | 889 | 2025-04-29 | ✓ | -| 3 | [b-mehta/HighlyAbundant](https://github.com/b-mehta/HighlyAbundant) | Formalisations relating to https://mathoverflow.net/q/501066/117945 | | v4.24.0-rc1 | 12,957 | 2025-12-19 | – | -| 3 | [BarinderBanwait/ramanujan_nagell](https://github.com/BarinderBanwait/ramanujan_nagell) | | | v4.26.0-rc2 | 3,571 | 2026-04-08 | – | -| 3 | [Bergschaf/Localic-Caratheodory-Extensions](https://github.com/Bergschaf/Localic-Caratheodory-Extensions) | | GPL-3.0 | v4.28.0-rc1 | 5,136 | 2026-03-12 | ✗ | -| 3 | [bjoernkjoshanssen/interest](https://github.com/bjoernkjoshanssen/interest) | Interest: a Lean library for financial mathematics | Apache-2.0 | v4.27.0-rc1 | 7,685 | 2026-02-13 | ✗ | -| 3 | [bridgekat/claude-formalizer](https://github.com/bridgekat/claude-formalizer) | Autoformalization baseline experiment with Claude Code. | | v4.29.0-rc8 | 2,449 | 2026-03-28 | – | -| 3 | [cymcymcymcym/Unique_Factorization_Lean4](https://github.com/cymcymcymcym/Unique_Factorization_Lean4) | A lean 4 proof of unique prime factorization in well-ordered rings, starting from ring axioms. | | v4.12.0-rc1 | 2,373 | 2026-01-15 | – | -| 3 | [enricozb/buffon-lean](https://github.com/enricozb/buffon-lean) | buffon's needle in lean 4 | | v4.4.0 | 922 | 2026-04-29 | – | -| 3 | [ezhuchko/RLTL-derivatives](https://github.com/ezhuchko/RLTL-derivatives) | Lean formalization for the paper "Symbolic Automata: 𝜔-Regularity Modulo Theories" | | v4.7.0 | 1,248 | 2025-05-15 | – | -| 3 | [fgdorais/GMLInit](https://github.com/fgdorais/GMLInit) | GML Init Package | CC0-1.0 | v4.9.0-rc1 | 6,818 | 2024-10-09 | – | -| 3 | [formalproofs/mdplib](https://github.com/formalproofs/MDPLib) | | Unlicense | v4.30.0-rc2 | 3,154 | 2026-04-24 | ✓ | -| 3 | [functionally/Crypto](https://github.com/functionally/crypto-lean4) | Implementation of various cryptographic functions in Lean4 | MIT | v4.7.0 | 2,842 | 2025-10-23 | ✗ | -| 3 | [goens/Hoare](https://github.com/goens/lean-hoare) | Hoare Logic in Lean | MIT | v4.22.0-rc2 | 1,487 | 2026-04-12 | ✗ | -| 3 | [guest2180/lean4-quantum](https://github.com/guest2180/lean4-quantum) | An implementation of the theory of quantum computing in the Lean programming language (using the Lean theorem prover ve… | | v4.16.0 | 5,150 | 2025-12-27 | – | -| 3 | [Gusarich/tvm-lean](https://github.com/Gusarich/tvm-lean) | | MIT | v4.24.0 | 345,213 | 2026-02-28 | ✗ | -| 3 | [harfe/fixed-point-theorems-lean4](https://github.com/harfe/fixed-point-theorems-lean4) | Kakutani fixed-point theorem and Brouwer fixed-point theorem formalized and proven in Lean 4 | | v4.21.0-rc3 | 3,257 | 2026-03-04 | – | -| 3 | [hdmkindom/mathmatic_in_elementary_number_th](https://github.com/hdmkindom/mathmatic_in_elementary_number_th) | 初等数论讲义的形式化证明 by lean4 | Apache-2.0 | v4.24.0-rc1 | 300 | 2025-09-23 | ✗ | -| 3 | [hsjoihs/dpda-lean](https://github.com/hsjoihs/dpda-lean) | | | v4.22.0-rc3 | 2,503 | 2025-07-10 | – | -| 3 | [ishiut/fo_zfc](https://github.com/ishiut/fo_zfc) | | Apache-2.0 | v4.22.0-rc3 | 2,450 | 2025-08-04 | – | -| 3 | [JasonShroyer/sgc](https://github.com/JasonShroyer/sgc-lean) | Lean 4 library characterizing the algebraic structure of metastability and consolidation in stochastic systems | Apache-2.0 | v4.25.2 | 12,192 | 2026-04-26 | ✗ | -| 3 | [jcpaik/erdos-tuza-valtr](https://github.com/jcpaik/erdos-tuza-valtr) | A formal verification of a mathematics/combinatorics paper "On the Erdős-Tuza-Valtr Conjecture" | | v4.13.0-rc3 | 2,302 | 2024-11-09 | – | -| 3 | [jjaassoonn/GAGA](https://github.com/jjaassoonn/GAGA) | (Attempt of) Formalising the GAGA theorem | | v4.7.0-rc2 | 338 | 2025-02-09 | – | -| 3 | [jjdishere/neukirch](https://github.com/jjdishere/neukirch) | | | v4.5.0-rc1 | 4,756 | 2024-12-03 | – | -| 3 | [Jun2M/Main-theorem-of-polytopes](https://github.com/Jun2M/Main-theorem-of-polytopes) | Proving the main theorem of polytopes using Lean 4 | | v4.7.0-rc2 | 2,293 | 2024-05-22 | – | -| 3 | [katzenpost/crypt_walker](https://github.com/katzenpost/crypt_walker) | Lean and Rust based cryptographic protocol framework for formally proving protocol properties | AGPL-3.0 | | | 2024-08-24 | ✓ | -| 3 | [KisaraBlue/ec-tate-lean](https://github.com/KisaraBlue/ec-tate-lean) | Separate project from mathib4 | | nightly-2023-08-19 | 7,786 | 2024-05-26 | – | -| 3 | [kmill/msri2023_graphs](https://github.com/kmill/msri2023_graphs) | Repository for graph theory & combinatorics group at the MSRI Lean summer school | Apache-2.0 | nightly-2023-06-10 | 3,851 | 2024-11-12 | ✓ | -| 3 | [LeastAuthority/STIR](https://github.com/LeastAuthority/STIR) | SC: Ethereum - zk(E)VM Verification - STIR Lean Blueprint | Apache-2.0 | v4.19.0-rc3 | 780 | 2025-05-05 | ✗ | -| 3 | [LodeVermeulen/Lean4_Bogdanovs_lemma](https://github.com/LodeVermeulen/Lean4_Bogdanovs_lemma) | | | v4.8.0-rc1 | 1,209 | 2024-07-03 | – | -| 3 | [lua-vr/BirkhoffErgodicThm](https://github.com/lua-vr/pointwise-birkhoff) | A proof of Pointwise Birkhoff Ergodic Theorem in Lean | Apache-2.0 | v4.20.0-rc5 | 567 | 2025-06-20 | ✗ | -| 3 | [lunsong/JaxProof](https://github.com/lunsong/JaxProof) | | | v4.28.0 | 1,354 | 2026-05-08 | – | -| 3 | [manuelpuebla/amo-lean](https://github.com/manuelpuebla/amo-lean) | | MIT | v4.26.0 | 70,605 | 2026-04-23 | – | -| 3 | [matematiflo/SumSq](https://github.com/matematiflo/SumsOfSquares) | Summing squares in Lean | Apache-2.0 | v4.10.0-rc2 | 1,389 | 2025-10-24 | ✗ | -| 3 | [mattrobball/BridgelandStability](https://github.com/mattrobball/BridgelandStability) | | Apache-2.0 | v4.29.0 | 36,493 | 2026-04-21 | – | -| 3 | [mckoen/quasicategory](https://github.com/mckoen/quasicategory) | Formalizing quasi-categories in Lean | | v4.18.0-rc1 | 11,675 | 2025-10-25 | – | -| 3 | [MichaelMMacLeod/formal-mergesort](https://github.com/MichaelMMacLeod/formal-mergesort) | WIP formally-verified implementation of mergesort (efficient; only allocates one auxiliary array, sorts arrays in-place) | | v4.19.0-rc3 | 2,916 | 2025-05-16 | – | -| 3 | [MohanadAhmed/LeanMathSigProc](https://github.com/MohanadAhmed/LeanMathSigProc) | | GPL-2.0 | v4.10.0 | 623 | 2025-08-29 | ✗ | -| 3 | [mrdouglasny/gaussian-field](https://github.com/mrdouglasny/gaussian-field) | | | v4.29.0 | 51,203 | 2026-05-09 | – | -| 3 | [mrigankpawagi/LeanearTemporalLogic](https://github.com/mrigankpawagi/LeanearTemporalLogic) | Formalization of Linear Temporal Logic (LTL) in Lean 4. | | v4.18.0-rc1 | 4,244 | 2026-03-10 | – | -| 3 | [nielstron/langlib](https://github.com/nielstron/langlib) | Library for formal language theory in Lean 4 | BSD-2-Clause | v4.28.0 | 40,844 | 2026-04-28 | ✗ | -| 3 | [nsglover/Lean-4.0-LLL](https://github.com/nsglover/Lean-4.0-LLL) | | | v4.4.0-rc1 | 589 | 2025-10-19 | – | -| 3 | [oneofvalts/desargues](https://github.com/oneofvalts/desargues) | Lean formalization of Desargues's Theorem | | | 1,221 | 2025-07-14 | – | -| 3 | [Oscario0/LeanBisection](https://github.com/Oscario0/LeanBisection) | The Bisection method is the simplest numerical approximation approach in mathematics that applies to any continuous fun… | MIT | v4.30.0-rc1 | 1,797 | 2026-02-28 | ✗ | -| 3 | [pannous/Hyper](https://github.com/pannous/hyper-lean) | Hyperreal Numbers in Lean 4 | Apache-2.0 | v4.27.0 | 9,636 | 2026-03-21 | ✗ | -| 3 | [peabrainiac/CatDG](https://github.com/peabrainiac/lean-catdg) | Aspects of categorical differential geometry, formalised in lean 4. | Apache-2.0 | v4.29.0 | 9,760 | 2026-04-14 | ✗ | -| 3 | [PratherConid/LeanLambda](https://github.com/PratherConid/LeanLambda) | | | v4.20.0 | 5,812 | 2026-02-23 | – | -| 3 | [provables/special-numbers](https://github.com/provables/special-numbers) | Special Numbers (Chapter 6 from Knuth's Concrete Mathematics) | MIT | v4.15.0 | 647 | 2025-06-10 | ✗ | -| 3 | [riccardobrasca/SDG](https://github.com/riccardobrasca/SDG) | Synthetic Differential Geometry in Lean | Apache-2.0 | riccardobrasca/lean4:v4.30.0-rc2-less-choice | 1,496 | 2026-04-28 | ✗ | -| 3 | [seb488/LeanComplexAnalysis](https://github.com/seb488/LeanComplexAnalysis) | Lean formalization of some classical complex analysis theorems | Apache-2.0 | v4.28.0-rc1 | 4,910 | 2026-03-19 | – | -| 3 | [smorel394/ExteriorPowers](https://github.com/smorel394/ExteriorPowers) | | | v4.7.0-rc2 | 8,922 | 2024-01-12 | – | -| 3 | [smorel394/Grassmannian](https://github.com/smorel394/Grassmannian) | | | v4.2.0-rc1 | 8,133 | 2024-10-08 | – | -| 3 | [smorel394/ProjectiveSpace_lean4](https://github.com/smorel394/ProjectiveSpace_lean4) | | | v4.2.0-rc1 | 5,767 | 2024-01-16 | – | -| 3 | [spitters/libcrux-lean-specs](https://github.com/spitters/libcrux-lean-specs) | Hax Lean 4 prelude for libcrux pure crypto specs | | v4.28.0 | 29,329 | 2026-04-20 | – | -| 3 | [suomela/Distributed2Coloring](https://github.com/suomela/2-coloring-1-round) | 2-Coloring Cycles in One Round: Formalization in Lean 4 | MIT | v4.28.0 | 17,214 | 2026-03-13 | ✗ | -| 3 | [tangentstorm/leansieve](https://github.com/tangentstorm/leansieve) | A formally verified prime number sieve in Lean4. | MIT | v4.29.0-rc6 | 1,241 | 2026-03-13 | – | -| 3 | [tchaumeny/KleeneTree](https://github.com/tchaumeny/KleeneTree) | Formalization of the Kleene tree in Lean | | v4.26.0 | 346 | 2026-04-08 | – | -| 3 | [themathqueen/Monlib](https://github.com/themathqueen/monlib4) | Formalising non-commutative graph theory in Lean | Apache-2.0 | v4.21.0-rc3 | 31,853 | 2026-01-06 | ✗ | -| 3 | [unhyperbolic/hyperbolicGeometryInLean](https://github.com/unhyperbolic/hyperbolicGeometryInLean) | Formalizing hyperbolic geometry in lean | | nightly-2023-06-20 | 933 | 2025-11-07 | – | -| 3 | [uw-math-ai/lean-polyhedral-geometry](https://github.com/uw-math-ai/lean-polyhedral-geometry) | Formalizing the basic definitions and results of polyhedral geometry in Lean 4. | GPL-3.0 | v4.20.0-rc5 | 1,475 | 2025-12-13 | – | -| 3 | [varosi/bitmap](https://github.com/varosi/Bitmap) | Lean 4 bitmap utilities with PNG encode/decode support, plus a small widget for visualization. | BSD-3-Clause | v4.29.0 | 23,444 | 2026-04-29 | ✗ | -| 3 | [wwylele/PentagonalNumberTheorem](https://github.com/wwylele/PentagonalNumberTheorem) | | | v4.26.0-rc2 | 2,856 | 2025-12-15 | – | -| 3 | [YanYablonovskiy/AlgebraicWheelTheory](https://github.com/YanYablonovskiy/AlgebraicWheelTheory) | Digitisation of algebraic wheel theory in Lean 4 | | v4.29.0-rc6 | 849 | 2026-04-02 | – | -| 3 | [YijunYuan/SphericalCompleteness](https://github.com/YijunYuan/SphericalCompleteness) | | | v4.29.1 | 5,743 | 2026-05-09 | – | -| 2 | [adambornemann-glitch/Logos_Library](https://github.com/adambornemann-glitch/Logos_Library) | Lean verified Science. | MIT | v4.29.0-rc3 | 128,550 | 2026-03-27 | – | -| 2 | [ADedecker/ProperAction](https://github.com/ADedecker/ProperAction) | | | v4.7.0-rc2 | 908 | 2024-05-14 | – | -| 2 | [AlexBrodbelt/DicksonsClassificationTheorem](https://github.com/AlexBrodbelt/DicksonsClassificationTheorem) | | | v4.24.0 | 5,831 | 2026-01-08 | – | -| 2 | [AlexeyMilovanov/lean-keccak-unrolled](https://github.com/AlexeyMilovanov/lean-keccak-unrolled) | | | v4.29.0 | 15,376 | 2026-04-27 | – | -| 2 | [alexjgreig/Quave](https://github.com/alexjgreig/QHL-Lean) | Quantum Hoare Logic Lean 4 - A quantum program verification tool | Apache-2.0 | v4.16.0-rc2 | 1,388 | 2025-09-08 | ✓ | -| 2 | [amarmaduke/lean-stlc](https://github.com/amarmaduke/lean-stlc) | Lean4 mechanization of the simply typed lambda calculus and its metatheory including strong normalization | MIT | v4.26.0 | 3,723 | 2026-04-28 | ✗ | -| 2 | [AnirudhG07/huffman](https://github.com/AnirudhG07/LeanHuffmanCoding) | Lean for Huffmann Coding Algorithms, as a course Project for Proof and Programs 25. | MIT | v4.29.0 | 3,388 | 2026-04-24 | ✓ | -| 2 | [AntoineChambert-Loir/Sion4](https://github.com/AntoineChambert-Loir/Sion4) | | | v4.21.0-rc3 | 3,319 | 2025-09-26 | – | -| 2 | [ATOMSLab/LeanBET](https://github.com/ATOMSLab/LeanBET) | Formally-verified BET Adsorption analysis in Lean | | v4.27.0-rc1 | 3,047 | 2026-04-28 | – | -| 2 | [AydenLamp/FinDFA](https://github.com/AydenLamp/FinDFA) | Lean code for thesis | | v4.25.0-rc2 | 2,375 | 2026-02-18 | – | -| 2 | [badly-drawn-wizards/noperthedron](https://github.com/badly-drawn-wizards/noperthedron) | A Lean4 formalization of "A convex polyhedron without Rupert’s property" | Apache-2.0 | v4.25.0-rc2 | 1,105 | 2026-02-15 | – | -| 2 | [bernborgess/lean-cutting-planes](https://github.com/bernborgess/lean-cutting-planes) | Cutting Planes formal logic modelled in Lean 4 for verified reasoning. | | v4.15.0-rc1 | 629 | 2025-12-03 | – | -| 2 | [bjoernkjoshanssen/ac-exercises](https://github.com/bjoernkjoshanssen/ac-exercises) | Exercise solutions in Lean 4 for the book "Automatic complexity: a computable measure of irregularity", De Gruyter, 202… | | v4.14.0-rc2 | 9,181 | 2026-02-13 | – | -| 2 | [bjoernkjoshanssen/hypothesis](https://github.com/bjoernkjoshanssen/hypothesis) | Probability and statistics in Lean | | v4.27.0-rc1 | 5,401 | 2026-02-18 | – | -| 2 | [bolito2/DemazureOperatorsLean](https://github.com/bolito2/DemazureOperatorsLean) | Formalizing some theorems about Demazure operators in Lean4 | Apache-2.0 | v4.14.0-rc3 | 2,927 | 2025-02-20 | – | -| 2 | [bsubercaseaux/lean-proofs](https://github.com/bsubercaseaux/lean-proofs) | Some of my Lean proofs | | v4.18.0-rc1 | 345 | 2025-03-19 | – | -| 2 | [CarlKCarlK/RangeSetBlaze](https://github.com/CarlKCarlK/range-set-blaze-lean) | | Apache-2.0 | v4.24.0-rc1 | 4,787 | 2025-11-01 | ✗ | -| 2 | [chrisflav/pi1](https://github.com/chrisflav/pi1) | A formalisation of the étale fundamental group of a scheme in Lean 4 | Apache-2.0 | v4.30.0-rc2 | 6,534 | 2026-04-27 | – | -| 2 | [ChrisHughes24/axgroth](https://github.com/ChrisHughes24/axgroth) | | | v4.23.0-rc2 | 933 | 2026-03-29 | – | -| 2 | [fgdorais/algebra](https://github.com/fgdorais/algebra4) | Algebra library for Lean 4 | Apache-2.0 | v4.29.0-rc3 | 2,853 | 2026-03-04 | ✗ | -| 2 | [fgdorais/lean4-automata](https://github.com/fgdorais/lean4-automata) | | Apache-2.0 | v4.23.0-rc1 | 1,938 | 2025-08-14 | ✗ | -| 2 | [fgdorais/logic](https://github.com/fgdorais/logic4) | Logic Library for Lean 4 | Apache-2.0 | v4.29.0-rc3 | 1,561 | 2026-03-03 | ✗ | -| 2 | [fpvandoorn/sard](https://github.com/fpvandoorn/sard) | Work towards a general version of Sard's theorem in Lean 4 | Apache-2.0 | v4.12.0 | 1,360 | 2024-10-07 | ✗ | -| 2 | [gift-framework/core](https://github.com/gift-framework/core) | GIFT Core: Certified mathematical identities from E8×E8 gauge theory on G2 manifolds. Verified in Lean 4 | MIT | v4.29.0 | 37,288 | 2026-05-05 | – | -| 2 | [gmcninch-prof/VERSEIM-2025](https://github.com/gmcninch-prof/VERSEIM-2025) | repo for the formalization project in VERSEIM-REU at Tufts 2025 | Apache-2.0 | | 29,081 | 2025-08-12 | – | -| 2 | [hwatheod/galeShapley](https://github.com/hwatheod/galeshapley-lean) | Formalization in Lean of some results related to stable matchings and the Gale-Shapley algorithm | MIT | v4.29.0-rc7 | 4,876 | 2026-03-24 | ✗ | -| 2 | [hyeoniuwu/CiL](https://github.com/hyeoniuwu/CiL) | | | v4.30.0-rc2 | 13,354 | 2026-05-05 | – | -| 2 | [idontgetoutmuch/DifferentialGeometry](https://github.com/idontgetoutmuch/DifferentialGeometry) | | | | 3,977 | 2026-04-17 | – | -| 2 | [int-y1/proofs](https://github.com/int-y1/proofs) | random proofs in lean 4 | MIT | v4.29.0-rc8 | 334,335 | 2026-04-09 | ✗ | -| 2 | [itsalissonsilva/LeanML](https://github.com/itsalissonsilva/lean-ml) | Formally verified machine learning in Lean 4. | Apache-2.0 | v4.30.0-rc1 | 626 | 2026-04-25 | ✓ | -| 2 | [ivankobe/FactorizationSystems](https://github.com/ivankobe/FactorizationSystems) | | MIT | v4.14.0-rc2 | 2,501 | 2025-01-21 | ✗ | -| 2 | [j-loreaux/LeanOA](https://github.com/j-loreaux/LeanOA) | Operator algebras in Lean | | v4.30.0-rc2 | 6,249 | 2026-05-04 | – | -| 2 | [JJYYY-JJY/NormalForms](https://github.com/JJYYY-JJY/lean-normal-forms) | Executable Hermite and Smith Normal Forms in Lean 4 over Euclidean Domains, with a PID bridge to mathlib. | Apache-2.0 | | | 2026-03-22 | ✗ | -| 2 | [jzxia/WhiteheadTheorem](https://github.com/jzxia/WhiteheadTheorem) | Proving the Whitehead theorem for Mathlib's homotopy groups. | | v4.21.0-rc3 | 7,984 | 2026-03-12 | – | -| 2 | [kckennylau/EllipticCurve](https://github.com/kckennylau/EllipticCurve) | Towards a general definition of elliptic curve over schemes | Apache-2.0 | v4.25.0-rc2 | 7,309 | 2025-11-04 | ✗ | -| 2 | [kkytola/ExtremeValueProject](https://github.com/kkytola/ExtremeValueProject) | A project to formalize Fisher-Tippett-Gnedenko theorem (default project of course MS-EV0029) | Apache-2.0 | v4.23.0-rc2 | 4,156 | 2025-08-15 | ✗ | -| 2 | [klavins/LeanBook](https://github.com/klavins/LeanBook) | Notes on the Foundations of Lean | GPL-3.0 | | | 2025-08-21 | ✗ | -| 2 | [Koukyosyumei/pol](https://github.com/Koukyosyumei/PoL) | Proof of Lean: Formalizing Blockchain Fundamentals in Lean | Apache-2.0 | v4.22.0-rc3 | 919 | 2025-08-26 | ✓ | -| 2 | [kuruczgy/lean-model-checking](https://github.com/kuruczgy/lean-model-checking) | Formalizations of some theorems related to model checking | Apache-2.0 | v4.29.0 | 2,420 | 2026-03-31 | – | -| 2 | [lambdaclass/optisat](https://github.com/lambdaclass/truth_research) | Formally verified equality saturation engine in Lean 4, parameterized by typeclasses. OptiSat provides a domain-agnosti… | MIT | v4.26.0 | 12,242 | 2026-04-27 | ✓ | -| 2 | [lean-ja/verso-manual](https://github.com/lean-ja/reference-manual-ja) | 「The Lean Language Reference」の日本語訳（作業中） | Apache-2.0 | v4.15.0-rc1 | 35,297 | 2025-01-05 | ✗ | -| 2 | [lindy-labs/WadrayVerification](https://github.com/lindy-labs/wadray_verification) | Verification of the Wadray library | GPL-3.0 | v4.9.0-rc2 | 3,344 | 2024-06-21 | ✗ | -| 2 | [Louis-Le-Grand/Formalisation-of-constructable-numbers](https://github.com/Louis-Le-Grand/Formalisation-of-constructable-numbers) | | | v4.11.0-rc2 | 6,146 | 2024-11-13 | – | -| 2 | [m4lvin/Gossip](https://github.com/m4lvin/Gossip-in-Lean) | Verified Results about Gossip protocols in Lean 4 | Apache-2.0 | v4.28.0 | 3,233 | 2026-04-29 | ✗ | -| 2 | [madvorak/matroids](https://github.com/madvorak/matroids) | Classes of matroids and their properties | MIT | v4.7.0 | 625 | 2024-04-25 | – | -| 2 | [madvorak/thue](https://github.com/madvorak/thue) | Semi-Thue systems a.k.a. string rewriting systems | BSD-2-Clause | nightly-2023-07-12 | 1,012 | 2024-10-21 | ✗ | -| 2 | [mariainesdff/ostrowski2024](https://github.com/mariainesdff/ostrowski2024) | | | v4.26.0-rc2 | 2,507 | 2025-12-14 | – | -| 2 | [mbkybky/InfiniteGaloisTheory](https://github.com/mbkybky/InfiniteGaloisTheory) | Formalizing infinite Galois theory in LEAN | | v4.12.0-rc1 | 4,728 | 2026-05-04 | – | -| 2 | [mbkybky/QuillenSuslin](https://github.com/mbkybky/QuillenSuslin) | Formalizing Quillen-Suslin theorem in LEAN | | v4.28.0-rc1 | 5,062 | 2026-05-06 | – | -| 2 | [mdbrnowski/Apportionmentlib](https://github.com/mdbrnowski/apportionmentlib) | Formal verification of apportionment theory. | Apache-2.0 | v4.28.0 | 376 | 2026-03-23 | ✗ | -| 2 | [Mintpath/p_ne_np](https://github.com/Mintpath/p-neq-np-lean) | Machine-verified proof (0 sorries, 2 axioms) that P ≠ NP via exponential circuit lower bounds for Hamiltonian Cycle. Le… | MIT | v4.28.0 | 15,606 | 2026-03-29 | ✗ | -| 2 | [misaka10987/archimedes](https://github.com/misaka10987/archimedes) | Don't disturb my circle! | MIT | v4.25.0-rc2 | 412 | 2025-11-04 | ✗ | -| 2 | [mitchell-horner/ErdosStoneSimonovitsKovariSosTuran](https://github.com/mitchell-horner/ErdosStoneSimonovitsKovariSosTuran) | Formalising the Erdős-Stone-Simonovits theorem and the Kővári–Sós–Turán theorem in Lean | Apache-2.0 | v4.16.0-rc2 | 3,341 | 2026-04-29 | ✗ | -| 2 | [monsterkrampe/PossiblyInfiniteTrees](https://github.com/monsterkrampe/Possibly-Infinite-Trees) | This repo formalizes (possibly) infinite trees of finite degree in Lean. So far this is mainly a dependency for one of… | Apache-2.0 | v4.29.0 | 3,114 | 2026-04-14 | ✗ | -| 2 | [mrdouglasny/jacobian-challenge](https://github.com/mrdouglasny/jacobian-challenge) | Lean 4 attempt at Kevin Buzzard's Jacobian Challenge (Apr 2026) | | v4.30.0-rc1 | 27,833 | 2026-04-29 | – | -| 2 | [nasqret/fineqs](https://github.com/nasqret/fineqs) | Lean4 formalization with Artistotle of the arXiv paper 1906.11174 | Apache-2.0 | v4.24.0 | 648 | 2026-01-26 | ✗ | -| 2 | [NickAdfor/The-polynomial-method-and-restricted-sums-of-congruence-classes](https://github.com/NickAdfor/The-polynomial-method-and-restricted-sums-of-congruence-classes) | | | v4.27.0-rc1 | 4,149 | 2026-03-13 | – | -| 2 | [niklasmohrin/LeanSeminar](https://github.com/niklasmohrin/lean-seminar-2023) | Construction of a flow equivalent forest from a flow matrix in Lean 4 | MIT | v4.7.0 | 2,306 | 2025-02-07 | ✗ | -| 2 | [nomeata/lean-darray](https://github.com/nomeata/lean-darray) | | Apache-2.0 | v4.28.0 | 933 | 2026-03-30 | – | -| 2 | [NoneMore/StabilityTheory](https://github.com/NoneMore/StabilityTheory) | | | v4.30.0-rc1 | 2,337 | 2026-05-07 | – | -| 2 | [penteract/pythagTreeProof](https://github.com/penteract/pythagTreeProof) | A formal proof that the area of the pythagoras tree is 1282341301154741436886299752561669174104157968892079433136395356… | | v4.22.0-rc3 | 7,813 | 2025-07-22 | – | -| 2 | [physicslib/Physicslib](https://github.com/physicslib/physicslib4) | Solving Hilbert's sixth problem in Lean | Apache-2.0 | v4.23.0-rc2 | 399 | 2026-01-19 | ✗ | -| 2 | [pitmonticone/QuadraticIntegers](https://github.com/pitmonticone/QuadraticIntegers) | Formalising the Ring of Integers in Quadratic Fields in the Lean proof assistant. | Apache-2.0 | v4.24.0 | 2,126 | 2026-03-09 | – | -| 2 | [pitmonticone/SumsThreeSquares](https://github.com/pitmonticone/SumsThreeSquares) | Formalising the paper "Sums of Three Squares" by N. C. Ankeny in Lean with Aristotle. | Apache-2.0 | v4.29.1 | 1,021 | 2026-04-23 | – | -| 2 | [Project-Navi/cd-formalization](https://github.com/Project-Navi/cd-formalization) | Lean 4 + Mathlib formalization of the Creative Determinant framework — 15 theorems proved with zero sorry, CI-enforced… | Apache-2.0 | v4.28.0 | 2,893 | 2026-04-22 | – | -| 2 | [SamuelSchlesinger/analysis-of-boolean-functions](https://github.com/SamuelSchlesinger/analysis-of-boolean-functions) | Lean 4 formalization of Analysis of Boolean Functions by Ryan O'Donnell | | v4.29.0-rc6 | 1,480 | 2026-04-02 | – | -| 2 | [schmittj/balanced-vectors-blueprint](https://github.com/schmittj/balanced-vectors-blueprint) | Lean Blueprint for technical lemma on maxima and minimal of certain log-concave functions | | v4.26.0 | 1,265 | 2026-03-21 | – | -| 2 | [Shilun-Allan-Li/tcslib](https://github.com/Shilun-Allan-Li/tcslib) | Lean 4 Theoretical Computer Science Library | Apache-2.0 | v4.25.0-rc2 | 70,012 | 2026-05-08 | – | -| 2 | [smmercuri/adele-ring_locally-compact](https://github.com/smmercuri/adele-ring_locally-compact) | The proof that the adele ring of a number field is locally compact, formalised in Lean 4. | Apache-2.0 | v4.10.0-rc2 | 1,937 | 2026-04-24 | ✗ | -| 2 | [SReichelt/universe-abstractions](https://github.com/SReichelt/universe-abstractions) | A Lean 4 project to formalize mathematical universes with added structure | | nightly-2022-01-14 | 19,432 | 2024-04-08 | – | -| 2 | [tdzl2003/geometry](https://github.com/tdzl2003/LeanEuclid) | | MIT | v4.21.0 | 2,733 | 2025-12-15 | ✗ | -| 2 | [tsurumi-yizhou/SPG](https://github.com/tsurumi-yizhou/SPG) | A Lean 4 library for analyzing Spin Point Groups | Apache-2.0 | v4.29.0-rc4 | 1,764 | 2026-03-10 | ✓ | -| 2 | [vikraman/event-structures](https://github.com/vikraman/event-structures) | Formalisation of some facts about event structures and reversibility | Apache-2.0 | v4.28.1 | 1,300 | 2026-04-24 | ✗ | -| 2 | [vporton/atgt](https://github.com/vporton/atgt) | Formalizing Victor Porton's Navier-Stokes Proof in Lean | | v4.28.0-rc1 | 8,661 | 2026-03-10 | – | -| 2 | [wjrtz/lean_game_theory](https://github.com/wjrtz/lean_game_theory) | Formalization of game theory in LEAN | | v4.2.0 | 918 | 2026-01-14 | – | -| 2 | [Xiyou-Wu/RiemannianGeometry](https://github.com/Xiyou-Wu/RiemannianGeometry) | | Apache-2.0 | | | 2026-01-01 | ✗ | -| 2 | [YaelDillies/ForbiddenMatrix](https://github.com/YaelDillies/forbidden-matrix) | Formalisation of forbidden matrix theory | Apache-2.0 | v4.29.0 | 1,667 | 2026-04-01 | ✗ | -| 2 | [YaelDillies/MeanFourier](https://github.com/YaelDillies/mean-fourier) | Formalisation of mean Fourier analysis in Lean 4 | Apache-2.0 | v4.30.0-rc2 | 1,079 | 2026-04-14 | ✗ | -| 2 | [YijunYuan/HarderNarasimhan](https://github.com/YijunYuan/HarderNarasimhan) | Formalization of Harder-Narasimhan theory | Apache-2.0 | v4.29.1 | 9,716 | 2026-04-12 | ✗ | +| Stars | Package | Description | License | Lean | LOC | Updated | Build | In Pool | +| ---: | --- | --- | --- | --- | ---: | --- | :---: | :---: | +| 1335 | [ulfjack/ryu](https://github.com/ulfjack/ryu) | Converts floating point numbers to decimal strings | Apache-2.0 | v4.27.0-rc1 | 578 | 2026-04-29 | ✗ | | +| 947 | [google-deepmind/formal_conjectures](https://github.com/google-deepmind/formal-conjectures) | A collection of formalized statements of conjectures in Lean. | Apache-2.0 | v4.27.0 | 66,093 | 2026-04-29 | ✗ | | +| 874 | [ImperialCollegeLondon/FLT](https://github.com/ImperialCollegeLondon/FLT) | Ongoing Lean formalisation of the proof of Fermat's Last Theorem | Apache-2.0 | v4.30.0-rc2 | 29,512 | 2026-04-29 | ✓ | | +| 555 | [leanprover-community/Physlib](https://github.com/leanprover-community/physlib) | A project to digitalise results from physics into Lean. | Apache-2.0 | v4.29.1 | 165,860 | 2026-04-29 | ✗ | | +| 516 | [teorth/equational_theories](https://github.com/teorth/equational_theories) | A project to map out the relations between different equational theories of Magmas. | Apache-2.0 | v4.29.1 | 163,668 | 2026-04-29 | ✗ | | +| 496 | [lecopivo/scilean](https://github.com/lecopivo/SciLean) | Scientific computing in Lean 4 | Apache-2.0 | v4.28.0-rc1 | 86,155 | 2026-04-28 | ✗ | | +| 376 | [leanprover-community/batteries](https://github.com/leanprover-community/batteries) | The "batteries included" extended library for the Lean programming language and theorem prover | Apache-2.0 | v4.30.0-rc2 | 32,053 | 2026-04-29 | ✓ | | +| 315 | [math-inc/strongpnt](https://github.com/math-inc/strongpnt) | | | v4.21.0 | 28,407 | 2026-05-07 | – | | +| 292 | [AlexKontorovich/PrimeNumberTheoremAnd](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd) | Blueprint for the PNT+ Project | Apache-2.0 | v4.28.0 | 67,777 | 2026-04-29 | ✗ | | +| 231 | [opencompl/SSA](https://github.com/opencompl/lean-mlir) | A minimal development of SSA theory | | nightly-2025-12-01 | 616,463 | 2026-04-29 | ✗ | | +| 228 | [verse-lab/veil](https://github.com/verse-lab/veil) | A verifier for automated and interactive proofs about transition systems. | Apache-2.0 | v4.24.0 | 12,878 | 2026-04-23 | ✗ | | +| 226 | [FormalizedFormalLogic/Foundation](https://github.com/FormalizedFormalLogic/Foundation) | Formalization of Mathematical Logic | Apache-2.0 | v4.29.0 | 100,587 | 2026-04-28 | ✗ | | +| 216 | [teorth/PFR](https://github.com/teorth/pfr) | Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results) | Apache-2.0 | v4.29.0 | 21,704 | 2026-04-20 | ✗ | | +| 189 | [Verified-zkEVM/Arklib](https://github.com/Verified-zkEVM/ArkLib) | Formally Verified Arguments of Knowledge in Lean | Apache-2.0 | v4.29.0 | 63,240 | 2026-04-28 | ✗ | | +| 182 | [digama0/lean4lean](https://github.com/digama0/lean4lean) | Lean 4 kernel / 'external checker' written in Lean 4 | Apache-2.0 | v4.29.0 | 20,191 | 2026-04-28 | ✗ | | +| 176 | [leanprover-community/iris-lean](https://github.com/leanprover-community/iris-lean) | Lean 4 port of Iris, a higher-order concurrent separation logic framework | Apache-2.0 | | 40,315 | 2026-04-29 | ✗ | | +| 134 | [Verified-zkEVM/Clean](https://github.com/Verified-zkEVM/clean) | Lean circuit DSL | MIT | v4.28.0 | 36,952 | 2026-04-29 | ✗ | | +| 128 | [eric-wieser/matrix_cookbook](https://github.com/eric-wieser/lean-matrix-cookbook) | The matrix cookbook, proved in the Lean theorem prover | MIT | v4.22.0-rc4 | 3,033 | 2026-04-04 | ✗ | | +| 128 | [loganrjmurphy/lib](https://github.com/loganrjmurphy/LeanEuclid) | LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean. | MIT | v4.19.0 | 9,719 | 2026-04-25 | ✗ | | +| 126 | [Timeroot/quantumInfo](https://github.com/Timeroot/Lean-QuantumInfo) | Quantum information theory in Lean 4 | MIT | v4.28.0 | 38,108 | 2026-04-22 | ✗ | | +| 117 | [google-deepmind/debate](https://github.com/google-deepmind/debate) | Formalizing stochastic doubly-efficient debate | Apache-2.0 | v4.8.0 | 3,106 | 2026-04-09 | ✗ | | +| 101 | [leanprover/lnsym](https://github.com/leanprover/LNSym) | Armv8 Native Code Symbolic Simulator in Lean | Apache-2.0 | nightly-2024-10-07 | 44,728 | 2026-04-19 | ✗ | | +| 98 | [optsuite/optlib](https://github.com/optsuite/optlib) | | Apache-2.0 | v4.13.0 | 17,275 | 2026-04-28 | ✗ | | +| 97 | [leanprover/sampcert](https://github.com/leanprover/SampCert) | SampCert : Verified Differential Privacy | Apache-2.0 | v4.29.0 | 18,503 | 2026-04-29 | ✗ | | +| 96 | [teorth/symmetric_project](https://github.com/teorth/symmetric_project) | | | v4.2.0-rc1 | 5,317 | 2026-04-11 | – | | +| 95 | [emilyriehl/InfinityCosmos](https://github.com/emilyriehl/infinity-cosmos) | A blueprint for a formalization of infinity-cosmos theory in Lean. | Apache-2.0 | v4.26.0-rc2 | 4,678 | 2026-04-25 | ✗ | | +| 95 | [pandaman64/lean-regex](https://github.com/pandaman64/lean-regex) | | Apache-2.0 | | 13,621 | 2026-04-12 | ✗ | | +| 91 | [Verified-zkEVM/VCVio](https://github.com/Verified-zkEVM/VCV-io) | Formalized Cryptography Proofs in Lean 4 | Apache-2.0 | v4.29.0 | 154,770 | 2026-04-29 | ✗ | | +| 90 | [fpvandoorn/carleson](https://github.com/fpvandoorn/carleson) | A formalized proof of Carleson's theorem in Lean | Apache-2.0 | v4.30.0-rc2 | 45,245 | 2026-04-29 | ✗ | | +| 87 | [morph-labs/lean-abc-true-almost-always](https://github.com/morph-labs/lean-abc-true-almost-always) | | | v4.20.0 | 3,602 | 2026-04-26 | – | | +| 85 | [thefundamentaltheor3m/SpherePacking](https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean) | A Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8. | Apache-2.0 | v4.29.0 | 23,020 | 2026-04-29 | ✗ | | +| 84 | [rzrn/GroundZero](https://github.com/rzrn/ground_zero) | Ground Zero: Lean 4 HoTT Library | Apache-2.0 | 4.28.0 | 19,200 | 2026-04-26 | ✗ | | +| 83 | [leanprover-community/ConNF](https://github.com/leanprover-community/con-nf) | A formal consistency proof of Quine's set theory New Foundations | Apache-2.0 | v4.21.0-rc3 | 41,728 | 2026-04-01 | ✗ | | +| 82 | [mo271/FormalBook](https://github.com/mo271/FormalBook) | Formalizing "Proofs from THE BOOK" | Apache-2.0 | v4.27.0-rc1 | 9,514 | 2026-04-08 | ✗ | | +| 79 | [YuanheZ/lean-stat-learning-theory](https://github.com/YuanheZ/lean-stat-learning-theory) | [ICML2026] The first comprehensive Lean 4 formalization of statistical learning theory, featuring Gaussian Lipschitz co… | | v4.27.0-rc1 | 34,893 | 2026-05-08 | – | | +| 78 | [fgdorais/Parser](https://github.com/fgdorais/lean4-parser) | Parser Combinator Library for Lean 4 | Apache-2.0 | v4.30.0-rc2 | 2,445 | 2026-04-21 | ✓ | | +| 77 | [risc0/risc0-lean4](https://github.com/risc0/risc0-lean4) | A model of the RISC Zero zkVM and ecosystem in the Lean 4 Theorem Prover | Apache-2.0 | nightly-2022-12-23 | 6,497 | 2026-03-13 | ✗ | | +| 76 | [teorth/estimate_tools](https://github.com/teorth/estimate_tools) | | | v4.20.0-rc5 | 3,794 | 2026-04-19 | – | | +| 76 | [YaelDillies/LeanCamCombi](https://github.com/YaelDillies/cam-combi) | Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Com… | Apache-2.0 | v4.29.0 | 1,346 | 2026-04-14 | ✗ | | +| 71 | [verified-optimization/CvxLean](https://github.com/verified-optimization/CvxLean) | Convex optimization modeling in Lean 4 | Apache-2.0 | v4.8.0-rc1 | 21,208 | 2026-04-28 | ✗ | | +| 70 | [NethermindEth/evmyul](https://github.com/NethermindEth/EVMYulLean) | Executable formal model of the EVM and Yul in Lean 4. | Apache-2.0 | v4.22.0 | 11,339 | 2026-03-29 | ✗ | | +| 68 | [starkware-libs/verification](https://github.com/starkware-libs/formal-proofs) | | Apache-2.0 | v4.13.0-rc3 | 66,896 | 2026-04-06 | ✗ | | +| 67 | [sinhp/hottlean](https://github.com/sinhp/HoTTLean) | | Apache-2.0 | v4.25.0-rc2 | 39,375 | 2026-04-26 | ✗ | | +| 66 | [harmonic-ai/IMO2025](https://github.com/harmonic-ai/IMO2025) | | | v4.20.0-rc5 | 5,302 | 2026-04-14 | – | | +| 66 | [math-inc/Sphere-Packing-Lean](https://github.com/math-inc/Sphere-Packing-Lean) | A Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8 a… | Apache-2.0 | v4.28.0 | 180,661 | 2026-05-08 | – | | +| 63 | [siddhartha-gadgil/saturn](https://github.com/siddhartha-gadgil/Saturn) | Experiments with SAT solvers with proofs in Lean 4 | MIT | v4.8.0 | 3,549 | 2025-12-19 | ✗ | | +| 62 | [leanprover-community/flt-regular](https://github.com/leanprover-community/flt-regular) | Fermat's Last Theorem for regular primes | Apache-2.0 | v4.30.0-rc2 | 5,199 | 2026-04-26 | ✓ | | +| 61 | [BoltonBailey/formalSnarksProject](https://github.com/BoltonBailey/formal-snarks-project) | A formal verification of Linear PCP SNARKs. | MIT | v4.10.0-rc2 | 6,219 | 2026-04-07 | ✗ | | +| 60 | [Verilean/sparkle](https://github.com/Verilean/sparkle) | A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis. | Apache-2.0 | v4.28.0 | 89,950 | 2026-04-26 | ✓ | | +| 59 | [vihdzp/CombinatorialGames](https://github.com/vihdzp/combinatorial-games) | Combinatorial game library in Lean 4 | Apache-2.0 | v4.30.0-rc2 | 17,744 | 2026-04-19 | ✗ | | +| 53 | [joehendrix/lean-crypto](https://github.com/joehendrix/lean-crypto) | Cryptographic routines for the Lean 4 language | Apache-2.0 | nightly-2023-04-20 | 3,812 | 2026-04-14 | ✗ | | +| 52 | [verse-lab/splean](https://github.com/verse-lab/splean) | Separation Logic Proofs in Lean | Apache-2.0 | v4.11.0 | 8,743 | 2026-04-06 | – | | +| 49 | [reilabs/proven-zk](https://github.com/reilabs/proven-zk) | A support library for working with zero knowledge cryptography in Lean 4. | Apache-2.0 | v4.21.0 | 1,249 | 2026-03-12 | ✗ | | +| 49 | [Timeroot/computableReal](https://github.com/Timeroot/ComputableReal) | computable implementation of real numbers in Lean4 | Apache-2.0 | v4.17.0-rc1 | 3,816 | 2026-04-17 | ✗ | | +| 48 | [ShangtongZhang/RL-Theory](https://github.com/ShangtongZhang/rl-theory-in-lean) | Towards Formalizing RL Theory | MIT | v4.28.0-rc1 | 10,208 | 2026-04-24 | ✗ | | +| 47 | [lean-dojo/problems](https://github.com/lean-dojo/LeanMillenniumPrizeProblems) | Formalization of the Millennium Problems in Lean 4 | Apache-2.0 | v4.26.0 | 5,558 | 2026-04-02 | ✗ | | +| 47 | [leanprover-community/SphereEversion](https://github.com/leanprover-community/sphere-eversion) | Formalization of the existence of sphere eversions | Apache-2.0 | v4.28.0 | 14,641 | 2026-03-30 | ✗ | | +| 47 | [RemyDegenne/BrownianMotion](https://github.com/RemyDegenne/brownian-motion) | Construction of a Brownian Motion in Lean | Apache-2.0 | v4.30.0-rc1 | 16,875 | 2026-04-22 | ✗ | | +| 45 | [opencompl/veir](https://github.com/opencompl/veir) | Verified Intermediate Representation | | nightly-2026-05-07 | 41,325 | 2026-05-09 | – | | +| 44 | [Ivan-Sergeyev/Seymour](https://github.com/Ivan-Sergeyev/seymour) | This project is about formally verifying Seymour's decomposition theorem for regular matroids. | Apache-2.0 | v4.18.0 | 9,042 | 2026-04-09 | ✗ | | +| 42 | [argumentcomputer/Wasm.lean](https://github.com/argumentcomputer/Wasm.lean) | A WebAssembly implementation in Lean4 | MIT | nightly-2023-01-10 | 4,616 | 2026-04-16 | ✗ | | +| 41 | [lengyijun/goldbach_tm](https://github.com/lengyijun/goldbach_tm) | Goldbach conjecture = 25-state turing machine | | v4.14.0-rc2 | 2,961 | 2026-04-25 | – | | +| 41 | [riccardobrasca/FLT3](https://github.com/riccardobrasca/flt3) | Proof in Lean of Fermat Last Theorem for exponent 3 | Apache-2.0 | v4.9.0-rc3 | 914 | 2026-02-26 | ✗ | | +| 40 | [AxiomMath/FelConjecture](https://github.com/AxiomMath/fel-polynomial) | Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups" | MIT | v4.26.0 | 2,710 | 2026-04-07 | ✗ | ✓ | +| 39 | [leanprover/TensorLib](https://github.com/leanprover/TensorLib) | A verified tensor library in Lean | Apache-2.0 | v4.23.0 | 5,347 | 2026-04-15 | ✗ | | +| 38 | [astrainfinita/algorithm](https://github.com/astrainfinita/Algorithm) | Verified efficient algorithms in Lean4. | Apache-2.0 | v4.27.0-rc1 | 5,490 | 2026-04-21 | ✗ | | +| 38 | [Verified-zkEVM/CompPoly](https://github.com/Verified-zkEVM/CompPoly) | A computable model of Polynomials in Lean. | Apache-2.0 | v4.29.1 | 36,432 | 2026-04-29 | ✗ | | +| 37 | [alerad/leancert](https://github.com/alerad/leancert) | Verified interval arithmetic for Lean 4 — prove bounds on exp, sin, cos, find roots, all machine-checked | Apache-2.0 | v4.28.0 | 75,256 | 2026-04-21 | – | | +| 37 | [project-numina/lib](https://github.com/project-numina/LeanGeo) | Solving Competition Geometry Problems in Lean | MIT | v4.15.0 | 12,011 | 2026-04-25 | ✗ | | +| 37 | [sgraf812/mpl](https://github.com/sgraf812/mpl) | A prototype for a monadic program logic in Lean that has since been upstreamed into the Lean 4 repo | Apache-2.0 | v4.21.0-rc3 #leanprover/lean4:nightly-2025-06-03 | 8,412 | 2025-10-18 | – | | +| 35 | [argumentcomputer/Megaparsec.lean](https://github.com/argumentcomputer/Megaparsec.lean) | Lean 4 port of Megaparsec | MIT | v4.0.0 | 2,291 | 2026-03-08 | ✗ | | +| 34 | [WuProver/groebner](https://github.com/WuProver/groebner_proj) | Formalization of Gröbner basis theory in Lean4 (WIP) | Apache-2.0 | v4.29.0-rc8 | 8,098 | 2026-04-14 | ✗ | | +| 33 | [model-checking/rust-lean-models](https://github.com/model-checking/rust-lean-models) | Lean models of Rust libraries | Apache-2.0 | v4.11.0 | 6,315 | 2026-04-23 | ✗ | | +| 33 | [optpku/ReasBook](https://github.com/optpku/ReasBook) | ReasBook main branch mirror for self-hosted CI | Apache-2.0 | | 275,519 | 2026-04-28 | – | | +| 33 | [vihdzp/Rubik](https://github.com/vihdzp/rubik-lean4) | Lean 4 formalization of Rubik's cubes | Apache-2.0 | v4.17.0-rc1 | 3,801 | 2026-04-13 | ✗ | | +| 32 | [haskell-spec/haskell-spec](https://github.com/haskell-spec/haskell-spec) | Formal specification of the Haskell Language Report | MIT | v4.22.0-rc4 | 4,076 | 2026-03-04 | ✓ | | +| 32 | [JamesGallicchio/leancolls](https://github.com/JamesGallicchio/LeanColls) | WIP collections library for Lean 4 | Apache-2.0 | v4.13.0 | 3,756 | 2025-05-08 | ✗ | | +| 32 | [marcusrossel/VerifiedCompiler](https://github.com/marcusrossel/verified-compiler) | A toy example of a verified compiler. | MIT | v4.29.0 | 347 | 2026-04-07 | ✓ | | +| 31 | [opencompl/sail-riscv-lean](https://github.com/opencompl/sail-riscv-lean) | | | v4.29.0 | 170,174 | 2026-05-09 | – | | +| 30 | [jjdishere/EG](https://github.com/jjdishere/EG) | Formalizing Euclidean Geometry in Lean | | v4.5.0-rc1 | 32,660 | 2025-12-30 | – | | +| 30 | [T-Brick/wasm](https://github.com/T-Brick/lean-wasm) | Formalising the WASM spec in Lean | GPL-3.0 | v4.25.0 | 7,005 | 2026-03-18 | ✗ | | +| 29 | [girving/ray](https://github.com/girving/ray) | Formalizing results about the Mandelbrot set in Lean | Apache-2.0 | v4.27.0-rc1 | 22,971 | 2026-02-17 | ✗ | | +| 29 | [scottnarmstrong/DeGiorgi](https://github.com/scottnarmstrong/DeGiorgi) | Lean 4 formalization of De Giorgi-Nash-Moser theory | Apache-2.0 | v4.29.0-rc6 | 56,283 | 2026-05-06 | – | | +| 28 | [GaloisInc/zkLeanEcosystem](https://github.com/GaloisInc/zkLean) | zkLean is a domain specific language (DSL) in Lean for specifying zero-knowledge statements | BSD-3-Clause | v4.25.2 | 4,048 | 2026-04-27 | ✓ | | +| 28 | [sinhp/Poly](https://github.com/sinhp/Poly) | A Lean4 Formalization of Polynomial Functors | | v4.27.0-rc1 | 6,453 | 2026-04-26 | – | | +| 27 | [MixedMatched/formalizing-game-theory](https://github.com/MixedMatched/formalizing-game-theory) | Example formalization of Game Theoretic concepts in Lean | | v4.17.0-rc1 | 1,304 | 2026-03-11 | – | | +| 26 | [lean-machines-central/lean-machines](https://github.com/lean-machines-central/lean-machines) | a Lean4 framework for the modeling and refinement of stateful systems | Apache-2.0 | v4.23.0-rc2 | 11,277 | 2026-03-30 | ✗ | | +| 26 | [merely-true/merely-true](https://github.com/merely-true/merely-true) | | Apache-2.0 | v4.29.0 | 11,252 | 2026-04-22 | – | | +| 25 | [girving/interval](https://github.com/girving/interval) | Conservative floating point interval arithmetic in Lean | Apache-2.0 | v4.27.0-rc1 | 15,731 | 2026-03-25 | ✗ | | +| 25 | [mortarsanjaya/IMOSLLean4](https://github.com/mortarsanjaya/IMOSLLean4) | Formalization of IMO shortlist problems in Lean 4 | Apache-2.0 | v4.30.0-rc2 | 38,524 | 2026-04-26 | ✓ | | +| 24 | [opencompl/C-parsing-for-Lean4](https://github.com/opencompl/C-parsing-for-Lean4) | A parser for ANSI C, in Lean4. | | Kha/lean4:vcustom-tokens | 2,682 | 2026-04-01 | – | | +| 23 | [ATOMSLab/LeanLJ](https://github.com/ATOMSLab/LeanLJ) | Lennard Jones in Lean | Apache-2.0 | v4.16.0-rc2 | 1,167 | 2026-04-29 | ✗ | | +| 23 | [digama0/mm-lean4](https://github.com/digama0/mm-lean4) | Lean 4 Metamath verifier | | v4.26.0-rc2 | 1,334 | 2026-02-20 | – | | +| 23 | [FormalSAT/trestle](https://github.com/FormalSAT/trestle) | | Apache-2.0 | v4.21.0 | 28,852 | 2026-03-25 | ✗ | | +| 23 | [math-inc/Erdos1196](https://github.com/math-inc/Erdos1196) | | Apache-2.0 | v4.30.0-rc1 | 4,035 | 2026-05-09 | – | | +| 22 | [opencompl/fp-lean](https://github.com/opencompl/fp-lean) | Floating Point Semantics Mechanization for Lean | Apache-2.0 | nightly-2026-01-14 | 17,616 | 2026-04-29 | ✗ | | +| 22 | [PeterKementzey/Graph](https://github.com/PeterKementzey/graph-library-for-lean4) | | MIT | v4.12.0 | 1,606 | 2026-01-02 | ✓ | | +| 22 | [VCA-EPFL/graphiti](https://github.com/VCA-EPFL/graphiti) | Verified graph rewriting (for dataflow circuits). | Apache-2.0 | v4.30.0-rc2 | 39,197 | 2026-04-29 | ✓ | | +| 22 | [YaelDillies/APAP](https://github.com/YaelDillies/apap) | Formalisation of the Kelley-Meka bound on Roth numbers | Apache-2.0 | v4.30.0-rc2 | 6,953 | 2026-04-27 | ✗ | | +| 21 | [frenzymath/Anderson-Conjecture](https://github.com/frenzymath/Anderson-Conjecture) | | Apache-2.0 | v4.29.0-rc8 | 19,482 | 2026-05-07 | – | | +| 21 | [logical-intelligence/Putnam](https://github.com/logical-intelligence/proofs) | | MIT | v4.26.0-rc2 | 8,857 | 2026-03-17 | ✗ | | +| 21 | [Luka-O/polya-enumeration-theorem](https://github.com/Luka-O/polya-enumeration-theorem) | A Lean 4 formalization of Pólya enumeration theorem. | MIT | v4.14.0-rc2 | 1,419 | 2025-09-11 | ✗ | | +| 20 | [b-mehta/ABCExceptions](https://github.com/b-mehta/ABC-Exceptions) | Exceptions to the ABC conjecture in Lean | Apache-2.0 | v4.21.0-rc3 | 3,353 | 2026-04-03 | ✗ | | +| 20 | [bergmannjg/Regex](https://github.com/bergmannjg/regex) | A PCRE2 compatible regular expression engine written in Lean 4. | MIT | v4.29.0 | 13,692 | 2026-04-27 | ✗ | | +| 20 | [ctchou/AutomataTheory](https://github.com/ctchou/AutomataTheory) | Automata theory in Lean | Apache-2.0 | v4.24.0-rc1 | 5,258 | 2026-04-17 | ✗ | | +| 20 | [JulsDE/MRiscX](https://github.com/JulsDE/MRiscX) | A certified RISC-V Interpreter with Hoare-logic in Lean | Apache-2.0 | v4.29.0 | 7,350 | 2026-04-29 | ✗ | | +| 20 | [provables/sequencelib](https://github.com/provables/sequencelib) | A platform for formalizing OEIS sequences in Lean 4 | CC-BY-SA-4.0 | v4.28.0 | 857,034 | 2026-05-08 | – | | +| 19 | [math-inc/KakeyaFiniteFields](https://github.com/math-inc/KakeyaFiniteFields) | A complete Lean 4 formalization of the Kakeya set problem over finite fields | | v4.26.0-rc2 | 315 | 2026-04-13 | – | | +| 19 | [quangvdao/Zklib](https://github.com/quangvdao/ZKLib-deprecated) | deprecated, use Verified-zkEVM repository instead | Apache-2.0 | | | 2025-04-14 | ✗ | | +| 18 | [codyroux/traat](https://github.com/codyroux/traat-lean) | Lean formalization of selected lemmas from "Term Rewriting and All That" | MIT | v4.30.0-rc1 | 3,897 | 2026-04-20 | ✓ | | +| 18 | [katydid/regexderiv](https://github.com/katydid/regex-deriv-lean) | Proofs written in Lean4 for the core katydid validation algorithm | Apache-2.0 | v4.22.0 | 7,622 | 2026-02-19 | ✗ | | +| 18 | [verse-lab/Lentil](https://github.com/verse-lab/Lentil) | (at least a useful portion of) Temporal Logic of Actions, a.k.a. TLA in Lean 4 | Apache-2.0 | v4.27.0 | 1,696 | 2026-04-22 | – | | +| 17 | [658060/topos](https://github.com/658060/topos) | Topos theory in Lean 4 | | v4.15.0 | 1,571 | 2026-02-20 | – | | +| 17 | [auto-res/FoML](https://github.com/auto-res/lean-rademacher) | Lean Formalization of Generalization Error Bound by Rademacher Complexity | MIT | v4.27.0-rc1 | 8,490 | 2026-04-28 | ✗ | | +| 17 | [dwrensha/rupert](https://github.com/dwrensha/Rupert.lean) | Formalization of the Rupert Problem for convex polyhedra. | Apache-2.0 | v4.28.0 | 1,713 | 2026-04-05 | ✗ | | +| 17 | [ElifUskuplu/stlc](https://github.com/ElifUskuplu/Stlc_deBruijn) | Simply Typed Lambda Calculus with de Bruijn indices | MIT | v4.16.0-rc2 | 2,806 | 2026-03-03 | ✗ | | +| 17 | [kovach/etch](https://github.com/kovach/etch) | | Apache-2.0 | v4.7.0 | 11,504 | 2026-04-11 | ✗ | | +| 17 | [leanprover-community/add-combi](https://github.com/leanprover-community/add-combi) | The sublibrary of Mathlib dedicated to additive combinatorics | Apache-2.0 | v4.30.0-rc2 | 1,474 | 2026-05-07 | – | | +| 17 | [mrdouglasny/OSforGFF](https://github.com/mrdouglasny/OSforGFF) | A Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms | Apache-2.0 | v4.29.0 | 31,054 | 2026-04-29 | ✗ | | +| 17 | [UCSCFormalMethods/LeanLTL](https://github.com/UCSCFormalMethods/LeanLTL) | A unifying framework for linear temporal logics in Lean | | v4.17.0-rc1 | 4,408 | 2026-04-12 | – | | +| 17 | [Vilin97/Clawristotle](https://github.com/Vilin97/Clawristotle) | OpenClaw-style theorem proving | | v4.24.0 | 10,760 | 2026-04-28 | – | | +| 16 | [leodemoura/RadixExperiment](https://github.com/leodemoura/RadixExperiment) | | | v4.29.0-rc1 | 6,330 | 2026-04-29 | – | | +| 16 | [m4lvin/pdl](https://github.com/m4lvin/lean4-pdl) | Tableaux for Propositional Dynamic Logic in Lean 4 (WORK IN PROGRESS) | Apache-2.0 | v4.28.0 | 24,200 | 2026-04-29 | ✗ | | +| 16 | [NethermindEth/plonky3-example](https://github.com/NethermindEth/CertiPlonk) | A framework for extracting and formally verifying constraint systems from the Plonky3 zkDSL in Lean. | Apache-2.0 | v4.23.0-rc2 | 903 | 2026-04-20 | ✗ | | +| 16 | [RemyDegenne/clt](https://github.com/RemyDegenne/CLT) | Central limit theorem in Lean | Apache-2.0 | v4.29.0-rc3 | 533 | 2026-03-19 | ✗ | | +| 15 | [aetilley/banach-tarski](https://github.com/aetilley/banach-tarski) | A formalization of the Banach-Tarski theorem in Lean | Apache-2.0 | v4.25.0 | 8,799 | 2026-05-01 | – | | +| 15 | [apnelson1/Matroid](https://github.com/apnelson1/Matroid) | | Apache-2.0 | v4.30.0-rc2 | 123,512 | 2026-04-29 | ✗ | | +| 15 | [artie2000/real-closed-field](https://github.com/artie2000/real_closed_field) | Formalisation of the theory of real closed fields in Lean 4. | Apache-2.0 | v4.30.0-rc1 | 7,956 | 2026-04-22 | ✗ | | +| 15 | [frenzymath/Archon-FirstProof-Results](https://github.com/frenzymath/Archon-FirstProof-Results) | | Apache-2.0 | v4.28.0 | 11,944 | 2026-04-11 | – | | +| 15 | [jsm28/AM](https://github.com/jsm28/AperiodicMonotilesLean) | Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib) | Apache-2.0 | v4.30.0-rc2 | 2,817 | 2026-04-18 | ✓ | | +| 15 | [Kha/do-supplement](https://github.com/Kha/do-supplement) | Supplement of the ICFP'22 paper "‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language" | | v4.15.0 | 1,289 | 2026-05-02 | – | | +| 14 | [acmepjz/Iwasawalib](https://github.com/acmepjz/lean-iwasawa) | Formalization of Iwasawa Theory in LꓱꓯN (tentative) | Apache-2.0 | v4.30.0-rc1 | 9,535 | 2026-04-29 | ✓ | | +| 14 | [ammkrn/timelib](https://github.com/ammkrn/timelib) | A date and time library for Lean 4 | Apache-2.0 | v4.19.0-rc2 | 5,639 | 2026-01-30 | ✗ | | +| 14 | [andrejbauer/partial-combinatory-algebras](https://github.com/andrejbauer/partial-combinatory-algebras) | A Lean 4 formalization of partial combinatory algebras. | MIT | v4.15.0-rc1 | 1,270 | 2025-06-23 | ✗ | | +| 14 | [FormalizedFormalLogic/arithmetization](https://github.com/FormalizedFormalLogic/Arithmetization) | Formalization of Arithmetization of Mathematics/Metamathematics | Apache-2.0 | v4.17.0-rc1 | 18,501 | 2026-04-08 | ✗ | | +| 14 | [iasakura/lean-yjs](https://github.com/iasakura/lean-yjs) | Lean-Yjs: Formal Verification of Yjs Integration Algorithm | MIT | v4.26.0-rc2 | 13,241 | 2026-04-27 | ✗ | | +| 14 | [jcreedcmu/Noperthedron](https://github.com/jcreedcmu/Noperthedron) | The Noperthedron does not have Rupert Property: a proof in Lean4 | Apache-2.0 | v4.30.0-rc2 | 13,792 | 2026-04-28 | ✓ | | +| 14 | [sven-manthe/borel_det](https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean) | | Apache-2.0 | v4.28.0-rc1 | 8,277 | 2026-02-26 | ✗ | | +| 13 | [AviCraimer/relational-calculus-library-lean4](https://github.com/AviCraimer/relational-calculus-library-lean4) | | | v4.12.0-rc1 | 1,947 | 2026-05-04 | – | | +| 13 | [eshelyaron/bdd](https://github.com/eshelyaron/lean4-bdd) | Binary Decision Diagrams in Lean 4 | Apache-2.0 | v4.27.0 | 8,155 | 2026-03-17 | ✗ | | +| 13 | [facebookresearch/algebraic-combinatorics](https://github.com/facebookresearch/algebraic-combinatorics) | Automatic textbook formalization of Grinberg Algebraic Combinatorics | | v4.28.0 | 130,245 | 2026-05-05 | – | | +| 13 | [girving/ray-series](https://github.com/girving/series) | Power series arithmetic in Lean | Apache-2.0 | v4.26.0-rc2 | 3,808 | 2025-12-19 | ✗ | | +| 13 | [kbuzzard/ClassFieldTheory](https://github.com/kbuzzard/ClassFieldTheory) | Github repository for the 2025 Clay Summer School on Formalizing Class Field Theory | Apache-2.0 | v4.29.0 | 12,246 | 2026-04-11 | ✗ | | +| 13 | [knowsys/certifyingDatalog](https://github.com/knowsys/CertifyingDatalog) | A certified checker for Datalog entailments, written in Lean | Apache-2.0 | v4.29.0 | 6,124 | 2026-04-01 | ✗ | | +| 13 | [NUS-Math-Formalization/coxeter](https://github.com/NUS-Math-Formalization/coxeter) | | | v4.7.0 | 8,290 | 2025-07-28 | – | | +| 13 | [RemyDegenne/testing_lower_bounds](https://github.com/RemyDegenne/testing-lower-bounds) | Information theory and hypothesis testing, in Lean | Apache-2.0 | v4.13.0-rc3 | 13,201 | 2026-04-15 | ✗ | | +| 12 | [ah1112/synthetic_euclid_4](https://github.com/ah1112/synthetic_euclid_4) | | Apache-2.0 | | 2,993 | 2026-02-16 | ✗ | | +| 12 | [b-mehta/AharoniKorman](https://github.com/b-mehta/AharoniKorman) | Disproof of the Aharoni–Korman conjecture | Apache-2.0 | v4.16.0-rc2 | 1,288 | 2025-12-01 | ✗ | | +| 12 | [Bergschaf/banach_tarski](https://github.com/Bergschaf/banach-tarski) | | Apache-2.0 | v4.10.0-rc2 | 1,624 | 2026-01-19 | ✗ | | +| 12 | [fpvandoorn/bonnAnalysis](https://github.com/fpvandoorn/BonnAnalysis) | repository for the collaborative formalization seminar in Analysis in Bonn | Apache-2.0 | v4.10.0-rc1 | 5,604 | 2026-04-01 | ✗ | | +| 12 | [kim-em/KnuthClaudeLean](https://github.com/kim-em/KnuthClaudeLean) | Lean 4 formalization of Knuth's 'Claude's Cycles' paper | | v4.28.0 | 1,818 | 2026-05-07 | – | | +| 12 | [math-xmum/Brouwer](https://github.com/math-xmum/Brouwer) | This repo is about the proof of the Nash Equilibrium through Scarf and Brouwer by Mathlib. | MIT | v4.22.0 | 4,790 | 2026-05-04 | – | | +| 12 | [mit-plv/lean4-itree](https://github.com/mit-plv/lean4-itree) | Coinductive Interaction Trees in Lean4 using QPFs | MIT | v4.29.0 | 1,123 | 2026-05-07 | – | | +| 12 | [NethermindEth/risczero-fv](https://github.com/NethermindEth/risczero-fv) | | Apache-2.0 | nightly-2023-06-10 | 49,206 | 2026-03-29 | ✗ | | +| 12 | [YaelDillies/Toric](https://github.com/YaelDillies/toric) | Formalisation of toric varieties in Lean 4 | Apache-2.0 | v4.30.0-rc1 | 3,591 | 2026-04-12 | ✗ | | +| 12 | [YnirPaz/PCF](https://github.com/YnirPaz/PCF-Theory) | A formalization of PCF theory in lean | MIT | v4.18.0-rc1 | 1,193 | 2026-02-24 | ✗ | | +| 11 | [AfonsoBitoque/LeanServer](https://github.com/AfonsoBitoque/LeanServer) | Verified HTTPS server in Lean 4 — TLS 1.3, HTTP/2, QUIC, WebSocket, gRPC — 914 machine-checked theorems, zero sorry. Pu… | Apache-2.0 | v4.27.0 | 38,581 | 2026-04-21 | ✗ | | +| 11 | [amarmaduke/lean-subst](https://github.com/amarmaduke/lean-subst) | Lean4 library for substitution inspired by autosubst | MIT | v4.29.0 | 2,279 | 2026-04-22 | ✓ | | +| 11 | [AxiomMath/Deadends](https://github.com/AxiomMath/dead-ends) | | MIT | v4.26.0 | 4,260 | 2026-04-02 | ✗ | | +| 11 | [AxiomMath/lattice-triangle](https://github.com/AxiomMath/lattice-triangle) | Lean formalizations for the paper "On the paucity of lattice triangles" | MIT | v4.26.0 | 9,978 | 2026-04-07 | – | | +| 11 | [ecyrbe/lean-units](https://github.com/ecyrbe/lean-units) | lean physical unit system, SI international | MIT | v4.24.0 | 4,166 | 2026-01-10 | ✗ | | +| 11 | [GasStationManager/ArtificialAlgorithms](https://github.com/GasStationManager/ArtificialAlgorithms) | Verified algorithms in Lean, implemented and proved by AIs | Apache-2.0 | v4.27.0 | 26,419 | 2026-04-28 | ✗ | | +| 11 | [imbrem/DeBruijnSSA](https://github.com/imbrem/debruijn-ssa) | A formalization of SSA in Lean 4 | 0BSD | v4.15.0-rc1 | 29,307 | 2025-12-14 | ✗ | | +| 11 | [Izzimach/pteffects](https://github.com/Izzimach/EffSpec-lean) | Effect monads with specifications (DIjkstra Monads) in Lean 4 | MIT | v4.3.0 | 1,393 | 2025-06-19 | ✗ | | +| 11 | [leanprover/leanbv](https://github.com/leanprover/leanbv) | | Apache-2.0 | | | 2024-06-03 | ✗ | | +| 11 | [matthunz/circuitlib](https://github.com/matthunz/circuitlib) | A digital circuit verification library for Lean4 | Apache-2.0 | v4.30.0-rc1 | 2,359 | 2026-04-27 | – | | +| 11 | [NyxFoundation/TopSingleLayer](https://github.com/NyxFoundation/tsl-formal-verification) | Formal Verification of Top Single Layer Encoding | MIT | v4.24.0-rc1 | 987 | 2026-03-25 | ✗ | | +| 11 | [Verified-zkEVM/EvmAsm](https://github.com/Verified-zkEVM/evm-asm) | | MIT | v4.30.0-rc1 | 172,772 | 2026-04-29 | ✓ | | +| 11 | [WuProver/MonomialOrderedPolynomial](https://github.com/WuProver/MonomialOrderedPolynomial) | Monomial ordered polynomial implementation in Lean4 | Apache-2.0 | v4.29.0-rc8 | 4,816 | 2026-04-10 | ✗ | | +| 11 | [Zetetic-Dhruv/formal-learning-theory-kernel](https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel) | Lean4 kernel for synthetic formalization and discovery of statistical learning theory. First and complete formalization… | | v4.29.0-rc6 | 23,679 | 2026-04-29 | – | | +| 11 | [znssong/SetTheory](https://github.com/znssong/SetTheory) | A formalization project of set theory and elementary embeddings in Lean 4. Includes a proof of Kunen's inconsistency th… | Apache-2.0 | v4.29.0-rc4 | 2,859 | 2026-04-20 | – | | +| 10 | [Beneficial-AI-Foundation/Curve25519Dalek](https://github.com/Beneficial-AI-Foundation/curve25519-dalek-lean-verify) | Verifying curve25519-dalek using Lean | Apache-2.0 | v4.28.0-rc1 | 50,007 | 2026-04-29 | ✗ | | +| 10 | [Brunn-Minkowski-in-Lean/BrunnMinkowski](https://github.com/Brunn-Minkowski-in-Lean/BrunnMinkowski) | | | v4.19.0-rc2 | 1,731 | 2026-02-11 | – | | +| 10 | [calcu16/lean_complexity](https://github.com/calcu16/lean_complexity) | Complexity analysis in Lean | | v4.5.0-rc1 | 5,595 | 2025-02-04 | – | | +| 10 | [DavePearce/LeanEVM](https://github.com/DavePearce/LeanEVM) | A toy implementation of the EVM in Lean4. | Apache-2.0 | v4.8.0-rc2 | 818 | 2024-05-29 | ✗ | | +| 10 | [gdncc/cryptography](https://github.com/gdncc/Cryptography) | Lean 4 programming language and theorem prover cryptography experiments | MIT | v4.27.0 | 1,300 | 2026-02-13 | ✓ | | +| 10 | [ianjauslin-rutgers/pythagoras4](https://github.com/ianjauslin-rutgers/pythagoras4) | Many proofs of the Pythagoras theorem - Lean 4 | | nightly-2023-05-16 | 2,118 | 2026-01-09 | – | | +| 10 | [katydid/sadol](https://github.com/katydid/regex-deriv-reproving-agda-in-lean) | Symbolic and Automatic Differentiation of Languages in Lean | Apache-2.0 | v4.14.0 | 1,231 | 2025-05-09 | ✓ | | +| 10 | [kebekus/VD](https://github.com/kebekus/ProjectVD) | Formalizing Value Distribution Theory | Apache-2.0 | v4.30.0-rc2 | 1,885 | 2026-04-29 | ✓ | | +| 10 | [knowsys/FormaleSystemeInLean](https://github.com/knowsys/Formale-Systeme-in-LEAN) | LEAN4 formalization of the undergraduate lecture "Formale Systeme" at TU Dresden (WIP) | Apache-2.0 | v4.28.0 | 8,973 | 2026-03-26 | ✗ | | +| 10 | [leanprover/LeroyCompilerVerificationCourse](https://github.com/leanprover/LeroyCompilerVerificationCourse) | | LGPL-2.1 | v4.23.0-rc2 | 3,189 | 2025-11-06 | ✗ | | +| 10 | [NethermindEth/CompPoly](https://github.com/NethermindEth/CompPoly) | | Apache-2.0 | v4.22.0-rc2 | 1,296 | 2026-04-20 | ✗ | | +| 10 | [NethermindEth/FVIntmax](https://github.com/NethermindEth/FVIntmax) | Formal verification of the Intmax protocol in Lean. | Apache-2.0 | v4.14.0-rc2 | 5,301 | 2026-03-17 | ✗ | | +| 10 | [RemyDegenne/kolmogorov_extension4](https://github.com/RemyDegenne/kolmogorov_extension4) | Lean formalization of the Kolmogorov extension theorem | Apache-2.0 | v4.30.0-rc1 | 635 | 2026-04-08 | ✓ | | +| 10 | [ruplet/formalization-of-bounded-arithmetic](https://github.com/ruplet/formalization-of-bounded-arithmetic) | | MIT | v4.22.0 | 6,612 | 2026-04-10 | – | | +| 10 | [teorth/asymptotic](https://github.com/teorth/asymptotic) | | | v4.5.0-rc1 | 1,469 | 2026-03-15 | – | | +| 10 | [urkud/DeRhamCohomology](https://github.com/urkud/DeRhamCohomology) | Formalization of de Rham cohomologies of a smooth manifold | | v4.21.0-rc2 | 2,159 | 2026-05-09 | – | | +| 10 | [YaelDillies/AddCombi](https://github.com/YaelDillies/add-combi) | The (currently unofficial) sublibrary of Mathlib dedicated to additive combinatorics | Apache-2.0 | v4.30.0-rc2 | 1,474 | 2026-04-29 | ✗ | | +| 10 | [YaelDillies/gibbs-measure](https://github.com/YaelDillies/gibbs-measure) | ASCI Summer Research Lean | Apache-2.0 | v4.29.0 | 1,298 | 2026-04-05 | – | | +| 10 | [YellPika/quasi-borel-spaces](https://github.com/YellPika/quasi-borel-spaces) | A formalization of Quasi-Borel Spaces in Lean 4 | MIT | v4.28.0-rc1 | 8,626 | 2026-04-10 | ✗ | | +| 9 | [ahhwuhu/Zeta3Irrational](https://github.com/ahhwuhu/zeta_3_irrational) | | Apache-2.0 | v4.18.0 | 4,157 | 2026-03-20 | ✗ | | +| 9 | [AxiomMath/ramanujan-tau-misses-primes](https://github.com/AxiomMath/ramanujan-tau-misses-primes) | Lean formalizations for the paper "ABC implies that Ramanujan's Tau function misses almost all primes" | MIT | v4.26.0 | 5,772 | 2026-04-23 | – | | +| 9 | [b-mehta/PrimeCert](https://github.com/b-mehta/PrimeCert) | Formal prime certificates in Lean 4 | MIT | v4.29.1 | 1,949 | 2026-04-29 | – | | +| 9 | [Beneficial-AI-Foundation/FloatSpec](https://github.com/Beneficial-AI-Foundation/FloatSpec) | Formally Verified Float Implementation with lean4 | Apache-2.0 | v4.29.0 | 70,827 | 2026-04-24 | ✗ | | +| 9 | [cameronfreer/exchangeability](https://github.com/cameronfreer/exchangeability) | Formalization of exchangeability and three proofs of de Finetti's theorem in Lean 4, following Probabilistic Symmetries… | Apache-2.0 | v4.27.0-rc1 | 43,823 | 2026-04-19 | ✗ | | +| 9 | [goens/lost-pop-lean](https://github.com/goens/lost-pop-lean) | POP Memory Model in Lean | MIT | v4.30.0-rc2 | 5,784 | 2026-04-20 | ✓ | | +| 9 | [Hagb/lean-groebner](https://github.com/Hagb/lean-groebner) | Lean4 formalization of Gröbner basis (WIP) | Apache-2.0 | nightly-2023-06-10 | 2,497 | 2025-07-28 | ✗ | | +| 9 | [jthulhu/2ltt](https://github.com/jthulhu/2ltt) | | | v4.10.0-rc1 | 6,746 | 2026-05-01 | – | | +| 9 | [LeanMachineLearning/LeanMachineLearning](https://github.com/LeanMachineLearning/LML) | The Lean Machine Learning Library | Apache-2.0 | v4.29.0 | 10,125 | 2026-04-27 | ✗ | | +| 9 | [LieLean/Lie](https://github.com/LieLean/LowDimSolvClassification) | A classification theorem in Lean of solvable Lie algebras of dimension zero to three | Apache-2.0 | v4.19.0 | 5,595 | 2025-10-09 | ✗ | | +| 9 | [madvorak/chomsky](https://github.com/madvorak/chomsky) | Port https://github.com/madvorak/grammars/ to Lean 4 | BSD-2-Clause | v4.18.0 | 5,760 | 2026-04-09 | ✗ | | +| 9 | [madvorak/duality](https://github.com/madvorak/duality) | Duality theory in linear optimization and its extensions | Apache-2.0 | v4.18.0 | 2,582 | 2026-02-26 | ✗ | | +| 9 | [madvorak/vcsp](https://github.com/madvorak/vcsp) | General-Valued Constraint Satisfaction Problems | Apache-2.0 | v4.18.0 | 1,050 | 2026-02-26 | ✗ | | +| 9 | [MichaelStollBayreuth/EulerProducts](https://github.com/MichaelStollBayreuth/EulerProducts) | An attempt at formalizing facts on Euler products in Lean | GPL-2.0 | v4.24.0 | 472 | 2026-04-10 | ✗ | | +| 9 | [oliver-butterley/SpectralThm](https://github.com/oliver-butterley/SpectralThm) | Ongoing project to formalise The Spectral Theorem in Lean prover | Apache-2.0 | v4.30.0-rc2 | 1,524 | 2026-04-16 | ✗ | | +| 9 | [or4nge19/NeuralNetworks](https://github.com/or4nge19/NeuralNetworks) | Formalization of Neural Networks in Lean 4 | Apache-2.0 | v4.24.0-rc1 | 31,666 | 2026-02-12 | ✗ | | +| 9 | [powdr-labs/leanr](https://github.com/powdr-labs/leanr) | | MIT | v4.30.0-rc1 | 3,810 | 2026-04-09 | ✓ | | +| 9 | [SamuelSchlesinger/shannon-entropy](https://github.com/SamuelSchlesinger/shannon-1948-formalization) | A formalization of Shannon's seminal 1948 paper defining entropy. | MIT | v4.28.0 | 1,912 | 2026-04-11 | ✗ | | +| 9 | [seewoo5/lean-poly-abc](https://github.com/seewoo5/lean-poly-abc) | Formalization of the proof of ABC conjecture for polynomials (Mason-Stothers theorem) in Lean 4 | | v4.9.0-rc2 | 1,290 | 2026-03-04 | – | | +| 9 | [smorel394/TS1](https://github.com/smorel394/TS1) | | | nightly-2023-07-12 | 12,727 | 2023-09-01 | – | | +| 9 | [staroperator/mathematical-logic-in-lean](https://github.com/staroperator/mathematical-logic-in-lean) | Mathematical Logic in Lean | | v4.23.0-rc2 | 13,956 | 2026-03-22 | – | | +| 9 | [tannerduve/computability](https://github.com/tannerduve/computability) | A Lean formalization of the theory of oracle computability and Turing degrees via partial recursive functions | | v4.24.0 | 3,035 | 2026-02-05 | – | | +| 8 | [alainchmt/RingOfIntegersProject](https://github.com/alainchmt/RingOfIntegersProject) | Certifying rings of integers in number fields with Lean | Apache-2.0 | v4.14.0-rc2 | 93,799 | 2026-03-20 | – | | +| 8 | [chrisflav/proetale](https://github.com/chrisflav/proetale) | Proétale cohomology in Lean | Apache-2.0 | v4.30.0-rc2 | 10,400 | 2026-04-28 | ✓ | | +| 8 | [Clap-lang/clap](https://github.com/Clap-lang/clap-lean) | Implementation of the Clap language for ZK Circuits in the Lean proof-assistant | Apache-2.0 | v4.29.0 | 59,183 | 2026-04-29 | ✗ | | +| 8 | [FormalizedFormalLogic/incompleteness](https://github.com/FormalizedFormalLogic/Incompleteness) | Formalize Incompleness Theorem Related Results | Apache-2.0 | v4.16.0-rc2 | 2,514 | 2025-09-23 | ✗ | | +| 8 | [FredRaj3/SemicircleLaw](https://github.com/FredRaj3/SemicircleLaw) | Formalization of Wigner's Semicircle Law in Lean | MIT | v4.24.0 | 3,174 | 2026-04-11 | ✗ | | +| 8 | [GasStationManager/ArtificialTheorems](https://github.com/GasStationManager/ArtificialTheorems) | AI-assisted formalizations of machine learning theory | | v4.27.0 | 12,858 | 2026-04-30 | – | | +| 8 | [joelriou/topcat-model-category](https://github.com/joelriou/topcat-model-category) | | | v4.25.0-rc2 | 42,295 | 2026-04-18 | – | | +| 8 | [jonhanke/quadratic_forms_in_lean](https://github.com/jonhanke/quadratic_forms_in_lean) | | | v4.19.0-rc3 | 2,113 | 2025-09-07 | – | | +| 8 | [josephmckinsey/flean](https://github.com/josephmckinsey/Flean) | Floating point numbers in lean. A replacement of Mathlib.Data.FP | Apache-2.0 | v4.27.0-rc1 | 2,587 | 2026-04-07 | ✗ | | +| 8 | [lecopivo/leanblas](https://github.com/lecopivo/LeanBLAS) | Bindings and specification for BLAS | Apache-2.0 | v4.28.0-rc1 | 2,674 | 2026-02-12 | ✗ | | +| 8 | [math-xmum/GameTheory](https://github.com/math-xmum/gametheory) | | Apache-2.0 | v4.24.0-rc1 | 11,547 | 2026-04-20 | ✗ | | +| 8 | [Mathias-Stout/Many-sorted-model-theory](https://github.com/Mathias-Stout/Many-sorted-model-theory) | A lean repository for building many-sorted logic, with a view towards model theory of valued fields | Apache-2.0 | v4.30.0-rc2 | 24,442 | 2026-04-20 | – | | +| 8 | [mtoohey31/tabular-types](https://github.com/mtoohey31/tabular-types) | Proofs for Extensible Data Types with Ad-Hoc Polymorphism | Apache-2.0 | v4.17.0 | 24,678 | 2026-01-13 | ✗ | | +| 8 | [siddhartha-gadgil/Polylean](https://github.com/siddhartha-gadgil/Polylean) | | Apache-2.0 | v4.19.0-rc3 | 5,102 | 2025-06-02 | ✗ | | +| 8 | [sivukhin/sqlite3-lean-proofs](https://github.com/sivukhin/sqlite3-lean-proofs) | | | v4.25.0 | 16,191 | 2026-04-25 | – | | +| 8 | [Timeroot/CircuitComp](https://github.com/Timeroot/CircuitComp) | Circuit complexity in Lean | | v4.28.0 | 9,668 | 2026-04-23 | – | | +| 8 | [vasnesterov/HadwigerNelson](https://github.com/vasnesterov/HadwigerNelson) | Hadwiger-Nelson Problem Formalization in Lean 4 | Apache-2.0 | nightly-2024-07-11 | 814 | 2024-12-09 | ✗ | | +| 8 | [vihdzp/ordinal-notation](https://github.com/vihdzp/ordinal-notation) | Ordinal notations in Lean | | v4.16.0-rc2 | 6,161 | 2025-07-20 | – | | +| 8 | [z-tech/sumcheck-lean4](https://github.com/z-tech/sumcheck-lean4) | | Apache-2.0 | v4.28.0 | 6,219 | 2026-05-05 | – | | +| 7 | [adamtopaz/CopenhagenMasterclass2023](https://github.com/adamtopaz/CopenhagenMasterclass2023) | | | nightly-2023-06-10 | 5,349 | 2025-05-17 | – | | +| 7 | [bkase/VerifiedGPU](https://github.com/bkase/verified-gpu) | | MIT | v4.25.0-rc2 | 3,755 | 2025-12-25 | ✓ | | +| 7 | [CBirkbeck/LeanBridge](https://github.com/CBirkbeck/LeanBridge) | Link LMFDB and Lean | Apache-2.0 | v4.23.0 | 3,272 | 2026-03-23 | – | | +| 7 | [fplaunchpad/sal](https://github.com/fplaunchpad/sal) | Multimodal verification of Replicated Data Types in Lean | MIT | v4.28.0 | 24,962 | 2026-04-29 | ✗ | | +| 7 | [hanwenzhu/MillerRabin](https://github.com/hanwenzhu/miller-rabin) | Miller–Rabin primality test in Lean | Apache-2.0 | v4.22.0 | 1,289 | 2026-04-27 | ✗ | | +| 7 | [haskell-spec/veriflex](https://github.com/haskell-spec/veriflex) | Verified lexer for Lean 4 | MIT | v4.21.0 | 1,226 | 2026-01-24 | – | | +| 7 | [hawkrobe/linglib](https://github.com/hawkrobe/linglib) | A Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formali… | Apache-2.0 | v4.30.0-rc2 | 873,929 | 2026-04-29 | ✗ | | +| 7 | [ISTA-PLV/Coinductive](https://github.com/ISTA-PLV/coinductive) | Co-inductive datatypes for Lean | BSD-3-Clause | v4.29.0 | 3,905 | 2026-04-29 | ✓ | | +| 7 | [katjabercic/Lean-HoG](https://github.com/katjabercic/Lean-HoG) | | BSD-2-Clause | v4.6.0 | 4,793 | 2025-12-04 | – | | +| 7 | [KunhongDu/HoTT-Model](https://github.com/KunhongDu/HoTT-Model) | | | v4.14.0-rc2 | 22,601 | 2026-02-12 | – | | +| 7 | [kyoDralliam/model-theory-topos](https://github.com/kyoDralliam/model-theory-topos) | First order model theory inside a topos in Lean | | v4.22.0-rc3 | 9,409 | 2026-01-29 | – | | +| 7 | [mkaratarakis/HopfieldNet](https://github.com/mkaratarakis/HopfieldNet) | | MIT | v4.27.0-rc1 | 149,180 | 2026-02-10 | ✗ | | +| 7 | [mseri/BET](https://github.com/mseri/BET) | Project for "Machine-Checked Mathematics" at the Lorentz Center | Apache-2.0 | v4.30.0-rc2 | 5,086 | 2026-04-28 | ✓ | | +| 7 | [objectionary/phi-calculus](https://github.com/objectionary/proof) | Proof of 𝜑-calculus confluence | MIT | v4.15.0-rc1 | 6,543 | 2026-04-29 | ✗ | | +| 7 | [Paul-Lez/Stacks-project](https://github.com/Paul-Lez/Stacks-project) | Formalizing Fibered Categories and Stacks in Lean | | v4.24.0-rc1 | 6,119 | 2025-12-30 | – | | +| 7 | [Rob23oba/lean4-no-axioms](https://github.com/Rob23oba/lean4-no-axioms) | Lean 4 without any axioms | | v4.27.0 | 7,738 | 2026-03-09 | – | | +| 7 | [scholzhannah/CWComplexes](https://github.com/scholzhannah/CWComplexes) | In this repository I am collecting the code of my formalisation of CW complexes in Lean. | | v4.30.0-rc1 | 7,012 | 2026-04-17 | – | | +| 7 | [T-Brick/controlflow](https://github.com/T-Brick/ControlFlow) | A control flow graph library for Lean | GPL-3.0 | v4.25.0 | 5,329 | 2025-11-17 | ✓ | | +| 7 | [taeyool/lean-flag-algebras](https://github.com/taeyool/lean-flag-algebras) | | | v4.27.0 | 30,605 | 2026-05-09 | – | | +| 7 | [Timeroot/lean-descartes-signs](https://github.com/Timeroot/lean-descartes-signs) | Lean 4 proof of Descartes' Rule of Signs | | v4.3.0-rc2 | 1,475 | 2025-09-04 | – | | +| 7 | [weiran-sun/PDE](https://github.com/weiran-sun/pde) | PDE Lean formalization | Apache-2.0 | v4.27.0 | 3,335 | 2026-04-29 | ✗ | | +| 7 | [Whysoserioushah/BrauerGroup_new](https://github.com/Whysoserioushah/BrauerGroup_new) | | Apache-2.0 | v4.26.0-rc2 | 14,855 | 2026-03-20 | – | | +| 6 | [anoma/juvix-lean](https://github.com/anoma/juvix-lean) | Juvix Lean library for compiler run verification | MIT | v4.19.0-rc2 | 3,505 | 2025-11-04 | ✗ | | +| 6 | [Antoine-dSG/frieze_patterns](https://github.com/Antoine-dSG/frieze_patterns) | A project to formalise Coxeter's frieze patterns | | v4.10.0-rc2 | 1,440 | 2025-03-18 | – | | +| 6 | [bergmannjg/time](https://github.com/bergmannjg/time) | Port of the haskell time library to Lean 4 and verification of date calculations | MIT | v4.20.0 | 5,647 | 2025-06-10 | ✗ | | +| 6 | [chrisflav/bruhat-tits](https://github.com/chrisflav/bruhat-tits) | A formalisation of the Bruhat-Tits tree in Lean4 | Apache-2.0 | v4.19.0 | 8,284 | 2026-02-17 | ✗ | | +| 6 | [girving/render](https://github.com/girving/ray-render) | Verified renders of the Mandelbrot set | Apache-2.0 | v4.27.0-rc1 | 2,941 | 2025-12-31 | ✗ | | +| 6 | [kkytola/VirasoroProject](https://github.com/kkytola/VirasoroProject) | Lean project on the Virasoro algebra (2-cohomology of the Witt algebra, definition of the Virasoro algebra, ...) | Apache-2.0 | v4.27.0-rc1 | 6,026 | 2026-04-05 | ✗ | | +| 6 | [Koukyosyumei/runwai_project](https://github.com/Koukyosyumei/Runwai) | COMS 6998 (Fall 2025): Refinement-typed DSL for certified AIR constraints and lookups | Apache-2.0 | v4.24.0 | 5,873 | 2026-03-26 | ✓ | | +| 6 | [mariainesdff/LocalClassFieldTheory](https://github.com/mariainesdff/LocalClassFieldTheory) | Formalization of local fields, and eventually LCFT | | v4.22.0-rc2 | 14,717 | 2026-03-10 | – | | +| 6 | [mbkybky/module_localProperties](https://github.com/mbkybky/module_localProperties) | Formalizing local properties of modules in LEAN | | v4.30.0-rc2 | 2,148 | 2026-05-08 | – | | +| 6 | [MichaelStollBayreuth/Weights](https://github.com/MichaelStollBayreuth/Weights) | Formalization in Lean4 of some results in "Minimization of hypersurfaces" by A.-S. Elsenhans and myself | GPL-2.0 | v4.24.0 | 1,845 | 2026-04-10 | ✗ | | +| 6 | [Paul-Lez/PersistentDecomp](https://github.com/Paul-Lez/PersistentDecomp) | Formalizing the Structure Theorem for Persistence Modules | Apache-2.0 | v4.29.0 | 1,607 | 2026-04-08 | ✗ | | +| 6 | [ro-gut/turan3](https://github.com/ro-gut/turan3) | Formalisation of (the 3rd) Turan's Theorem Proof from The Book (6th Edition) | | v4.24.0-rc1 | 2,836 | 2025-09-24 | – | | +| 6 | [septract/denyguarantee-v3](https://github.com/septract/denyguarantee-v3) | | | v4.21.0 | 3,116 | 2026-01-11 | – | | +| 6 | [Shreyas4991/DGAlgorithms](https://github.com/Shreyas4991/DGAlgorithms) | Distributed Graph Algorithms in Lean | Apache-2.0 | v4.28.0 | 3,658 | 2026-03-10 | ✗ | | +| 6 | [ToposInstitute/lean-poly](https://github.com/ToposInstitute/lean-poly) | | | v4.3.0-rc1 | 797 | 2024-12-04 | – | | +| 6 | [urkud/SardMoreira](https://github.com/urkud/SardMoreira) | Formalization of Moreira's version of Sard's Theorem | Apache-2.0 | v4.27.0-rc1 | 4,869 | 2025-12-27 | ✗ | | +| 5 | [AdrienChampion/collChoSoWel](https://github.com/AdrienChampion/collChoSoWel) | | Apache-2.0 | nightly-2023-09-02 | 7,379 | 2026-01-31 | ✗ | | +| 5 | [AlexeyMilovanov/kolmogorov-complexity-lean](https://github.com/AlexeyMilovanov/kolmogorov-complexity-lean) | Formalization of Algorithmic Information Theory in Lean 4 | | v4.29.0-rc8 | 2,046 | 2026-04-07 | – | | +| 5 | [alexoltean61/hybrid_logic_lean](https://github.com/alexoltean61/hybrid_logic_lean) | | | nightly-2023-06-10 | 5,287 | 2025-09-18 | – | | +| 5 | [alja123/hyperstabilityES](https://github.com/alja123/hyperstabilityES) | | | v4.8.0-rc1 | 35,993 | 2024-12-17 | – | | +| 5 | [AntoineChambert-Loir/DividedPowers4](https://github.com/AntoineChambert-Loir/DividedPowers4) | DividedPowers in Lean / Mathlib 4 | | v4.30.0-rc1 | 70,762 | 2026-04-10 | – | | +| 5 | [atlas-computing-org/bignum](https://github.com/atlas-computing-org/bignum) | port of s2n-bignum to Lean | Apache-2.0 | v4.30.0-rc2 | 4,637 | 2026-04-23 | ✓ | | +| 5 | [ATOMSLab/DimensionalAnalysis](https://github.com/ATOMSLab/LeanDimensionalAnalysis) | Formally-verified dimensional analysis in Lean | Apache-2.0 | v4.23.0-rc2 | 1,052 | 2025-10-15 | ✗ | | +| 5 | [BasisResearch/VerifiedJS](https://github.com/BasisResearch/VerifiedJS) | A vibe-slopped verified compiler maybe? | | v4.29.0-rc6 | 102,423 | 2026-04-19 | – | | +| 5 | [dagurtomas/LeanCondensed](https://github.com/dagurtomas/LeanCondensed) | | Apache-2.0 | v4.28.0-rc1 | 1,876 | 2026-03-20 | ✗ | | +| 5 | [Danelnov/Lambda-Calculus-Formalization](https://github.com/Danelnov/Lambda-Calculus-Formalization) | This formalization uses the De Bruijn indices, the objective is to formalize the Church-Rosser theorem | | v4.26.0-rc2 | 675 | 2026-01-29 | – | | +| 5 | [dhyan-aranha/Monsky](https://github.com/dhyan-aranha/Monsky) | This is a repository on the formalization of Monsky's theorem by the UvA lean community. | Apache-2.0 | v4.16.0-rc2 | 8,137 | 2025-10-30 | – | | +| 5 | [DhyeyMavani2003/chip-firing-with-lean](https://github.com/DhyeyMavani2003/chip-firing-with-lean) | A formalization of chip-firing games and the Riemann-Roch theorem for graphs using the Lean 4 theorem prover. | Apache-2.0 | v4.29.0 | 5,732 | 2026-04-03 | ✗ | | +| 5 | [elazarg/GameTheory](https://github.com/elazarg/GameTheory) | | MIT | v4.29.0 | 51,502 | 2026-05-07 | – | | +| 5 | [girving/aks](https://github.com/girving/aks) | Seiferas's simplified construction of the AKS O(log n) depth sorting network, formalised in Lean | Apache-2.0 | v4.29.0-rc4 | 36,974 | 2026-03-19 | – | | +| 5 | [girving/bottcher](https://github.com/girving/bottcher) | Verified computation of the Mandelbrot set Böttcher series | Apache-2.0 | v4.26.0-rc2 | 373 | 2025-12-19 | ✗ | | +| 5 | [lf-lang/reactor-model](https://github.com/lf-lang/reactor-model) | A Lean-based formalization of the Reactor model. | Apache-2.0 | v4.24.0-rc1 | 4,174 | 2025-10-08 | ✗ | | +| 5 | [markusdemedeiros/Eileen](https://github.com/markusdemedeiros/Eileen) | Reimplementing some data structures from Iris in Lean | | v4.17.0-rc1 | 4,333 | 2025-09-09 | – | | +| 5 | [MichaelStollBayreuth/Heights](https://github.com/MichaelStollBayreuth/Heights) | An attempt at formalizing the theory of heights in Lean | GPL-2.0 | v4.30.0-rc2 | 6,086 | 2026-04-28 | ✓ | | +| 5 | [monsterkrampe/ExistentialRules](https://github.com/monsterkrampe/Existential-Rules-in-Lean) | This repo contains formalizations around Existential Rules (aka. Tuple-Generating Dependencies) with disjunctions and t… | Apache-2.0 | v4.29.0 | 17,493 | 2026-04-23 | ✗ | | +| 5 | [or4nge19/MCMC](https://github.com/or4nge19/MCMC) | Formalization of Markov Chain Monte Carlo in Lean 4 | Apache-2.0 | v4.29.0 | 12,563 | 2026-04-29 | ✗ | | +| 5 | [Parcly-Taxel/Redhill](https://github.com/Parcly-Taxel/Redhill) | A formalisation of the disproof of Ramaekers's conjecture | MIT | v4.30.0-rc2 | 3,455 | 2026-05-05 | – | | +| 5 | [paulcadman/lean-effects](https://github.com/paulcadman/lean-effects) | | Apache-2.0 | v4.29.0 | 1,694 | 2026-04-04 | ✓ | | +| 5 | [PierreSenellart/provenance](https://github.com/PierreSenellart/provenance-lean) | Lean4 formalization of some provenance notions | MIT | v4.26.0-rc2 | 7,675 | 2026-04-16 | ✗ | | +| 5 | [RichardZandi/kleene2](https://github.com/RichardZandi/kleene2) | A lightweight Lean 4 library that formalizes the generalized Kleene Second Recursion Theorem and provides a reusable di… | | v4.20.0 | 387 | 2025-06-26 | – | | +| 5 | [Rob23oba/dependent-computability](https://github.com/Rob23oba/dependent-computability) | Automatically proving computability for Lean functions | | leanprover/lean4-pr-releases:pr-release-8867-9a8a69e | 11,286 | 2026-05-06 | – | | +| 5 | [SamuelSchlesinger/sensitivity](https://github.com/SamuelSchlesinger/sensitivity-conjecture) | Lean 4 formalization of the Sensitivity Conjecture (Huang 2019) | Apache-2.0 | v4.28.0 | 971 | 2026-03-03 | ✗ | | +| 5 | [sinhp/leanFibredCategories](https://github.com/sinhp/LeanFibredCategories) | A Lean4 Formalization of Fibred Categories | Apache-2.0 | v4.4.0-rc1 | 3,574 | 2026-04-15 | ✗ | | +| 5 | [smorel394/AbstractSimplicialComplex](https://github.com/smorel394/AbstractSimplicialComplex) | | | v4.0.0-rc4 | 4,552 | 2026-05-01 | – | | +| 5 | [somombo/quicksort](https://github.com/somombo/formalized-quicksort) | Implementation and Formal Verification of the Quicksort Algorithm | Apache-2.0 | v4.14.0 | 2,168 | 2026-03-20 | ✗ | | +| 5 | [VTrelat/ZFLean](https://github.com/VTrelat/ZFLean) | A practical framework for set-theoretical development in Lean | Apache-2.0 | v4.27.0 | 9,623 | 2026-04-01 | ✗ | | +| 5 | [WuProver/lean_characteristic_set](https://github.com/WuProver/lean_characteristic_set) | Formalization of the Characteristic Set Method in Lean 4 | Apache-2.0 | v4.29.0-rc6 | 4,317 | 2026-03-26 | – | | +| 5 | [znssong/Frucht](https://github.com/znssong/Frucht) | Formalization of Frucht's theorem in Lean | Apache-2.0 | v4.29.0-rc4 | 2,418 | 2026-03-21 | ✗ | | +| 4 | [anlucia/chromatic_polynomial](https://github.com/anlucia/ChromaticPolynomial) | Chromatic polynomial in Lean4 | Apache-2.0 | v4.11.0-rc1 | 473 | 2025-03-24 | ✓ | | +| 4 | [AtticusKuhn/Transition-System-Ranking-Function](https://github.com/AtticusKuhn/Transition-System-Ranking-Function) | | | v4.21.0-rc3 | 4,139 | 2026-01-12 | – | | +| 4 | [AxiomMath/PartialRegularity](https://github.com/AxiomMath/partial-regularity) | Lean formalizations for the paper "Almost all primes are partially regular" | MIT | v4.26.0 | 4,274 | 2026-03-25 | ✗ | | +| 4 | [bustercopley/lean-float](https://github.com/bustercopley/lean-float) | Lemmas on floating-point arithmetic, in Lean 4 | | v4.19.0-rc2 | 1,773 | 2025-08-05 | – | | +| 4 | [CBirkbeck/ModularForms_Lean4](https://github.com/CBirkbeck/ModularForms_Lean4) | | | v4.5.0-rc1 | 11,539 | 2024-11-08 | – | | +| 4 | [Command-Master/pseudorandom](https://github.com/Command-Master/lean-bourgain) | | Apache-2.0 | v4.7.0 | 7,322 | 2024-11-05 | ✗ | | +| 4 | [Dominique-Lawson/lean_4](https://github.com/Dominique-Lawson/Directed-Topology-Lean-4) | | MIT | v4.6.0-rc1 | 6,721 | 2026-03-26 | ✓ | | +| 4 | [doxtor6/MerLean_FormalQualBench](https://github.com/doxtor6/MerLean_FormalQualBench) | | | v4.28.0-rc1 | 10,415 | 2026-05-08 | – | | +| 4 | [fgdorais/extra](https://github.com/fgdorais/extra4) | Supplements to the Lean 4 Standard Library | Apache-2.0 | v4.29.0-rc3 | 4,647 | 2026-04-18 | ✗ | | +| 4 | [FLDutchmann/selbergSieve](https://github.com/FLDutchmann/selberg-sieve4) | A formalisation of the Selberg sieve in Lean 4 | Apache-2.0 | v4.7.0-rc2 | 3,534 | 2026-04-08 | ✗ | | +| 4 | [FordUniver/thebook.lean](https://github.com/FordUniver/thebook.lean) | Proofs from THE BOOK written up in lean | | v4.17.0-rc1 | 1,072 | 2025-12-30 | – | | +| 4 | [hgoldstein95/palamedes](https://github.com/hgoldstein95/palamedes-lean) | | MIT | v4.24.0 | 6,291 | 2026-04-09 | ✗ | | +| 4 | [hojonathanho/isoperimetric](https://github.com/hojonathanho/isoperimetric) | Lean 4 proofs of the isoperimetric inequality, Brunn-Minkowski inequality, and Prékopa-Leindler inequality | Apache-2.0 | v4.26.0-rc2 | 1,157 | 2026-04-25 | – | | +| 4 | [imbrem/discretion](https://github.com/imbrem/discretion) | Utilities for formalizing programming languages in Lean 4, along with other tidbits | 0BSD | v4.20.0-rc5 | 27,354 | 2025-07-02 | ✗ | | +| 4 | [input-output-hk/CardanoLedgerApi](https://github.com/input-output-hk/CardanoLedgerApiBlaster) | Cardano Ledger Api providing the necessary types and predicates to prove Plutus smart contracts with Blaster | Apache-2.0 | v4.24.0 | 7,037 | 2026-04-27 | ✗ | | +| 4 | [ionathanch/CBPV](https://github.com/ionathanch/CBPV) | Lean 4 mechanization of assorted CBPV metatheory. | Zlib | v4.28.0 | 4,756 | 2026-04-01 | ✗ | | +| 4 | [JobPetrovcic/ArtinWedderburn](https://github.com/JobPetrovcic/ArtinWedderburn) | A formalized proof of Artin-Wedderburn theorem in Lean4 | MIT | v4.14.0-rc2 | 2,768 | 2025-07-14 | ✗ | | +| 4 | [JoeyEremondi/lean-cwf](https://github.com/JoeyEremondi/lean-cwf) | A basic Categories with Families library for Lean | BSD-3-Clause | | 5,346 | 2025-02-18 | – | | +| 4 | [jrr6/lean-tables](https://github.com/jrr6/lean-tables) | A dependently-typed tables library, written in Lean 4, based on the Brown Benchmark for Table Types (B2T2). | | v4.14.0 | 8,097 | 2026-03-26 | – | | +| 4 | [juanjomadrigal/denotational-lean](https://github.com/juanjomadrigal/denotational-lean) | | | v4.24.0 | 1,048 | 2025-12-03 | – | | +| 4 | [kim-em/lean-finmap](https://github.com/kim-em/lean-finmap) | | Apache-2.0 | nightly-2025-08-19 | 1,103 | 2025-10-01 | ✗ | | +| 4 | [lexzaiello/Dcc](https://github.com/lexzaiello/DCC) | The dependently-typed combinator calculus (DCC). | GPL-3.0 | v4.26.0 | 2,203 | 2026-04-29 | ✗ | | +| 4 | [lindy-labs/corelib_verification](https://github.com/lindy-labs/corelib_verification) | | GPL-3.0 | v4.20.0-rc5 | 4,729 | 2025-06-11 | ✗ | | +| 4 | [Linyxus/capless](https://github.com/Linyxus/capless-lean) | | MIT | v4.21.0-rc3 | 11,441 | 2026-01-29 | ✗ | | +| 4 | [mariovagomarzal/HigherCategoryTheory](https://github.com/mariovagomarzal/higher_category_theory) | A formal verification project based on the work by Enric Cosme Llópez on "Higher-order categories". | Apache-2.0 | v4.28.0 | 2,864 | 2026-04-25 | ✗ | | +| 4 | [markusdemedeiros/Metrology](https://github.com/markusdemedeiros/Metrology) | | | v4.29.0 | 37,035 | 2026-05-08 | – | | +| 4 | [mbkybky/KoszulComplex](https://github.com/mbkybky/KoszulComplex) | | | v4.28.0-rc1 | 429 | 2026-03-16 | – | | +| 4 | [MichaelStollBayreuth/LegendreQF](https://github.com/MichaelStollBayreuth/LegendreQF) | Lean code formalizing a proof of Legendre's theorem on diagonal ternary quadratic forms | GPL-2.0 | v4.24.0 | 1,888 | 2025-11-01 | – | | +| 4 | [pandaman64/QuickSortInLean](https://github.com/pandaman64/QuickSortInLean) | | | v4.8.0-rc2 | 1,041 | 2024-08-08 | – | | +| 4 | [pandaman64/Tables](https://github.com/pandaman64/Tables) | | | v4.30.0-rc2 | 4,908 | 2026-05-02 | – | | +| 4 | [parabamoghv/Symm](https://github.com/parabamoghv/DashedMonoids) | Formalization of a new data structure: Dashed-Monoids | GPL-3.0 | v4.7.0 | 6,139 | 2026-02-01 | ✗ | | +| 4 | [Rickerd1234/RelationalAlgebra](https://github.com/Rickerd1234/RelationalAlgebra) | University Master Thesis | Apache-2.0 | v4.24.0 | 6,315 | 2026-03-08 | ✗ | | +| 4 | [roos-j/BooleanFun](https://github.com/roos-j/lean-booleanfun) | Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier anal… | Apache-2.0 | v4.16.0-rc2 | 1,517 | 2026-03-03 | ✗ | | +| 4 | [rupakm/leslie](https://github.com/rupakm/leslie) | | Apache-2.0 | v4.27.0 | 103,563 | 2026-04-29 | ✗ | | +| 4 | [samuelborza/IsTranscendentalPi](https://github.com/samuelborza/IsTranscendentalPi) | Formalization in Lean of the transcendence of π. | Apache-2.0 | v4.30.0-rc2 | 1,755 | 2026-04-27 | – | | +| 4 | [samvang/StoneDualityInLean](https://github.com/samvang/StoneDualityInLean) | | | v4.8.0-rc1 | 1,079 | 2025-11-27 | – | | +| 4 | [Shreyas4991/Algolean](https://github.com/Shreyas4991/Algolean) | Algorithms and Complexity Library using the lightweight query combinator framework called "Prog" | Apache-2.0 | v4.29.0 | 4,840 | 2026-04-21 | ✗ | | +| 4 | [sinianluoye/LeanOfRudinAnalysis](https://github.com/sinianluoye/LeanOfRudinAnalysis) | Lean code about Rudin's 《Principles of Mathematical Analysis》 | | v4.22.0-rc4 | 8,438 | 2026-02-21 | – | | +| 4 | [sterraf/ChainBounding](https://github.com/sterraf/ChainBounding) | Formalization of a simpler proof of Zorn's Lemma | Apache-2.0 | v4.8.0-rc1 | 441 | 2025-07-03 | – | | +| 4 | [T-Brick/numbers](https://github.com/T-Brick/Numbers) | Arbitrary Bit-Length Integers in Lean | GPL-3.0 | v4.25.0 | 676 | 2025-11-14 | ✓ | | +| 4 | [thejohncrafter/Catlib4](https://github.com/thejohncrafter/Catlib4) | Lean 4 library heavily focused on category theory and theoretical computer science | | nightly-2023-04-20 | 3,045 | 2024-11-25 | – | | +| 4 | [Timeroot/Z80Emu](https://github.com/Timeroot/Z80Emu) | Z80 Emulator in Lean with verified program demos | | v4.28.0 | 7,523 | 2026-04-30 | – | | +| 4 | [uw-math-ai/FormalizingGMT](https://github.com/uw-math-ai/FormalizingGMT) | | | v4.26.0-rc2 | 3,141 | 2026-04-30 | – | | +| 4 | [vbeffara/rMT4](https://github.com/vbeffara/RMT4) | The Riemann mapping theorem | Apache-2.0 | v4.26.0 | 1,988 | 2026-01-10 | ✗ | | +| 4 | [wupr/order-p-q](https://github.com/wupr/order-p-q) | Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers. | Apache-2.0 | v4.15.0 | 924 | 2026-01-19 | ✗ | | +| 4 | [xyzw12345/CohenMacaulay](https://github.com/xyzw12345/CohenMacaulay) | | | v4.19.0-rc2 | 2,083 | 2025-05-01 | – | | +| 4 | [YaelDillies/MiscYD](https://github.com/YaelDillies/misc-yd) | Miscellaneous projects I am working on in Lean | Apache-2.0 | v4.29.0 | 3,384 | 2026-04-14 | ✗ | | +| 3 | [adri326/rubin-lean4](https://github.com/adri326/rubin-lean4) | Proof of Rubin's theorem, written in Lean 4 | | v4.5.0-rc1 | 9,198 | 2024-03-29 | – | | +| 3 | [Aksenov239/lean-fun](https://github.com/Aksenov239/lean-fun) | | | v4.27.0-rc1 | 1,883 | 2026-05-05 | – | | +| 3 | [Akwardbro/RamificationGroup](https://github.com/Akwardbro/RamificationGroup) | Formalizing Ramification Group in LEAN | | v4.29.0-rc2 | 16,430 | 2026-03-01 | – | | +| 3 | [AlexKontorovich/CoveringSpacesProject](https://github.com/AlexKontorovich/CoveringSpacesProject) | | Apache-2.0 | v4.29.0-rc8 | 6,174 | 2026-04-15 | ✗ | | +| 3 | [AlexLoitzl/pumping_cfg](https://github.com/AlexLoitzl/pumping_cfg) | | Apache-2.0 | v4.15.0-rc1 | 3,944 | 2025-11-22 | ✗ | | +| 3 | [AntoineChambert-Loir/Jordan4](https://github.com/AntoineChambert-Loir/Jordan4) | | | v4.16.0 | 13,660 | 2025-09-13 | – | | +| 3 | [aroheebhoja/vizing](https://github.com/aroheebhoja/vizing) | Lean4 formalization of Vizing's theorem using the Misra and Gries edge contraction algorithm | | v4.21.0-rc3 | 3,752 | 2026-03-27 | – | | +| 3 | [Arthur742Ramos/Metatheory](https://github.com/Arthur742Ramos/Metatheory) | | MIT | v4.24.0 | 61,416 | 2026-04-24 | ✓ | | +| 3 | [atrieu/cryptolib](https://github.com/atrieu/lean-cryptolib) | | Apache-2.0 | v4.17.0-rc1 | 889 | 2025-04-29 | ✓ | | +| 3 | [b-mehta/HighlyAbundant](https://github.com/b-mehta/HighlyAbundant) | Formalisations relating to https://mathoverflow.net/q/501066/117945 | | v4.24.0-rc1 | 12,957 | 2025-12-19 | – | | +| 3 | [BarinderBanwait/ramanujan_nagell](https://github.com/BarinderBanwait/ramanujan_nagell) | | | v4.26.0-rc2 | 3,571 | 2026-04-08 | – | | +| 3 | [Bergschaf/Localic-Caratheodory-Extensions](https://github.com/Bergschaf/Localic-Caratheodory-Extensions) | | GPL-3.0 | v4.28.0-rc1 | 5,136 | 2026-03-12 | ✗ | | +| 3 | [bjoernkjoshanssen/interest](https://github.com/bjoernkjoshanssen/interest) | Interest: a Lean library for financial mathematics | Apache-2.0 | v4.27.0-rc1 | 7,685 | 2026-02-13 | ✗ | | +| 3 | [bridgekat/claude-formalizer](https://github.com/bridgekat/claude-formalizer) | Autoformalization baseline experiment with Claude Code. | | v4.29.0-rc8 | 2,449 | 2026-03-28 | – | | +| 3 | [cymcymcymcym/Unique_Factorization_Lean4](https://github.com/cymcymcymcym/Unique_Factorization_Lean4) | A lean 4 proof of unique prime factorization in well-ordered rings, starting from ring axioms. | | v4.12.0-rc1 | 2,373 | 2026-01-15 | – | | +| 3 | [enricozb/buffon-lean](https://github.com/enricozb/buffon-lean) | buffon's needle in lean 4 | | v4.4.0 | 922 | 2026-04-29 | – | | +| 3 | [ezhuchko/RLTL-derivatives](https://github.com/ezhuchko/RLTL-derivatives) | Lean formalization for the paper "Symbolic Automata: 𝜔-Regularity Modulo Theories" | | v4.7.0 | 1,248 | 2025-05-15 | – | | +| 3 | [fgdorais/GMLInit](https://github.com/fgdorais/GMLInit) | GML Init Package | CC0-1.0 | v4.9.0-rc1 | 6,818 | 2024-10-09 | – | | +| 3 | [formalproofs/mdplib](https://github.com/formalproofs/MDPLib) | | Unlicense | v4.30.0-rc2 | 3,154 | 2026-04-24 | ✓ | | +| 3 | [functionally/Crypto](https://github.com/functionally/crypto-lean4) | Implementation of various cryptographic functions in Lean4 | MIT | v4.7.0 | 2,842 | 2025-10-23 | ✗ | | +| 3 | [goens/Hoare](https://github.com/goens/lean-hoare) | Hoare Logic in Lean | MIT | v4.22.0-rc2 | 1,487 | 2026-04-12 | ✗ | | +| 3 | [guest2180/lean4-quantum](https://github.com/guest2180/lean4-quantum) | An implementation of the theory of quantum computing in the Lean programming language (using the Lean theorem prover ve… | | v4.16.0 | 5,150 | 2025-12-27 | – | | +| 3 | [Gusarich/tvm-lean](https://github.com/Gusarich/tvm-lean) | | MIT | v4.24.0 | 345,213 | 2026-02-28 | ✗ | | +| 3 | [harfe/fixed-point-theorems-lean4](https://github.com/harfe/fixed-point-theorems-lean4) | Kakutani fixed-point theorem and Brouwer fixed-point theorem formalized and proven in Lean 4 | | v4.21.0-rc3 | 3,257 | 2026-03-04 | – | | +| 3 | [hdmkindom/mathmatic_in_elementary_number_th](https://github.com/hdmkindom/mathmatic_in_elementary_number_th) | 初等数论讲义的形式化证明 by lean4 | Apache-2.0 | v4.24.0-rc1 | 300 | 2025-09-23 | ✗ | | +| 3 | [hsjoihs/dpda-lean](https://github.com/hsjoihs/dpda-lean) | | | v4.22.0-rc3 | 2,503 | 2025-07-10 | – | | +| 3 | [ishiut/fo_zfc](https://github.com/ishiut/fo_zfc) | | Apache-2.0 | v4.22.0-rc3 | 2,450 | 2025-08-04 | – | | +| 3 | [JasonShroyer/sgc](https://github.com/JasonShroyer/sgc-lean) | Lean 4 library characterizing the algebraic structure of metastability and consolidation in stochastic systems | Apache-2.0 | v4.25.2 | 12,192 | 2026-04-26 | ✗ | | +| 3 | [jcpaik/erdos-tuza-valtr](https://github.com/jcpaik/erdos-tuza-valtr) | A formal verification of a mathematics/combinatorics paper "On the Erdős-Tuza-Valtr Conjecture" | | v4.13.0-rc3 | 2,302 | 2024-11-09 | – | | +| 3 | [jjaassoonn/GAGA](https://github.com/jjaassoonn/GAGA) | (Attempt of) Formalising the GAGA theorem | | v4.7.0-rc2 | 338 | 2025-02-09 | – | | +| 3 | [jjdishere/neukirch](https://github.com/jjdishere/neukirch) | | | v4.5.0-rc1 | 4,756 | 2024-12-03 | – | | +| 3 | [Jun2M/Main-theorem-of-polytopes](https://github.com/Jun2M/Main-theorem-of-polytopes) | Proving the main theorem of polytopes using Lean 4 | | v4.7.0-rc2 | 2,293 | 2024-05-22 | – | | +| 3 | [katzenpost/crypt_walker](https://github.com/katzenpost/crypt_walker) | Lean and Rust based cryptographic protocol framework for formally proving protocol properties | AGPL-3.0 | | | 2024-08-24 | ✓ | | +| 3 | [KisaraBlue/ec-tate-lean](https://github.com/KisaraBlue/ec-tate-lean) | Separate project from mathib4 | | nightly-2023-08-19 | 7,786 | 2024-05-26 | – | | +| 3 | [kmill/msri2023_graphs](https://github.com/kmill/msri2023_graphs) | Repository for graph theory & combinatorics group at the MSRI Lean summer school | Apache-2.0 | nightly-2023-06-10 | 3,851 | 2024-11-12 | ✓ | | +| 3 | [LeastAuthority/STIR](https://github.com/LeastAuthority/STIR) | SC: Ethereum - zk(E)VM Verification - STIR Lean Blueprint | Apache-2.0 | v4.19.0-rc3 | 780 | 2025-05-05 | ✗ | | +| 3 | [LodeVermeulen/Lean4_Bogdanovs_lemma](https://github.com/LodeVermeulen/Lean4_Bogdanovs_lemma) | | | v4.8.0-rc1 | 1,209 | 2024-07-03 | – | | +| 3 | [lua-vr/BirkhoffErgodicThm](https://github.com/lua-vr/pointwise-birkhoff) | A proof of Pointwise Birkhoff Ergodic Theorem in Lean | Apache-2.0 | v4.20.0-rc5 | 567 | 2025-06-20 | ✗ | | +| 3 | [lunsong/JaxProof](https://github.com/lunsong/JaxProof) | | | v4.28.0 | 1,354 | 2026-05-08 | – | | +| 3 | [manuelpuebla/amo-lean](https://github.com/manuelpuebla/amo-lean) | | MIT | v4.26.0 | 70,605 | 2026-04-23 | – | | +| 3 | [matematiflo/SumSq](https://github.com/matematiflo/SumsOfSquares) | Summing squares in Lean | Apache-2.0 | v4.10.0-rc2 | 1,389 | 2025-10-24 | ✗ | | +| 3 | [mattrobball/BridgelandStability](https://github.com/mattrobball/BridgelandStability) | | Apache-2.0 | v4.29.0 | 36,493 | 2026-04-21 | – | | +| 3 | [mckoen/quasicategory](https://github.com/mckoen/quasicategory) | Formalizing quasi-categories in Lean | | v4.18.0-rc1 | 11,675 | 2025-10-25 | – | | +| 3 | [MichaelMMacLeod/formal-mergesort](https://github.com/MichaelMMacLeod/formal-mergesort) | WIP formally-verified implementation of mergesort (efficient; only allocates one auxiliary array, sorts arrays in-place) | | v4.19.0-rc3 | 2,916 | 2025-05-16 | – | | +| 3 | [MohanadAhmed/LeanMathSigProc](https://github.com/MohanadAhmed/LeanMathSigProc) | | GPL-2.0 | v4.10.0 | 623 | 2025-08-29 | ✗ | | +| 3 | [mrdouglasny/gaussian-field](https://github.com/mrdouglasny/gaussian-field) | | | v4.29.0 | 51,203 | 2026-05-09 | – | | +| 3 | [mrigankpawagi/LeanearTemporalLogic](https://github.com/mrigankpawagi/LeanearTemporalLogic) | Formalization of Linear Temporal Logic (LTL) in Lean 4. | | v4.18.0-rc1 | 4,244 | 2026-03-10 | – | | +| 3 | [nielstron/langlib](https://github.com/nielstron/langlib) | Library for formal language theory in Lean 4 | BSD-2-Clause | v4.28.0 | 40,844 | 2026-04-28 | ✗ | | +| 3 | [nsglover/Lean-4.0-LLL](https://github.com/nsglover/Lean-4.0-LLL) | | | v4.4.0-rc1 | 589 | 2025-10-19 | – | | +| 3 | [oneofvalts/desargues](https://github.com/oneofvalts/desargues) | Lean formalization of Desargues's Theorem | | | 1,221 | 2025-07-14 | – | | +| 3 | [Oscario0/LeanBisection](https://github.com/Oscario0/LeanBisection) | The Bisection method is the simplest numerical approximation approach in mathematics that applies to any continuous fun… | MIT | v4.30.0-rc1 | 1,797 | 2026-02-28 | ✗ | | +| 3 | [pannous/Hyper](https://github.com/pannous/hyper-lean) | Hyperreal Numbers in Lean 4 | Apache-2.0 | v4.27.0 | 9,636 | 2026-03-21 | ✗ | | +| 3 | [peabrainiac/CatDG](https://github.com/peabrainiac/lean-catdg) | Aspects of categorical differential geometry, formalised in lean 4. | Apache-2.0 | v4.29.0 | 9,760 | 2026-04-14 | ✗ | | +| 3 | [PratherConid/LeanLambda](https://github.com/PratherConid/LeanLambda) | | | v4.20.0 | 5,812 | 2026-02-23 | – | | +| 3 | [provables/special-numbers](https://github.com/provables/special-numbers) | Special Numbers (Chapter 6 from Knuth's Concrete Mathematics) | MIT | v4.15.0 | 647 | 2025-06-10 | ✗ | | +| 3 | [riccardobrasca/SDG](https://github.com/riccardobrasca/SDG) | Synthetic Differential Geometry in Lean | Apache-2.0 | riccardobrasca/lean4:v4.30.0-rc2-less-choice | 1,496 | 2026-04-28 | ✗ | | +| 3 | [seb488/LeanComplexAnalysis](https://github.com/seb488/LeanComplexAnalysis) | Lean formalization of some classical complex analysis theorems | Apache-2.0 | v4.28.0-rc1 | 4,910 | 2026-03-19 | – | | +| 3 | [smorel394/ExteriorPowers](https://github.com/smorel394/ExteriorPowers) | | | v4.7.0-rc2 | 8,922 | 2024-01-12 | – | | +| 3 | [smorel394/Grassmannian](https://github.com/smorel394/Grassmannian) | | | v4.2.0-rc1 | 8,133 | 2024-10-08 | – | | +| 3 | [smorel394/ProjectiveSpace_lean4](https://github.com/smorel394/ProjectiveSpace_lean4) | | | v4.2.0-rc1 | 5,767 | 2024-01-16 | – | | +| 3 | [spitters/libcrux-lean-specs](https://github.com/spitters/libcrux-lean-specs) | Hax Lean 4 prelude for libcrux pure crypto specs | | v4.28.0 | 29,329 | 2026-04-20 | – | | +| 3 | [suomela/Distributed2Coloring](https://github.com/suomela/2-coloring-1-round) | 2-Coloring Cycles in One Round: Formalization in Lean 4 | MIT | v4.28.0 | 17,214 | 2026-03-13 | ✗ | | +| 3 | [tangentstorm/leansieve](https://github.com/tangentstorm/leansieve) | A formally verified prime number sieve in Lean4. | MIT | v4.29.0-rc6 | 1,241 | 2026-03-13 | – | | +| 3 | [tchaumeny/KleeneTree](https://github.com/tchaumeny/KleeneTree) | Formalization of the Kleene tree in Lean | | v4.26.0 | 346 | 2026-04-08 | – | | +| 3 | [themathqueen/Monlib](https://github.com/themathqueen/monlib4) | Formalising non-commutative graph theory in Lean | Apache-2.0 | v4.21.0-rc3 | 31,853 | 2026-01-06 | ✗ | | +| 3 | [unhyperbolic/hyperbolicGeometryInLean](https://github.com/unhyperbolic/hyperbolicGeometryInLean) | Formalizing hyperbolic geometry in lean | | nightly-2023-06-20 | 933 | 2025-11-07 | – | | +| 3 | [uw-math-ai/lean-polyhedral-geometry](https://github.com/uw-math-ai/lean-polyhedral-geometry) | Formalizing the basic definitions and results of polyhedral geometry in Lean 4. | GPL-3.0 | v4.20.0-rc5 | 1,475 | 2025-12-13 | – | | +| 3 | [varosi/bitmap](https://github.com/varosi/Bitmap) | Lean 4 bitmap utilities with PNG encode/decode support, plus a small widget for visualization. | BSD-3-Clause | v4.29.0 | 23,444 | 2026-04-29 | ✗ | | +| 3 | [wwylele/PentagonalNumberTheorem](https://github.com/wwylele/PentagonalNumberTheorem) | | | v4.26.0-rc2 | 2,856 | 2025-12-15 | – | | +| 3 | [YanYablonovskiy/AlgebraicWheelTheory](https://github.com/YanYablonovskiy/AlgebraicWheelTheory) | Digitisation of algebraic wheel theory in Lean 4 | | v4.29.0-rc6 | 849 | 2026-04-02 | – | | +| 3 | [YijunYuan/SphericalCompleteness](https://github.com/YijunYuan/SphericalCompleteness) | | | v4.29.1 | 5,743 | 2026-05-09 | – | | +| 2 | [adambornemann-glitch/Logos_Library](https://github.com/adambornemann-glitch/Logos_Library) | Lean verified Science. | MIT | v4.29.0-rc3 | 128,550 | 2026-03-27 | – | | +| 2 | [ADedecker/ProperAction](https://github.com/ADedecker/ProperAction) | | | v4.7.0-rc2 | 908 | 2024-05-14 | – | | +| 2 | [AlexBrodbelt/DicksonsClassificationTheorem](https://github.com/AlexBrodbelt/DicksonsClassificationTheorem) | | | v4.24.0 | 5,831 | 2026-01-08 | – | | +| 2 | [AlexeyMilovanov/lean-keccak-unrolled](https://github.com/AlexeyMilovanov/lean-keccak-unrolled) | | | v4.29.0 | 15,376 | 2026-04-27 | – | | +| 2 | [alexjgreig/Quave](https://github.com/alexjgreig/QHL-Lean) | Quantum Hoare Logic Lean 4 - A quantum program verification tool | Apache-2.0 | v4.16.0-rc2 | 1,388 | 2025-09-08 | ✓ | | +| 2 | [amarmaduke/lean-stlc](https://github.com/amarmaduke/lean-stlc) | Lean4 mechanization of the simply typed lambda calculus and its metatheory including strong normalization | MIT | v4.26.0 | 3,723 | 2026-04-28 | ✗ | | +| 2 | [AnirudhG07/huffman](https://github.com/AnirudhG07/LeanHuffmanCoding) | Lean for Huffmann Coding Algorithms, as a course Project for Proof and Programs 25. | MIT | v4.29.0 | 3,388 | 2026-04-24 | ✓ | | +| 2 | [AntoineChambert-Loir/Sion4](https://github.com/AntoineChambert-Loir/Sion4) | | | v4.21.0-rc3 | 3,319 | 2025-09-26 | – | | +| 2 | [ATOMSLab/LeanBET](https://github.com/ATOMSLab/LeanBET) | Formally-verified BET Adsorption analysis in Lean | | v4.27.0-rc1 | 3,047 | 2026-04-28 | – | | +| 2 | [AydenLamp/FinDFA](https://github.com/AydenLamp/FinDFA) | Lean code for thesis | | v4.25.0-rc2 | 2,375 | 2026-02-18 | – | | +| 2 | [badly-drawn-wizards/noperthedron](https://github.com/badly-drawn-wizards/noperthedron) | A Lean4 formalization of "A convex polyhedron without Rupert’s property" | Apache-2.0 | v4.25.0-rc2 | 1,105 | 2026-02-15 | – | | +| 2 | [bernborgess/lean-cutting-planes](https://github.com/bernborgess/lean-cutting-planes) | Cutting Planes formal logic modelled in Lean 4 for verified reasoning. | | v4.15.0-rc1 | 629 | 2025-12-03 | – | | +| 2 | [bjoernkjoshanssen/ac-exercises](https://github.com/bjoernkjoshanssen/ac-exercises) | Exercise solutions in Lean 4 for the book "Automatic complexity: a computable measure of irregularity", De Gruyter, 202… | | v4.14.0-rc2 | 9,181 | 2026-02-13 | – | | +| 2 | [bjoernkjoshanssen/hypothesis](https://github.com/bjoernkjoshanssen/hypothesis) | Probability and statistics in Lean | | v4.27.0-rc1 | 5,401 | 2026-02-18 | – | | +| 2 | [bolito2/DemazureOperatorsLean](https://github.com/bolito2/DemazureOperatorsLean) | Formalizing some theorems about Demazure operators in Lean4 | Apache-2.0 | v4.14.0-rc3 | 2,927 | 2025-02-20 | – | | +| 2 | [bsubercaseaux/lean-proofs](https://github.com/bsubercaseaux/lean-proofs) | Some of my Lean proofs | | v4.18.0-rc1 | 345 | 2025-03-19 | – | | +| 2 | [CarlKCarlK/RangeSetBlaze](https://github.com/CarlKCarlK/range-set-blaze-lean) | | Apache-2.0 | v4.24.0-rc1 | 4,787 | 2025-11-01 | ✗ | | +| 2 | [chrisflav/pi1](https://github.com/chrisflav/pi1) | A formalisation of the étale fundamental group of a scheme in Lean 4 | Apache-2.0 | v4.30.0-rc2 | 6,534 | 2026-04-27 | – | | +| 2 | [ChrisHughes24/axgroth](https://github.com/ChrisHughes24/axgroth) | | | v4.23.0-rc2 | 933 | 2026-03-29 | – | | +| 2 | [fgdorais/algebra](https://github.com/fgdorais/algebra4) | Algebra library for Lean 4 | Apache-2.0 | v4.29.0-rc3 | 2,853 | 2026-03-04 | ✗ | | +| 2 | [fgdorais/lean4-automata](https://github.com/fgdorais/lean4-automata) | | Apache-2.0 | v4.23.0-rc1 | 1,938 | 2025-08-14 | ✗ | | +| 2 | [fgdorais/logic](https://github.com/fgdorais/logic4) | Logic Library for Lean 4 | Apache-2.0 | v4.29.0-rc3 | 1,561 | 2026-03-03 | ✗ | | +| 2 | [fpvandoorn/sard](https://github.com/fpvandoorn/sard) | Work towards a general version of Sard's theorem in Lean 4 | Apache-2.0 | v4.12.0 | 1,360 | 2024-10-07 | ✗ | | +| 2 | [gift-framework/core](https://github.com/gift-framework/core) | GIFT Core: Certified mathematical identities from E8×E8 gauge theory on G2 manifolds. Verified in Lean 4 | MIT | v4.29.0 | 37,288 | 2026-05-05 | – | | +| 2 | [gmcninch-prof/VERSEIM-2025](https://github.com/gmcninch-prof/VERSEIM-2025) | repo for the formalization project in VERSEIM-REU at Tufts 2025 | Apache-2.0 | | 29,081 | 2025-08-12 | – | | +| 2 | [hwatheod/galeShapley](https://github.com/hwatheod/galeshapley-lean) | Formalization in Lean of some results related to stable matchings and the Gale-Shapley algorithm | MIT | v4.29.0-rc7 | 4,876 | 2026-03-24 | ✗ | | +| 2 | [hyeoniuwu/CiL](https://github.com/hyeoniuwu/CiL) | | | v4.30.0-rc2 | 13,354 | 2026-05-05 | – | | +| 2 | [idontgetoutmuch/DifferentialGeometry](https://github.com/idontgetoutmuch/DifferentialGeometry) | | | | 3,977 | 2026-04-17 | – | | +| 2 | [int-y1/proofs](https://github.com/int-y1/proofs) | random proofs in lean 4 | MIT | v4.29.0-rc8 | 334,335 | 2026-04-09 | ✗ | | +| 2 | [itsalissonsilva/LeanML](https://github.com/itsalissonsilva/lean-ml) | Formally verified machine learning in Lean 4. | Apache-2.0 | v4.30.0-rc1 | 626 | 2026-04-25 | ✓ | | +| 2 | [ivankobe/FactorizationSystems](https://github.com/ivankobe/FactorizationSystems) | | MIT | v4.14.0-rc2 | 2,501 | 2025-01-21 | ✗ | | +| 2 | [j-loreaux/LeanOA](https://github.com/j-loreaux/LeanOA) | Operator algebras in Lean | | v4.30.0-rc2 | 6,249 | 2026-05-04 | – | | +| 2 | [JJYYY-JJY/NormalForms](https://github.com/JJYYY-JJY/lean-normal-forms) | Executable Hermite and Smith Normal Forms in Lean 4 over Euclidean Domains, with a PID bridge to mathlib. | Apache-2.0 | | | 2026-03-22 | ✗ | | +| 2 | [jzxia/WhiteheadTheorem](https://github.com/jzxia/WhiteheadTheorem) | Proving the Whitehead theorem for Mathlib's homotopy groups. | | v4.21.0-rc3 | 7,984 | 2026-03-12 | – | | +| 2 | [kckennylau/EllipticCurve](https://github.com/kckennylau/EllipticCurve) | Towards a general definition of elliptic curve over schemes | Apache-2.0 | v4.25.0-rc2 | 7,309 | 2025-11-04 | ✗ | | +| 2 | [kkytola/ExtremeValueProject](https://github.com/kkytola/ExtremeValueProject) | A project to formalize Fisher-Tippett-Gnedenko theorem (default project of course MS-EV0029) | Apache-2.0 | v4.23.0-rc2 | 4,156 | 2025-08-15 | ✗ | | +| 2 | [klavins/LeanBook](https://github.com/klavins/LeanBook) | Notes on the Foundations of Lean | GPL-3.0 | | | 2025-08-21 | ✗ | | +| 2 | [Koukyosyumei/pol](https://github.com/Koukyosyumei/PoL) | Proof of Lean: Formalizing Blockchain Fundamentals in Lean | Apache-2.0 | v4.22.0-rc3 | 919 | 2025-08-26 | ✓ | | +| 2 | [kuruczgy/lean-model-checking](https://github.com/kuruczgy/lean-model-checking) | Formalizations of some theorems related to model checking | Apache-2.0 | v4.29.0 | 2,420 | 2026-03-31 | – | | +| 2 | [lambdaclass/optisat](https://github.com/lambdaclass/truth_research) | Formally verified equality saturation engine in Lean 4, parameterized by typeclasses. OptiSat provides a domain-agnosti… | MIT | v4.26.0 | 12,242 | 2026-04-27 | ✓ | | +| 2 | [lean-ja/verso-manual](https://github.com/lean-ja/reference-manual-ja) | 「The Lean Language Reference」の日本語訳（作業中） | Apache-2.0 | v4.15.0-rc1 | 35,297 | 2025-01-05 | ✗ | | +| 2 | [lindy-labs/WadrayVerification](https://github.com/lindy-labs/wadray_verification) | Verification of the Wadray library | GPL-3.0 | v4.9.0-rc2 | 3,344 | 2024-06-21 | ✗ | | +| 2 | [Louis-Le-Grand/Formalisation-of-constructable-numbers](https://github.com/Louis-Le-Grand/Formalisation-of-constructable-numbers) | | | v4.11.0-rc2 | 6,146 | 2024-11-13 | – | | +| 2 | [m4lvin/Gossip](https://github.com/m4lvin/Gossip-in-Lean) | Verified Results about Gossip protocols in Lean 4 | Apache-2.0 | v4.28.0 | 3,233 | 2026-04-29 | ✗ | | +| 2 | [madvorak/matroids](https://github.com/madvorak/matroids) | Classes of matroids and their properties | MIT | v4.7.0 | 625 | 2024-04-25 | – | | +| 2 | [madvorak/thue](https://github.com/madvorak/thue) | Semi-Thue systems a.k.a. string rewriting systems | BSD-2-Clause | nightly-2023-07-12 | 1,012 | 2024-10-21 | ✗ | | +| 2 | [mariainesdff/ostrowski2024](https://github.com/mariainesdff/ostrowski2024) | | | v4.26.0-rc2 | 2,507 | 2025-12-14 | – | | +| 2 | [mbkybky/InfiniteGaloisTheory](https://github.com/mbkybky/InfiniteGaloisTheory) | Formalizing infinite Galois theory in LEAN | | v4.12.0-rc1 | 4,728 | 2026-05-04 | – | | +| 2 | [mbkybky/QuillenSuslin](https://github.com/mbkybky/QuillenSuslin) | Formalizing Quillen-Suslin theorem in LEAN | | v4.28.0-rc1 | 5,062 | 2026-05-06 | – | | +| 2 | [mdbrnowski/Apportionmentlib](https://github.com/mdbrnowski/apportionmentlib) | Formal verification of apportionment theory. | Apache-2.0 | v4.28.0 | 376 | 2026-03-23 | ✗ | | +| 2 | [Mintpath/p_ne_np](https://github.com/Mintpath/p-neq-np-lean) | Machine-verified proof (0 sorries, 2 axioms) that P ≠ NP via exponential circuit lower bounds for Hamiltonian Cycle. Le… | MIT | v4.28.0 | 15,606 | 2026-03-29 | ✗ | | +| 2 | [misaka10987/archimedes](https://github.com/misaka10987/archimedes) | Don't disturb my circle! | MIT | v4.25.0-rc2 | 412 | 2025-11-04 | ✗ | | +| 2 | [mitchell-horner/ErdosStoneSimonovitsKovariSosTuran](https://github.com/mitchell-horner/ErdosStoneSimonovitsKovariSosTuran) | Formalising the Erdős-Stone-Simonovits theorem and the Kővári–Sós–Turán theorem in Lean | Apache-2.0 | v4.16.0-rc2 | 3,341 | 2026-04-29 | ✗ | | +| 2 | [monsterkrampe/PossiblyInfiniteTrees](https://github.com/monsterkrampe/Possibly-Infinite-Trees) | This repo formalizes (possibly) infinite trees of finite degree in Lean. So far this is mainly a dependency for one of… | Apache-2.0 | v4.29.0 | 3,114 | 2026-04-14 | ✗ | | +| 2 | [mrdouglasny/jacobian-challenge](https://github.com/mrdouglasny/jacobian-challenge) | Lean 4 attempt at Kevin Buzzard's Jacobian Challenge (Apr 2026) | | v4.30.0-rc1 | 27,833 | 2026-04-29 | – | | +| 2 | [nasqret/fineqs](https://github.com/nasqret/fineqs) | Lean4 formalization with Artistotle of the arXiv paper 1906.11174 | Apache-2.0 | v4.24.0 | 648 | 2026-01-26 | ✗ | | +| 2 | [NickAdfor/The-polynomial-method-and-restricted-sums-of-congruence-classes](https://github.com/NickAdfor/The-polynomial-method-and-restricted-sums-of-congruence-classes) | | | v4.27.0-rc1 | 4,149 | 2026-03-13 | – | | +| 2 | [niklasmohrin/LeanSeminar](https://github.com/niklasmohrin/lean-seminar-2023) | Construction of a flow equivalent forest from a flow matrix in Lean 4 | MIT | v4.7.0 | 2,306 | 2025-02-07 | ✗ | | +| 2 | [nomeata/lean-darray](https://github.com/nomeata/lean-darray) | | Apache-2.0 | v4.28.0 | 933 | 2026-03-30 | – | | +| 2 | [NoneMore/StabilityTheory](https://github.com/NoneMore/StabilityTheory) | | | v4.30.0-rc1 | 2,337 | 2026-05-07 | – | | +| 2 | [penteract/pythagTreeProof](https://github.com/penteract/pythagTreeProof) | A formal proof that the area of the pythagoras tree is 1282341301154741436886299752561669174104157968892079433136395356… | | v4.22.0-rc3 | 7,813 | 2025-07-22 | – | | +| 2 | [physicslib/Physicslib](https://github.com/physicslib/physicslib4) | Solving Hilbert's sixth problem in Lean | Apache-2.0 | v4.23.0-rc2 | 399 | 2026-01-19 | ✗ | | +| 2 | [pitmonticone/QuadraticIntegers](https://github.com/pitmonticone/QuadraticIntegers) | Formalising the Ring of Integers in Quadratic Fields in the Lean proof assistant. | Apache-2.0 | v4.24.0 | 2,126 | 2026-03-09 | – | | +| 2 | [pitmonticone/SumsThreeSquares](https://github.com/pitmonticone/SumsThreeSquares) | Formalising the paper "Sums of Three Squares" by N. C. Ankeny in Lean with Aristotle. | Apache-2.0 | v4.29.1 | 1,021 | 2026-04-23 | – | | +| 2 | [Project-Navi/cd-formalization](https://github.com/Project-Navi/cd-formalization) | Lean 4 + Mathlib formalization of the Creative Determinant framework — 15 theorems proved with zero sorry, CI-enforced… | Apache-2.0 | v4.28.0 | 2,893 | 2026-04-22 | – | | +| 2 | [SamuelSchlesinger/analysis-of-boolean-functions](https://github.com/SamuelSchlesinger/analysis-of-boolean-functions) | Lean 4 formalization of Analysis of Boolean Functions by Ryan O'Donnell | | v4.29.0-rc6 | 1,480 | 2026-04-02 | – | | +| 2 | [schmittj/balanced-vectors-blueprint](https://github.com/schmittj/balanced-vectors-blueprint) | Lean Blueprint for technical lemma on maxima and minimal of certain log-concave functions | | v4.26.0 | 1,265 | 2026-03-21 | – | | +| 2 | [Shilun-Allan-Li/tcslib](https://github.com/Shilun-Allan-Li/tcslib) | Lean 4 Theoretical Computer Science Library | Apache-2.0 | v4.25.0-rc2 | 70,012 | 2026-05-08 | – | | +| 2 | [smmercuri/adele-ring_locally-compact](https://github.com/smmercuri/adele-ring_locally-compact) | The proof that the adele ring of a number field is locally compact, formalised in Lean 4. | Apache-2.0 | v4.10.0-rc2 | 1,937 | 2026-04-24 | ✗ | | +| 2 | [SReichelt/universe-abstractions](https://github.com/SReichelt/universe-abstractions) | A Lean 4 project to formalize mathematical universes with added structure | | nightly-2022-01-14 | 19,432 | 2024-04-08 | – | | +| 2 | [tdzl2003/geometry](https://github.com/tdzl2003/LeanEuclid) | | MIT | v4.21.0 | 2,733 | 2025-12-15 | ✗ | | +| 2 | [tsurumi-yizhou/SPG](https://github.com/tsurumi-yizhou/SPG) | A Lean 4 library for analyzing Spin Point Groups | Apache-2.0 | v4.29.0-rc4 | 1,764 | 2026-03-10 | ✓ | | +| 2 | [vikraman/event-structures](https://github.com/vikraman/event-structures) | Formalisation of some facts about event structures and reversibility | Apache-2.0 | v4.28.1 | 1,300 | 2026-04-24 | ✗ | | +| 2 | [vporton/atgt](https://github.com/vporton/atgt) | Formalizing Victor Porton's Navier-Stokes Proof in Lean | | v4.28.0-rc1 | 8,661 | 2026-03-10 | – | | +| 2 | [wjrtz/lean_game_theory](https://github.com/wjrtz/lean_game_theory) | Formalization of game theory in LEAN | | v4.2.0 | 918 | 2026-01-14 | – | | +| 2 | [Xiyou-Wu/RiemannianGeometry](https://github.com/Xiyou-Wu/RiemannianGeometry) | | Apache-2.0 | | | 2026-01-01 | ✗ | | +| 2 | [YaelDillies/ForbiddenMatrix](https://github.com/YaelDillies/forbidden-matrix) | Formalisation of forbidden matrix theory | Apache-2.0 | v4.29.0 | 1,667 | 2026-04-01 | ✗ | | +| 2 | [YaelDillies/MeanFourier](https://github.com/YaelDillies/mean-fourier) | Formalisation of mean Fourier analysis in Lean 4 | Apache-2.0 | v4.30.0-rc2 | 1,079 | 2026-04-14 | ✗ | | +| 2 | [YijunYuan/HarderNarasimhan](https://github.com/YijunYuan/HarderNarasimhan) | Formalization of Harder-Narasimhan theory | Apache-2.0 | v4.29.1 | 9,716 | 2026-04-12 | ✗ | | diff --git a/python/lean_pool/aggregator/__main__.py b/python/lean_pool/aggregator/__main__.py index 1d3c60c25c..cf9b5bdfd3 100644 --- a/python/lean_pool/aggregator/__main__.py +++ b/python/lean_pool/aggregator/__main__.py @@ -26,7 +26,12 @@ parse_manual_list, save_manual_packages, ) -from lean_pool.aggregator.render import load_decisions, render_table, update_readme +from lean_pool.aggregator.render import ( + load_decisions, + load_pool_repos, + render_table, + update_readme, +) from lean_pool.aggregator.reservoir import ( MANIFEST_URL, fetch_manifest, @@ -42,6 +47,7 @@ DEFAULT_CLONES_DIR = CANDIDATES_DIR / "raw_data" / "clones" DEFAULT_DECISIONS = CANDIDATES_DIR / "decisions.jsonl" DEFAULT_README = CANDIDATES_DIR / "README.md" +DEFAULT_PROJECTS_YML = REPO_ROOT / "LeanPool" / "projects.yml" @click.group() @@ -228,6 +234,19 @@ def clone( show_default=True, help="Candidates README to update in place.", ) +@click.option( + "--projects-yml", + "projects_yml_path", + type=click.Path(dir_okay=False, path_type=Path), + default=DEFAULT_PROJECTS_YML, + show_default=True, + help=( + "Path to LeanPool/projects.yml. Each project's optional " + "`source.github_repo` field marks the upstream candidate as " + "merged, putting a ✓ in the In Pool column. Pass a missing " + "path to leave the column blank for every row." + ), +) def render( manifest_path: Path, manual_data_path: Path, @@ -236,6 +255,7 @@ def render( min_loc: int, decisions_path: Path, readme_path: Path, + projects_yml_path: Path, ) -> None: """Render the candidates README table from a manifest.""" with manifest_path.open() as manifest_file: @@ -244,12 +264,14 @@ def render( combined = {**manifest, "packages": list(manifest["packages"]) + manual_packages} effective_clones_dir = clones_dir if clones_dir.exists() else None decisions = load_decisions(decisions_path) + pool_repos = load_pool_repos(projects_yml_path) table = render_table( combined, clones_dir=effective_clones_dir, min_stars=min_stars, min_loc=min_loc, decisions=decisions, + pool_repos=pool_repos, ) update_readme(readme_path, table) rendered_rows = sum(1 for line in table.splitlines() if line.startswith("| ")) @@ -259,7 +281,7 @@ def render( f"Rendered {rendered_rows} of {len(combined['packages'])} packages " f"({len(manifest['packages'])} reservoir + {len(manual_packages)} manual; " f"min-stars={min_stars}, min-loc={min_loc}, " - f"decisions={len(decisions)}) into {readme_path}" + f"decisions={len(decisions)}, pool={len(pool_repos)}) into {readme_path}" ) diff --git a/python/lean_pool/aggregator/render.py b/python/lean_pool/aggregator/render.py index 3e00ac9ea6..ad18405bf1 100644 --- a/python/lean_pool/aggregator/render.py +++ b/python/lean_pool/aggregator/render.py @@ -21,6 +21,8 @@ from pathlib import Path from typing import TypedDict +import yaml + from lean_pool.aggregator.reservoir import Build, Package, ReservoirManifest @@ -51,8 +53,9 @@ class Decision(TypedDict, total=False): ) _TABLE_HEADER = ( - "| Stars | Package | Description | License | Lean | LOC | Updated | Build |\n" - "| ---: | --- | --- | --- | --- | ---: | --- | :---: |\n" + "| Stars | Package | Description | License | Lean | LOC | Updated" + " | Build | In Pool |\n" + "| ---: | --- | --- | --- | --- | ---: | --- | :---: | :---: |\n" ) # Directories under a clone whose ``.lean`` files don't count as the @@ -187,6 +190,50 @@ def count_lean_loc(clones_dir: Path, key: str) -> int | None: return total +def load_pool_repos(projects_yml_path: Path) -> set[str]: + """Load canonical GitHub keys for projects already merged into lean-pool. + + Reads ``LeanPool/projects.yml`` and collects the + ``source.github_repo`` field of each project that has one. Keys are + normalised via :func:`canonical_key` so they match the keys produced + by :func:`package_key` for Reservoir entries. + + Args: + projects_yml_path: Path to ``LeanPool/projects.yml``. + + Returns: + Set of canonical ``owner/name`` keys. Empty if the file is + missing, malformed, or contains no ``source.github_repo`` + fields. A malformed file is logged but not fatal so renderer + output keeps working when ``projects.yml`` is being edited. + """ + if not projects_yml_path.is_file(): + return set() + try: + data = yaml.safe_load(projects_yml_path.read_text()) or {} + except yaml.YAMLError as exc: + logger.warning("%s: invalid YAML: %s", projects_yml_path, exc) + return set() + if not isinstance(data, dict): + return set() + projects = data.get("projects") or [] + if not isinstance(projects, list): + return set() + keys: set[str] = set() + for project in projects: + if not isinstance(project, dict): + continue + source = project.get("source") + if not isinstance(source, dict): + continue + repo = source.get("github_repo") + if not isinstance(repo, str) or "/" not in repo: + continue + owner, _, name = repo.partition("/") + keys.add(canonical_key(owner, name)) + return keys + + def load_decisions(path: Path) -> dict[str, Decision]: """Load classifier verdicts from a JSONL file, keyed by canonical repo. @@ -256,7 +303,12 @@ def read_toolchain(clones_dir: Path, key: str) -> str | None: return stripped or None -def _row(package: Package, toolchain: str | None, loc: int | None) -> str: +def _row( + package: Package, + toolchain: str | None, + loc: int | None, + in_pool: bool, +) -> str: """Render a single package as a markdown table row.""" full_name = package["fullName"] repo_url = _repo_url(package) @@ -274,12 +326,13 @@ def _row(package: Package, toolchain: str | None, loc: int | None) -> str: builds = package.get("builds") or [] build_glyph = _build_glyph(builds[0] if builds else None) + in_pool_glyph = "✓" if in_pool else "" stars = package.get("stars", 0) return ( f"| {stars} | {name_cell} | {description} | " f"{license_name} | {toolchain_cell} | {loc_cell} | " - f"{updated} | {build_glyph} |" + f"{updated} | {build_glyph} | {in_pool_glyph} |" ) @@ -289,6 +342,7 @@ def render_table( min_stars: int = 0, min_loc: int = 0, decisions: dict[str, Decision] | None = None, + pool_repos: set[str] | None = None, ) -> str: """Render the manifest as a markdown table. @@ -322,6 +376,11 @@ def render_table( canonical key has ``include == False`` are dropped. Repos with no entry in ``decisions`` are kept regardless, so partial classification doesn't silently lose packages. + pool_repos: Optional set of canonical ``owner/name`` keys for + candidates already merged into lean-pool (see + :func:`load_pool_repos`). Rows whose key is in the set get + a ``✓`` in the ``In Pool`` column; everything else is left + blank. Defaults to no merged candidates when omitted. Returns: A markdown table including header, separator, and one row per @@ -375,8 +434,15 @@ def _details(package: Package) -> tuple[str | None, int | None]: key=lambda row: (-row[0].get("stars", 0), row[0]["fullName"].lower()), ) + pool_keys = pool_repos or set() + + def _in_pool(package: Package) -> bool: + key = package_key(package) + return key is not None and key in pool_keys + rows = "\n".join( - _row(package, toolchain, loc) for package, toolchain, loc in enriched + _row(package, toolchain, loc, _in_pool(package)) + for package, toolchain, loc in enriched ) return _TABLE_HEADER + rows + "\n" diff --git a/python/tests/aggregator/test_render.py b/python/tests/aggregator/test_render.py index 6ea8816dc4..ce0d415e0c 100644 --- a/python/tests/aggregator/test_render.py +++ b/python/tests/aggregator/test_render.py @@ -12,6 +12,7 @@ canonical_key, count_lean_loc, load_decisions, + load_pool_repos, package_key, read_toolchain, render_table, @@ -126,9 +127,12 @@ def test_render_table_handles_missing_optional_fields() -> None: table = render_table(manifest) - # Build column is the last cell on the row; expect the missing-glyph. package_row = next(line for line in table.splitlines() if "acme/demo" in line) - assert package_row.rstrip().endswith("| – |") + cells = [cell.strip() for cell in package_row.split("|")] + # Build glyph sits in the Build column (index 8); the trailing In + # Pool cell is blank when no pool_repos is provided. + assert cells[8] == "–" + assert cells[9] == "" def test_render_table_escapes_pipes_and_newlines_in_description() -> None: @@ -536,5 +540,119 @@ def test_render_table_lean_column_blank_without_clone(tmp_path: Path) -> None: package_row = next(line for line in table.splitlines() if "acme/demo" in line) cells = [cell.strip() for cell in package_row.split("|")] - # Cells: ['', stars, name, description, license, lean, updated, build, ''] + # Cells: ['', stars, name, description, license, lean, loc, updated, + # build, in_pool, ''] assert cells[5] == "" + + +def test_load_pool_repos_collects_github_repo_keys(tmp_path: Path) -> None: + """Each ``source.github_repo`` becomes a canonical key in the result.""" + path = tmp_path / "projects.yml" + path.write_text( + "projects:\n" + " - slug: alpha\n" + " source:\n" + " github_repo: Acme/Demo\n" + " - slug: beta\n" + " source:\n" + " github_repo: other/repo.lean\n" + ) + + assert load_pool_repos(path) == {"acme/demo", "other/repo"} + + +def test_load_pool_repos_ignores_projects_without_github_repo(tmp_path: Path) -> None: + """Projects with only arxiv/doi/url sources contribute no keys.""" + path = tmp_path / "projects.yml" + path.write_text( + "projects:\n" + " - slug: alpha\n" + " source:\n" + " arxiv: '2602.03716'\n" + " - slug: beta\n" + " source:\n" + " github_repo: kept/here\n" + ) + + assert load_pool_repos(path) == {"kept/here"} + + +def test_load_pool_repos_missing_file_returns_empty(tmp_path: Path) -> None: + """A missing projects.yml is the same as no merged candidates.""" + assert load_pool_repos(tmp_path / "absent.yml") == set() + + +def test_load_pool_repos_invalid_yaml_returns_empty(tmp_path: Path) -> None: + """A malformed file logs and returns empty rather than crashing render.""" + path = tmp_path / "projects.yml" + path.write_text("projects:\n - : : :\n bad indent\n") + + assert load_pool_repos(path) == set() + + +def test_load_pool_repos_skips_malformed_entries(tmp_path: Path) -> None: + """Non-mapping projects, missing slashes, and non-string repos are skipped.""" + path = tmp_path / "projects.yml" + path.write_text( + "projects:\n" + " - slug: ok\n" + " source:\n" + " github_repo: kept/here\n" + " - slug: bare-source-string\n" + " source: arxiv:1234.5678\n" + " - slug: missing-slash\n" + " source:\n" + " github_repo: noslash\n" + " - slug: non-string\n" + " source:\n" + " github_repo: 42\n" + ) + + assert load_pool_repos(path) == {"kept/here"} + + +def test_render_table_includes_in_pool_column_header() -> None: + """The In Pool column header sits at the right edge of the table.""" + table = render_table(_manifest([_package(stars=1)])) + + header_line = table.splitlines()[0] + separator_line = table.splitlines()[1] + assert "| In Pool |" in header_line + assert header_line.index("| Build ") < header_line.index("| In Pool ") + columns = [cell.strip() for cell in separator_line.split("|")] + # Last data column should be center-aligned via ``:---:``. + assert columns[9] == ":---:" + + +def test_render_table_marks_pool_repos_with_check() -> None: + """Rows whose canonical key is in pool_repos render ✓ in the last cell.""" + merged = _package( + full_name="acme/merged", + repo_url="https://github.com/acme/merged", + stars=1, + ) + other = _package( + full_name="acme/other", + repo_url="https://github.com/acme/other", + stars=1, + ) + + table = render_table( + _manifest([merged, other]), + pool_repos={"acme/merged"}, + ) + + merged_row = next(line for line in table.splitlines() if "acme/merged" in line) + other_row = next(line for line in table.splitlines() if "acme/other" in line) + assert merged_row.rstrip().endswith("| ✓ |") + assert other_row.rstrip().endswith("| |") + + +def test_render_table_in_pool_column_blank_when_pool_repos_omitted() -> None: + """Without ``pool_repos`` every row's In Pool cell is blank.""" + package = _package(stars=1) + + table = render_table(_manifest([package])) + + package_row = next(line for line in table.splitlines() if "acme/demo" in line) + assert package_row.rstrip().endswith("| |")