From 18fe399e1504d030986f2ee6c591c770e078a7c2 Mon Sep 17 00:00:00 2001 From: justincasher Date: Sat, 9 May 2026 14:26:07 -0700 Subject: [PATCH] Dedupe candidates by canonical GitHub key The previous filter for manual.txt missed entries that differed from their Reservoir counterparts only by a `.lean` suffix or by case, and GitHub URL redirects mean some manual URLs canonicalise to repos already in Reservoir at fetch time. Result: ~80 duplicated rows in the rendered table. Adds canonical_key(owner, name) and package_key(package) in render.py that lowercase and strip `.lean`/`.git` suffixes, deriving the key from the package's source URL rather than its lakefile name (which Reservoir sets independently of the GitHub path). render_table now deduplicates by package_key keeping the first occurrence, so when the CLI puts the Reservoir manifest before the manual list, Reservoir entries win on conflicts and any future overlaps disappear automatically. Also one-shot filters manual.txt with the new helper, removing 10 entries (9 suffix-bug duplicates plus 1 internal duplicate). --- aggregator/candidates/README.md | 115 ------------------------- aggregator/candidates/manual.txt | 10 --- python/lean_pool/aggregator/render.py | 73 ++++++++++++++-- python/tests/aggregator/test_render.py | 83 +++++++++++++++++- 4 files changed, 148 insertions(+), 133 deletions(-) diff --git a/aggregator/candidates/README.md b/aggregator/candidates/README.md index 7dbf3fed09..05b7233740 100644 --- a/aggregator/candidates/README.md +++ b/aggregator/candidates/README.md @@ -25,65 +25,45 @@ Do not edit the autogenerated section by hand. | 3235 | [leanprover-community/mathlib](https://github.com/leanprover-community/mathlib4) | The math library of Lean 4 | Apache-2.0 | 2026-04-29 | ✓ | | 1686 | [teorth/Analysis](https://github.com/teorth/analysis) | A Lean companion to Analysis I | Apache-2.0 | 2026-04-29 | ✗ | | 1335 | [ulfjack/ryu](https://github.com/ulfjack/ryu) | Converts floating point numbers to decimal strings | Apache-2.0 | 2026-04-29 | ✗ | -| 1273 | [lean-dojo/LeanCopilot](https://github.com/lean-dojo/LeanCopilot) | LLMs as Copilots for Theorem Proving in Lean | MIT | 2026-05-09 | – | | 1268 | [lean-dojo/LeanCopilot](https://github.com/lean-dojo/LeanCopilot) | LLMs as Copilots for Theorem Proving in Lean | MIT | 2026-04-28 | ✓ | | 947 | [google-deepmind/formal_conjectures](https://github.com/google-deepmind/formal-conjectures) | A collection of formalized statements of conjectures in Lean. | Apache-2.0 | 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 | 2026-04-29 | ✓ | -| 566 | [leanprover-community/physlib](https://github.com/leanprover-community/physlib) | A project to digitalise results from physics into Lean. | Apache-2.0 | 2026-05-09 | – | -| 566 | [leanprover-community/physlib](https://github.com/leanprover-community/physlib) | A project to digitalise results from physics into Lean. | Apache-2.0 | 2026-05-09 | – | -| 566 | [leanprover-community/physlib](https://github.com/leanprover-community/physlib) | A project to digitalise results from physics into Lean. | Apache-2.0 | 2026-05-09 | – | | 555 | [leanprover-community/Physlib](https://github.com/leanprover-community/physlib) | A project to digitalise results from physics into Lean. | Apache-2.0 | 2026-04-29 | ✗ | -| 531 | [leanprover/cslib](https://github.com/leanprover/cslib) | The Lean Computer Science Library (CSLib) | Apache-2.0 | 2026-05-08 | – | | 517 | [leanprover/cslib](https://github.com/leanprover/cslib) | The Lean Computer Science Library (CSLib) | Apache-2.0 | 2026-04-29 | ✓ | | 517 | [Paper-Proof/paperproof](https://github.com/Paper-Proof/paperproof) | Lean theorem proving interface which feels like pen-and-paper proofs. | MIT | 2026-04-24 | ✗ | | 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 | 2026-04-29 | ✗ | | 503 | [leanprover-community/mil](https://github.com/leanprover-community/mathematics_in_lean) | The user home repository for the Mathematics in Lean tutorial. | Apache-2.0 | 2026-04-28 | ✗ | | 496 | [lecopivo/scilean](https://github.com/lecopivo/SciLean) | Scientific computing in Lean 4 | Apache-2.0 | 2026-04-28 | ✗ | -| 380 | [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 | 2026-05-09 | – | | 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 | 2026-04-29 | ✓ | -| 367 | [PatrickMassot/GlimpseOfLean](https://github.com/PatrickMassot/GlimpseOfLean) | An introduction to theorem proving in Lean for the impatient. | Apache-2.0 | 2026-05-08 | – | -| 365 | [leanprover-community/aesop](https://github.com/leanprover-community/aesop) | White-box automation for Lean 4 | Apache-2.0 | 2026-05-08 | – | | 364 | [PatrickMassot/glimpseOfLean](https://github.com/PatrickMassot/GlimpseOfLean) | An introduction to theorem proving in Lean for the impatient. | Apache-2.0 | 2026-04-23 | ✗ | | 360 | [leanprover-community/aesop](https://github.com/leanprover-community/aesop) | White-box automation for Lean 4 | Apache-2.0 | 2026-04-28 | ✓ | | 338 | [hrmacbeth/math2001](https://github.com/hrmacbeth/math2001) | Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant | | 2026-05-05 | – | | 319 | [leanprover/verso](https://github.com/leanprover/verso) | Lean documentation authoring tool | Apache-2.0 | 2026-04-28 | ✓ | -| 318 | [leanprover-community/NNG4](https://github.com/leanprover-community/NNG4) | Natural Number Game | Apache-2.0 | 2026-05-05 | – | | 315 | [leanprover-community/Game](https://github.com/leanprover-community/NNG4) | Natural Number Game | Apache-2.0 | 2026-04-29 | ✗ | | 315 | [math-inc/strongpnt](https://github.com/math-inc/strongpnt) | | | 2026-05-07 | – | | 292 | [AlexKontorovich/PrimeNumberTheoremAnd](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd) | Blueprint for the PNT+ Project | Apache-2.0 | 2026-04-29 | ✗ | | 291 | [konne88/functorio](https://github.com/konne88/functorio) | | Apache-2.0 | 2026-03-16 | ✗ | -| 288 | [leanprover-community/lean4-metaprogramming-book](https://github.com/leanprover-community/lean4-metaprogramming-book) | | Apache-2.0 | 2026-05-04 | – | | 287 | [leanprover-community/lean4-metaprogramming-book](https://github.com/leanprover-community/lean4-metaprogramming-book) | | Apache-2.0 | 2026-04-24 | ✗ | | 285 | [ufmg-smite/smt](https://github.com/ufmg-smite/lean-smt) | Tactics for discharging Lean goals into SMT solvers. | Apache-2.0 | 2026-04-27 | ✗ | | 251 | [ImperialCollegeLondon/formalising-mathematics-2024](https://github.com/ImperialCollegeLondon/formalising-mathematics-2024) | Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024. | Apache-2.0 | 2026-04-22 | ✗ | | 243 | [dwrensha/compfiles](https://github.com/dwrensha/compfiles) | Catalog Of Math Problems Formalized In Lean | Apache-2.0 | 2026-04-29 | ✓ | -| 243 | [dwrensha/compfiles](https://github.com/dwrensha/compfiles) | Catalog Of Math Problems Formalized In Lean | Apache-2.0 | 2026-05-09 | – | -| 234 | [opencompl/lean-mlir](https://github.com/opencompl/lean-mlir) | A minimal development of SSA theory | | 2026-05-04 | – | | 231 | [opencompl/SSA](https://github.com/opencompl/lean-mlir) | A minimal development of SSA theory | | 2026-04-29 | ✗ | -| 230 | [FormalizedFormalLogic/Foundation](https://github.com/FormalizedFormalLogic/Foundation) | Formalization of Mathematical Logic | Apache-2.0 | 2026-05-08 | – | | 228 | [verse-lab/veil](https://github.com/verse-lab/veil) | A verifier for automated and interactive proofs about transition systems. | Apache-2.0 | 2026-04-23 | ✗ | | 226 | [FormalizedFormalLogic/Foundation](https://github.com/FormalizedFormalLogic/Foundation) | Formalization of Mathematical Logic | Apache-2.0 | 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 | 2026-04-20 | ✗ | | 207 | [cmu-l3/llmlean](https://github.com/cmu-l3/llmlean) | LLMs + Lean, on your laptop or in the cloud | MIT | 2026-04-17 | ✗ | -| 204 | [leanprover-community/ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4) | Helper toolkit for creating your own Lean 4 UserWidgets | Apache-2.0 | 2026-05-04 | – | -| 204 | [leanprover-community/ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4) | Helper toolkit for creating your own Lean 4 UserWidgets | Apache-2.0 | 2026-05-04 | – | | 201 | [leanprover-community/proofwidgets](https://github.com/leanprover-community/ProofWidgets4) | Helper toolkit for creating your own Lean 4 UserWidgets | Apache-2.0 | 2026-04-27 | ✓ | | 201 | [leanprover-community/repl](https://github.com/leanprover-community/repl) | A simple REPL for Lean 4, returning information about errors and sorries. | Apache-2.0 | 2026-05-04 | – | -| 193 | [Verified-zkEVM/ArkLib](https://github.com/Verified-zkEVM/ArkLib) | Formally Verified Arguments of Knowledge in Lean | Apache-2.0 | 2026-05-09 | – | | 191 | [avigad/mathematics_in_lean_source](https://github.com/avigad/mathematics_in_lean_source) | Source code for the Mathematics in Lean tutorial. | Apache-2.0 | 2026-05-06 | – | | 189 | [Verified-zkEVM/Arklib](https://github.com/Verified-zkEVM/ArkLib) | Formally Verified Arguments of Knowledge in Lean | Apache-2.0 | 2026-04-28 | ✗ | | 182 | [digama0/lean4lean](https://github.com/digama0/lean4lean) | Lean 4 kernel / 'external checker' written in Lean 4 | Apache-2.0 | 2026-04-28 | ✗ | | 179 | [wellecks/ntptutorial](https://github.com/wellecks/ntptutorial) | Tutorial on neural theorem proving | MIT | 2026-03-19 | ✓ | | 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 | 2026-04-29 | ✗ | -| 174 | [leanprover-community/lean-auto](https://github.com/leanprover-community/lean-auto) | Experiments on automation for Lean | Apache-2.0 | 2026-05-05 | – | | 169 | [leanprover-community/auto](https://github.com/leanprover-community/lean-auto) | Experiments on automation for Lean | Apache-2.0 | 2026-04-26 | ✓ | | 160 | [strata-org/Strata](https://github.com/strata-org/Strata) | | Apache-2.0 | 2026-04-29 | ✗ | | 156 | [lean-ja/Lean by Example](https://github.com/lean-ja/lean-by-example) | プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。 | | 2026-04-29 | ✗ | | 150 | [wellecks/llmstep](https://github.com/wellecks/llmstep) | llmstep: [L]LM proofstep suggestions in Lean 4. | MIT | 2026-04-21 | ✗ | | 146 | [argumentcomputer/yatima](https://github.com/argumentcomputer/yatima) | A zero-knowledge Lean4 compiler and kernel | MIT | 2026-03-20 | ✗ | -| 146 | [argumentcomputer/yatima](https://github.com/argumentcomputer/yatima) | A zero-knowledge Lean4 compiler and kernel | MIT | 2026-03-20 | – | -| 146 | [argumentcomputer/yatima](https://github.com/argumentcomputer/yatima) | A zero-knowledge Lean4 compiler and kernel | MIT | 2026-03-20 | – | -| 146 | [argumentcomputer/yatima](https://github.com/argumentcomputer/yatima) | A zero-knowledge Lean4 compiler and kernel | MIT | 2026-03-20 | – | | 146 | [leanprover/doc-gen4](https://github.com/leanprover/doc-gen4) | Document Generator for Lean 4 | Apache-2.0 | 2026-04-28 | ✓ | | 144 | [kmill/render](https://github.com/kmill/lean4-raytracer) | A simple raytracer written in Lean 4 | Apache-2.0 | 2026-04-17 | ✗ | | 143 | [verse-lab/Loom](https://github.com/verse-lab/loom) | Loom is a framework for automated generation of foundational multi-modal verifiers. This repository is a mirror with st… | Apache-2.0 | 2026-04-29 | ✗ | @@ -93,28 +73,21 @@ Do not edit the autogenerated section by hand. | 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 | 2026-04-25 | ✗ | | 128 | [PatrickMassot/verbose](https://github.com/PatrickMassot/verbose-lean4) | Natural language tactics to teach mathematics using Lean 4 | Apache-2.0 | 2026-04-29 | ✗ | | 126 | [Timeroot/quantumInfo](https://github.com/Timeroot/Lean-QuantumInfo) | Quantum information theory in Lean 4 | MIT | 2026-04-22 | ✗ | -| 120 | [frenzymath/jixia](https://github.com/frenzymath/jixia) | A static analysis tool for Lean 4. | Apache-2.0 | 2026-05-06 | – | | 119 | [frenzymath/jixia](https://github.com/frenzymath/jixia) | A static analysis tool for Lean 4. | Apache-2.0 | 2026-04-22 | ✓ | | 117 | [google-deepmind/debate](https://github.com/google-deepmind/debate) | Formalizing stochastic doubly-efficient debate | Apache-2.0 | 2026-04-09 | ✗ | | 116 | [avigad/lamr](https://github.com/avigad/lamr) | Logic and Mechanized Reasoning | | 2026-04-25 | – | | 116 | [siddhartha-gadgil/leanaide](https://github.com/siddhartha-gadgil/LeanAide) | Tools based on AI for helping with Lean 4 | Apache-2.0 | 2026-04-29 | ✗ | | 113 | [chasenorman/Canonical](https://github.com/chasenorman/CanonicalLean) | A Lean tactic for Canonical, a search procedure for terms in dependent type theory. | MIT | 2026-04-20 | ✗ | | 110 | [leanprover-community/Duper](https://github.com/leanprover-community/duper) | | Apache-2.0 | 2026-04-23 | ✗ | -| 110 | [leanprover-community/duper](https://github.com/leanprover-community/duper) | | Apache-2.0 | 2026-04-23 | – | | 110 | [leanprover/verso-manual](https://github.com/leanprover/reference-manual) | The Lean reference manual | Apache-2.0 | 2026-04-29 | ✓ | | 107 | [leanprover/Cli](https://github.com/leanprover/lean4-cli) | A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments. | MIT | 2026-04-19 | ✓ | -| 107 | [leanprover/lean4-cli](https://github.com/leanprover/lean4-cli) | A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments. | MIT | 2026-04-19 | – | | 107 | [rami3l/plfl](https://github.com/rami3l/PLFaLean) | Learn Lean 4 with PLFA proofs. | MIT | 2026-04-04 | ✗ | | 107 | [sdiehl/ZeroToQED](https://github.com/sdiehl/zero-to-qed) | From Zero to QED: An informal introduction to formality with Lean 4 | MIT | 2026-04-29 | ✗ | -| 106 | [leanprover-community/quote4](https://github.com/leanprover-community/quote4) | Intuitive, type-safe expression quotations for Lean 4. | Apache-2.0 | 2026-05-08 | – | -| 105 | [leanprover-community/LeanProject](https://github.com/leanprover-community/LeanProject) | A template for blueprint-driven formalization projects in Lean. | Apache-2.0 | 2026-05-03 | – | | 104 | [b-mehta/FormalisingMathematics2026](https://github.com/b-mehta/formalising-mathematics-notes) | Course notes for Formalising Mathematics 2026 | MIT | 2026-04-28 | ✗ | | 104 | [leanprover-community/Project](https://github.com/leanprover-community/LeanProject) | A template for blueprint-driven formalization projects in Lean. | Apache-2.0 | 2026-04-24 | ✓ | | 104 | [leanprover-community/Qq](https://github.com/leanprover-community/quote4) | Intuitive, type-safe expression quotations for Lean 4. | Apache-2.0 | 2026-04-28 | ✓ | | 101 | [leanprover/lnsym](https://github.com/leanprover/LNSym) | Armv8 Native Code Symbolic Simulator in Lean | Apache-2.0 | 2026-04-19 | ✗ | | 100 | [leanprover/lake](https://github.com/leanprover/lake) | **(Deprecated: Merged into Lean 4)** Lean 4 build system and package manager with configuration files written in Lean. | Apache-2.0 | 2026-03-06 | – | -| 100 | [leanprover/lake](https://github.com/leanprover/lake) | **(Deprecated: Merged into Lean 4)** Lean 4 build system and package manager with configuration files written in Lean. | Apache-2.0 | 2026-03-06 | – | -| 100 | [leanprover/lake](https://github.com/leanprover/lake) | **(Deprecated: Merged into Lean 4)** Lean 4 build system and package manager with configuration files written in Lean. | Apache-2.0 | 2026-03-06 | – | | 99 | [AxiomMath/Putnam2025](https://github.com/AxiomMath/Putnam2025) | Our solutions to Putnam 2025. | MIT | 2026-05-08 | – | | 98 | [optsuite/optlib](https://github.com/optsuite/optlib) | | Apache-2.0 | 2026-04-28 | ✗ | | 97 | [leanprover/sampcert](https://github.com/leanprover/SampCert) | SampCert : Verified Differential Privacy | Apache-2.0 | 2026-04-29 | ✗ | @@ -122,7 +95,6 @@ Do not edit the autogenerated section by hand. | 96 | [yuma-mizuno/lean-math-workshop](https://github.com/yuma-mizuno/lean-math-workshop) | 数学系のためのLean勉強会 | Apache-2.0 | 2026-03-31 | ✗ | | 95 | [emilyriehl/InfinityCosmos](https://github.com/emilyriehl/infinity-cosmos) | A blueprint for a formalization of infinity-cosmos theory in Lean. | Apache-2.0 | 2026-04-25 | ✗ | | 95 | [pandaman64/lean-regex](https://github.com/pandaman64/lean-regex) | | Apache-2.0 | 2026-04-12 | ✗ | -| 92 | [Verified-zkEVM/VCV-io](https://github.com/Verified-zkEVM/VCV-io) | Formalized Cryptography Proofs in Lean 4 | Apache-2.0 | 2026-05-09 | – | | 91 | [Verified-zkEVM/VCVio](https://github.com/Verified-zkEVM/VCV-io) | Formalized Cryptography Proofs in Lean 4 | Apache-2.0 | 2026-04-29 | ✗ | | 90 | [fpvandoorn/carleson](https://github.com/fpvandoorn/carleson) | A formalized proof of Carleson's theorem in Lean | Apache-2.0 | 2026-04-29 | ✗ | | 88 | [dwrensha/animate](https://github.com/dwrensha/animate-lean-proofs) | tool for turning Lean proofs into Blender animations | Apache-2.0 | 2026-04-18 | ✗ | @@ -133,18 +105,14 @@ Do not edit the autogenerated section by hand. | 86 | [marcusrossel/egg](https://github.com/marcusrossel/lean-egg) | A deprecated equality saturation tactic for Lean based on egg. | Apache-2.0 | 2026-04-29 | ✗ | | 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 | 2026-04-29 | ✗ | | 85 | [tydeu/alloy](https://github.com/tydeu/lean4-alloy) | Write C shims from within Lean code. | Apache-2.0 | 2026-04-14 | ✗ | -| 84 | [rzrn/ground_zero](https://github.com/rzrn/ground_zero) | Ground Zero: Lean 4 HoTT Library | Apache-2.0 | 2026-04-26 | – | | 84 | [rzrn/GroundZero](https://github.com/rzrn/ground_zero) | Ground Zero: Lean 4 HoTT Library | Apache-2.0 | 2026-04-26 | ✗ | | 83 | [fraware/leanverifier](https://github.com/fraware/leanverifier) | Framework for specifying and proving properties—such as robustness, fairness, and interpretability—of machine learning… | MIT | 2026-04-17 | – | | 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 | 2026-04-01 | ✗ | | 82 | [mo271/FormalBook](https://github.com/mo271/FormalBook) | Formalizing "Proofs from THE BOOK" | Apache-2.0 | 2026-04-08 | ✗ | -| 82 | [mo271/FormalBook](https://github.com/mo271/FormalBook) | Formalizing "Proofs from THE BOOK" | Apache-2.0 | 2026-05-01 | – | | 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… | | 2026-05-08 | – | | 78 | [fgdorais/Parser](https://github.com/fgdorais/lean4-parser) | Parser Combinator Library for Lean 4 | Apache-2.0 | 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 | 2026-03-13 | ✗ | | 76 | [argumentcomputer/LSpec](https://github.com/argumentcomputer/LSpec) | A Testing Framework for Lean | MIT | 2026-04-15 | ✓ | -| 76 | [argumentcomputer/LSpec](https://github.com/argumentcomputer/LSpec) | A Testing Framework for Lean | MIT | 2026-04-15 | – | -| 76 | [argumentcomputer/LSpec](https://github.com/argumentcomputer/LSpec) | A Testing Framework for Lean | MIT | 2026-04-15 | – | | 76 | [teorth/estimate_tools](https://github.com/teorth/estimate_tools) | | | 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 | 2026-04-14 | ✗ | | 75 | [yangky11/miniF2F-lean4](https://github.com/yangky11/miniF2F-lean4) | | MIT | 2026-04-18 | ✗ | @@ -154,7 +122,6 @@ Do not edit the autogenerated section by hand. | 71 | [verified-optimization/CvxLean](https://github.com/verified-optimization/CvxLean) | Convex optimization modeling in Lean 4 | Apache-2.0 | 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 | 2026-03-29 | ✗ | | 69 | [dwrensha/maze](https://github.com/dwrensha/lean4-maze) | maze game encoded in Lean 4 syntax | Apache-2.0 | 2026-02-13 | ✓ | -| 69 | [sinhp/HoTTLean](https://github.com/sinhp/HoTTLean) | | Apache-2.0 | 2026-05-05 | – | | 68 | [SrGaabriel/soma-workspace](https://github.com/SrGaabriel/soma) | ⚗️ \| Soma is a general-purpose dependently-typed functional programming language powered by Interaction Nets with a min… | Apache-2.0 | 2026-04-28 | ✓ | | 68 | [starkware-libs/verification](https://github.com/starkware-libs/formal-proofs) | | Apache-2.0 | 2026-04-06 | ✗ | | 67 | [aripiprazole/rinha](https://github.com/aripiprazole/rinha) | 🧪 \| Rinha de Backend Lean4 | | 2026-04-11 | – | @@ -166,12 +133,9 @@ Do not edit the autogenerated section by hand. | 63 | [siddhartha-gadgil/saturn](https://github.com/siddhartha-gadgil/Saturn) | Experiments with SAT solvers with proofs in Lean 4 | MIT | 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 | 2026-04-26 | ✓ | | 62 | [leanprover/pantograph](https://github.com/leanprover/Pantograph) | (Mirror) A Machine-to-Machine Interaction System for Lean 4 | Apache-2.0 | 2026-04-26 | ✗ | -| 62 | [leanprover/Pantograph](https://github.com/leanprover/Pantograph) | (Mirror) A Machine-to-Machine Interaction System for Lean 4 | Apache-2.0 | 2026-04-26 | – | | 61 | [AlexKontorovich/Game](https://github.com/AlexKontorovich/RealAnalysisGame) | RealAnalysisGame | Apache-2.0 | 2026-04-14 | ✗ | -| 61 | [BoltonBailey/formal-snarks-project](https://github.com/BoltonBailey/formal-snarks-project) | A formal verification of Linear PCP SNARKs. | MIT | 2026-04-07 | – | | 61 | [BoltonBailey/formalSnarksProject](https://github.com/BoltonBailey/formal-snarks-project) | A formal verification of Linear PCP SNARKs. | MIT | 2026-04-07 | ✗ | | 61 | [kim-em/lean-training-data](https://github.com/kim-em/lean-training-data) | | Apache-2.0 | 2026-04-12 | ✓ | -| 61 | [kim-em/lean-training-data](https://github.com/kim-em/lean-training-data) | | Apache-2.0 | 2026-04-12 | – | | 61 | [sunblaze-ucb/verina](https://github.com/sunblaze-ucb/verina) | Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation o… | Apache-2.0 | 2026-04-28 | ✗ | | 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 | 2026-04-26 | ✓ | | 59 | [vihdzp/CombinatorialGames](https://github.com/vihdzp/combinatorial-games) | Combinatorial game library in Lean 4 | Apache-2.0 | 2026-04-19 | ✗ | @@ -179,14 +143,11 @@ Do not edit the autogenerated section by hand. | 57 | [leanprover-community/tutorials4](https://github.com/leanprover-community/tutorials4) | Lean 4 tutorial files | Apache-2.0 | 2026-04-19 | ✗ | | 56 | [leanprover/LeanSAT](https://github.com/leanprover/leansat) | This package provides an interface and foundation for verified SAT reasoning | Apache-2.0 | 2026-03-09 | ✗ | | 54 | [algebraic-dev/Http](https://github.com/algebraic-dev/http) | 🌐 \| HTTP primitives for Lean 4 | Apache-2.0 | 2026-03-30 | ✗ | -| 54 | [algebraic-dev/http](https://github.com/algebraic-dev/http) | 🌐 \| HTTP primitives for Lean 4 | Apache-2.0 | 2026-03-30 | – | -| 54 | [algebraic-dev/http](https://github.com/algebraic-dev/http) | 🌐 \| HTTP primitives for Lean 4 | Apache-2.0 | 2026-03-30 | – | | 53 | [haruhisa-enomoto/mathlib4-all-tactics](https://github.com/haruhisa-enomoto/mathlib4-all-tactics) | Markdown file of the list and explanations of all mathlib4 tactics | Apache-2.0 | 2025-11-28 | ✓ | | 53 | [joehendrix/lean-crypto](https://github.com/joehendrix/lean-crypto) | Cryptographic routines for the Lean 4 language | Apache-2.0 | 2026-04-14 | ✗ | | 52 | [plfa/plfl](https://github.com/plfa/plfl) | Programming Language Foundations in Lean | | 2026-05-04 | – | | 52 | [verse-lab/splean](https://github.com/verse-lab/splean) | Separation Logic Proofs in Lean | Apache-2.0 | 2026-04-06 | – | | 51 | [alexkeizer/qpf](https://github.com/alexkeizer/QPFTypes) | A WIP definitional (co)datatype package for Lean4 | Apache-2.0 | 2026-04-12 | ✗ | -| 51 | [alexkeizer/QPFTypes](https://github.com/alexkeizer/QPFTypes) | A WIP definitional (co)datatype package for Lean4 | Apache-2.0 | 2026-04-12 | – | | 50 | [verse-lab/Velvet](https://github.com/verse-lab/velvet) | An auto-active verifier embedded into Lean | Apache-2.0 | 2026-04-23 | ✗ | | 49 | [leanprover/KLR](https://github.com/leanprover/KLR) | A formalization of ML kernel languages | Apache-2.0 | 2026-04-29 | ✗ | | 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 | 2026-03-12 | ✗ | @@ -197,16 +158,12 @@ Do not edit the autogenerated section by hand. | 47 | [leanprover-community/SphereEversion](https://github.com/leanprover-community/sphere-eversion) | Formalization of the existence of sphere eversions | Apache-2.0 | 2026-03-30 | ✗ | | 47 | [RemyDegenne/BrownianMotion](https://github.com/RemyDegenne/brownian-motion) | Construction of a Brownian Motion in Lean | Apache-2.0 | 2026-04-22 | ✗ | | 45 | [GasStationManager/SafeVerify](https://github.com/GasStationManager/SafeVerify) | A Lean4 script for robustly verifying submitted proofs of theorems and implementations of functions | Apache-2.0 | 2026-04-23 | ✗ | -| 45 | [hanwenzhu/LeanArchitect](https://github.com/hanwenzhu/LeanArchitect) | LeanArchitect extracts a blueprint directly from Lean source. | Apache-2.0 | 2026-05-04 | – | | 45 | [leanprover-community/mathport](https://github.com/leanprover-community/mathport) | Mathport is a tool for porting Lean3 projects to Lean4 | Apache-2.0 | 2026-04-29 | ✗ | -| 45 | [leanprover-community/mathport](https://github.com/leanprover-community/mathport) | Mathport is a tool for porting Lean3 projects to Lean4 | Apache-2.0 | 2026-04-29 | – | | 45 | [opencompl/veir](https://github.com/opencompl/veir) | Verified Intermediate Representation | | 2026-05-09 | – | | 44 | [fpvandoorn/LeanCourse](https://github.com/fpvandoorn/LeanCourse24) | Bonn Lean course for winter 24/25 | Apache-2.0 | 2026-04-12 | ✗ | | 44 | [hanwenzhu/LeanArchitect](https://github.com/hanwenzhu/LeanArchitect) | LeanArchitect extracts a blueprint directly from Lean source. | Apache-2.0 | 2026-04-24 | ✓ | | 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 | 2026-04-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 | 2026-04-09 | – | | 43 | [leanprover/leansqlite](https://github.com/leanprover/leansqlite) | SQLite bindings for Lean | Apache-2.0 | 2026-04-25 | ✓ | -| 43 | [leanprover/leansqlite](https://github.com/leanprover/leansqlite) | SQLite bindings for Lean | Apache-2.0 | 2026-04-25 | – | | 43 | [verse-lab/ssreflect](https://github.com/verse-lab/lean-ssr) | LeanSSR: an SSReflect-Like Tactic Language for Lean | Apache-2.0 | 2026-02-14 | ✗ | | 42 | [argumentcomputer/Wasm.lean](https://github.com/argumentcomputer/Wasm.lean) | A WebAssembly implementation in Lean4 | MIT | 2026-04-16 | ✗ | | 41 | [DSLstandard/Lean4-FFI-Programming-Tutorial-GLFW](https://github.com/DSLstandard/Lean4-FFI-Programming-Tutorial-GLFW) | Lean4 Tutorial/Notes on creating FFI bindings with GLFW as an example. | MIT | 2026-05-07 | – | @@ -214,13 +171,11 @@ Do not edit the autogenerated section by hand. | 41 | [lengyijun/goldbach_tm](https://github.com/lengyijun/goldbach_tm) | Goldbach conjecture = 25-state turing machine | | 2026-04-25 | – | | 41 | [riccardobrasca/FLT3](https://github.com/riccardobrasca/flt3) | Proof in Lean of Fermat Last Theorem for exponent 3 | Apache-2.0 | 2026-02-26 | ✗ | | 41 | [riyazahuja/ImProver](https://github.com/riyazahuja/ImProver) | ImProver: Agent-Based Automated Proof Optimization | | 2026-03-18 | – | -| 41 | [riyazahuja/ImProver](https://github.com/riyazahuja/ImProver) | ImProver: Agent-Based Automated Proof Optimization | | 2026-03-18 | – | | 40 | [AxiomMath/FelConjecture](https://github.com/AxiomMath/fel-polynomial) | Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups" | MIT | 2026-04-07 | ✗ | | 40 | [T-Brick/c0deine](https://github.com/T-Brick/c0deine) | Reference compiler for c0 | | 2026-04-07 | – | | 39 | [djvelleman/htpi](https://github.com/djvelleman/HTPILeanPackage) | Lean package for "How To Prove It with Lean", a companion to the book "How To Prove It" | Apache-2.0 | 2026-04-10 | ✗ | | 39 | [leanprover/TensorLib](https://github.com/leanprover/TensorLib) | A verified tensor library in Lean | Apache-2.0 | 2026-04-15 | ✗ | | 38 | [astrainfinita/algorithm](https://github.com/astrainfinita/Algorithm) | Verified efficient algorithms in Lean4. | Apache-2.0 | 2026-04-21 | ✗ | -| 38 | [astrainfinita/Algorithm](https://github.com/astrainfinita/Algorithm) | Verified efficient algorithms in Lean4. | Apache-2.0 | 2026-04-21 | – | | 38 | [Verified-zkEVM/CompPoly](https://github.com/Verified-zkEVM/CompPoly) | A computable model of Polynomials in Lean. | Apache-2.0 | 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 | 2026-04-21 | – | | 37 | [project-numina/lib](https://github.com/project-numina/LeanGeo) | Solving Competition Geometry Problems in Lean | MIT | 2026-04-25 | ✗ | @@ -228,13 +183,10 @@ Do not edit the autogenerated section by hand. | 36 | [cmu-l3/ntp-toolkit](https://github.com/cmu-l3/ntp-toolkit) | Neural theorem proving toolkit: data extraction tools for Lean 4 | | 2026-03-12 | – | | 36 | [dwrensha/tryAtEachStep](https://github.com/dwrensha/tryAtEachStep) | Try a tactic at each step in a Lean proof. | Apache-2.0 | 2026-04-05 | ✓ | | 35 | [argumentcomputer/Megaparsec.lean](https://github.com/argumentcomputer/Megaparsec.lean) | Lean 4 port of Megaparsec | MIT | 2026-03-08 | ✗ | -| 35 | [argumentcomputer/Megaparsec.lean](https://github.com/argumentcomputer/Megaparsec.lean) | Lean 4 port of Megaparsec | MIT | 2026-03-08 | – | -| 35 | [argumentcomputer/Megaparsec.lean](https://github.com/argumentcomputer/Megaparsec.lean) | Lean 4 port of Megaparsec | MIT | 2026-03-08 | – | | 35 | [kmill/LeanTeX](https://github.com/kmill/LeanTeX) | Lean 4 library for pretty printing expressions as LaTeX | Apache-2.0 | 2026-03-23 | ✗ | | 34 | [fpvandoorn/LeanCourse23](https://github.com/fpvandoorn/LeanCourse23) | | Apache-2.0 | 2025-10-03 | – | | 34 | [google-deepmind/imo](https://github.com/google-deepmind/formal-imo) | Lean formalizations of IMO problem statements | Apache-2.0 | 2026-04-29 | ✗ | | 34 | [leanprover/lean4checker](https://github.com/leanprover/lean4checker) | Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel. | Apache-2.0 | 2026-03-25 | ✓ | -| 34 | [leanprover/lean4export](https://github.com/leanprover/lean4export) | Plain-text declaration export for Lean 4 | Apache-2.0 | 2026-05-08 | – | | 34 | [nomeata/calcify](https://github.com/nomeata/lean-calcify) | | Apache-2.0 | 2026-04-13 | ✓ | | 34 | [WuProver/groebner](https://github.com/WuProver/groebner_proj) | Formalization of Gröbner basis theory in Lean4 (WIP) | Apache-2.0 | 2026-04-14 | ✗ | | 33 | [lambdaclass/trzk](https://github.com/lambdaclass/truth_research_zk) | Verified Optimizing Compiler for Cryptographic Primitives | MIT | 2026-04-29 | ✗ | @@ -244,14 +196,11 @@ Do not edit the autogenerated section by hand. | 33 | [vihdzp/Rubik](https://github.com/vihdzp/rubik-lean4) | Lean 4 formalization of Rubik's cubes | Apache-2.0 | 2026-04-13 | ✗ | | 32 | [facebookresearch/wybecoder](https://github.com/facebookresearch/wybecoder) | WybeCoder Verified Generation of Imperative Code with LLMs | | 2026-05-02 | – | | 32 | [haskell-spec/haskell-spec](https://github.com/haskell-spec/haskell-spec) | Formal specification of the Haskell Language Report | MIT | 2026-03-04 | ✓ | -| 32 | [haskell-spec/haskell-spec](https://github.com/haskell-spec/haskell-spec) | Formal specification of the Haskell Language Report | MIT | 2026-03-04 | – | | 32 | [JamesGallicchio/leancolls](https://github.com/JamesGallicchio/LeanColls) | WIP collections library for Lean 4 | Apache-2.0 | 2025-05-08 | ✗ | | 32 | [leanprover-community/LeanSearchClient](https://github.com/leanprover-community/LeanSearchClient) | Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services) | Apache-2.0 | 2026-04-07 | ✓ | -| 32 | [leanprover-community/LeanSearchClient](https://github.com/leanprover-community/LeanSearchClient) | Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services) | Apache-2.0 | 2026-04-07 | – | | 32 | [marcusrossel/VerifiedCompiler](https://github.com/marcusrossel/verified-compiler) | A toy example of a verified compiler. | MIT | 2026-04-07 | ✓ | | 32 | [rkirov/category-theory-in-context-lean](https://github.com/rkirov/category-theory-in-context-lean) | Lean Companion to the Category Theory in Context textbook by Emily Riehl | MIT | 2026-04-19 | ✗ | | 31 | [dwrensha/Chess](https://github.com/dwrensha/Chess.lean) | Chess in Lean 4 | Apache-2.0 | 2026-04-15 | ✗ | -| 31 | [dwrensha/Chess.lean](https://github.com/dwrensha/Chess.lean) | Chess in Lean 4 | Apache-2.0 | 2026-04-15 | – | | 31 | [hhu-adam/Robo](https://github.com/hhu-adam/Robo) | A game for learning Lean 4 where a cute little smart-elf joins you on your exploration of the Leaniverse. | Apache-2.0 | 2026-04-25 | – | | 31 | [lftcm2023/lftcm2023](https://github.com/lftcm2023/lftcm2023) | | | 2026-04-19 | – | | 31 | [opencompl/sail-riscv-lean](https://github.com/opencompl/sail-riscv-lean) | | | 2026-05-09 | – | @@ -261,10 +210,8 @@ Do not edit the autogenerated section by hand. | 30 | [rahul3613/proofNet-lean4](https://github.com/rahul3613/ProofNet-lean4) | ProofNet dataset ported into Lean 4 | MIT | 2026-04-29 | ✗ | | 30 | [T-Brick/wasm](https://github.com/T-Brick/lean-wasm) | Formalising the WASM spec in Lean | GPL-3.0 | 2026-03-18 | ✗ | | 29 | [dignissimus/Untangle](https://github.com/dignissimus/Untangle) | Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4 | | 2026-01-28 | – | -| 29 | [GaloisInc/zkLean](https://github.com/GaloisInc/zkLean) | zkLean is a domain specific language (DSL) in Lean for specifying zero-knowledge statements | BSD-3-Clause | 2026-05-04 | – | | 29 | [girving/ray](https://github.com/girving/ray) | Formalizing results about the Mandelbrot set in Lean | Apache-2.0 | 2026-02-17 | ✗ | | 29 | [KislyjKisel/raylib](https://github.com/KislyjKisel/Raylib.lean) | Raylib bindings for Lean4 | BSD-3-Clause | 2026-02-24 | ✗ | -| 29 | [KislyjKisel/Raylib.lean](https://github.com/KislyjKisel/Raylib.lean) | Raylib bindings for Lean4 | BSD-3-Clause | 2026-02-24 | – | | 29 | [leanprover/human-eval-lean](https://github.com/leanprover/human-eval-lean) | Hand-written verified Lean solutions for the HumanEval benchmark | MIT | 2026-04-27 | – | | 29 | [scottnarmstrong/DeGiorgi](https://github.com/scottnarmstrong/DeGiorgi) | Lean 4 formalization of De Giorgi-Nash-Moser theory | Apache-2.0 | 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 | 2026-04-27 | ✓ | @@ -273,7 +220,6 @@ Do not edit the autogenerated section by hand. | 28 | [sinhp/Poly](https://github.com/sinhp/Poly) | A Lean4 Formalization of Polynomial Functors | | 2026-04-26 | – | | 27 | [MixedMatched/formalizing-game-theory](https://github.com/MixedMatched/formalizing-game-theory) | Example formalization of Game Theoretic concepts in Lean | | 2026-03-11 | – | | 27 | [xubaiw/Socket.lean](https://github.com/xubaiw/Socket.lean) | A toy implementation of socket programming for Lean 4. | Apache-2.0 | 2026-03-05 | – | -| 27 | [xubaiw/Socket.lean](https://github.com/xubaiw/Socket.lean) | A toy implementation of socket programming for Lean 4. | Apache-2.0 | 2026-03-05 | – | | 26 | [djvelleman/STG4](https://github.com/djvelleman/STG4) | Set Theory Game | | 2026-05-01 | – | | 26 | [frenzymath/reap](https://github.com/frenzymath/reap) | General neural tactic for Lean 4 | Apache-2.0 | 2026-04-29 | ✓ | | 26 | [kiranandcode/LeanTeX](https://github.com/kiranandcode/LeanTeX) | Write LaTeX presentations directly from Lean4~ | | 2026-04-27 | – | @@ -289,7 +235,6 @@ Do not edit the autogenerated section by hand. | 25 | [sciencraft/LeanCat](https://github.com/sciencraft/LeanCat) | Lean4 benchmark on 1 category. | MIT | 2026-04-24 | ✗ | | 25 | [Seasawher/mdgen](https://github.com/Seasawher/mdgen) | Tool to generate markdown files from lean files. | MIT | 2026-04-20 | ✓ | | 24 | [Anderssorby/SDL](https://github.com/Anderssorby/SDL.lean) | SDL2 bindings for lean | MIT | 2026-02-24 | ✓ | -| 24 | [Anderssorby/SDL.lean](https://github.com/Anderssorby/SDL.lean) | SDL2 bindings for lean | MIT | 2026-02-24 | – | | 24 | [AxiomMath/parity-differential](https://github.com/AxiomMath/parity-differential) | Lean formalizations for the paper "Parity of k-differentials in genus zero and one" | MIT | 2026-04-02 | – | | 24 | [funexists/raylean](https://github.com/funexists/raylean) | Lean4 bindings for raylib | Zlib | 2026-04-25 | ✗ | | 24 | [lecopivo/HouLean](https://github.com/lecopivo/HouLean) | Lean 4 as a scripting language in Houdini | | 2026-04-27 | – | @@ -299,14 +244,11 @@ Do not edit the autogenerated section by hand. | 23 | [ATOMSLab/LeanLJ](https://github.com/ATOMSLab/LeanLJ) | Lennard Jones in Lean | Apache-2.0 | 2026-04-29 | ✗ | | 23 | [digama0/mm-lean4](https://github.com/digama0/mm-lean4) | Lean 4 Metamath verifier | | 2026-02-20 | – | | 23 | [FormalSAT/trestle](https://github.com/FormalSAT/trestle) | | Apache-2.0 | 2026-03-25 | ✗ | -| 23 | [FormalSAT/trestle](https://github.com/FormalSAT/trestle) | | Apache-2.0 | 2025-12-12 | – | | 23 | [hargoniX/socket](https://github.com/hargoniX/socket.lean) | sockets for Lean 4 | MIT | 2026-04-14 | ✗ | -| 23 | [hargoniX/socket.lean](https://github.com/hargoniX/socket.lean) | sockets for Lean 4 | MIT | 2026-04-14 | – | | 23 | [math-inc/Erdos1196](https://github.com/math-inc/Erdos1196) | | Apache-2.0 | 2026-05-09 | – | | 23 | [paulch42/leanSpec](https://github.com/paulch42/lean-spec) | Program Specification in Lean 4 | Apache-2.0 | 2026-04-21 | ✗ | | 23 | [pitmonticone/ItaLean](https://github.com/pitmonticone/ItaLean2025) | Repository hosting the resources for the conference "ItaLean 2025", held in Bologna, Italy, December 9–12, 2025. | Apache-2.0 | 2026-03-24 | ✗ | | 23 | [vltanh/lean4-analysis-tao](https://github.com/vltanh/lean4-analysis-tao) | Formalization of "Analysis I" by Terence Tao | MIT | 2026-04-17 | ✗ | -| 22 | [ATOMSLab/LeanLJ](https://github.com/ATOMSLab/LeanLJ) | Lennard Jones in Lean | Apache-2.0 | 2026-05-09 | – | | 22 | [BartoszPiotrowski/lean-premise-selection](https://github.com/BartoszPiotrowski/lean-premise-selection) | | | 2025-10-09 | – | | 22 | [brendanzab/lean-holes](https://github.com/brendanzab/lean-holes) | Interactive holes for Lean 4 | | 2025-06-17 | – | | 22 | [opencompl/fp-lean](https://github.com/opencompl/fp-lean) | Floating Point Semantics Mechanization for Lean | Apache-2.0 | 2026-04-29 | ✗ | @@ -314,7 +256,6 @@ Do not edit the autogenerated section by hand. | 22 | [VCA-EPFL/graphiti](https://github.com/VCA-EPFL/graphiti) | Verified graph rewriting (for dataflow circuits). | Apache-2.0 | 2026-04-29 | ✓ | | 22 | [Verilean/Hesper](https://github.com/Verilean/hesper) | Verified GPU programming framework for Lean 4. Write type-safe WebGPU shaders with formal verification, hardware-accele… | Apache-2.0 | 2026-04-25 | ✗ | | 22 | [YaelDillies/APAP](https://github.com/YaelDillies/apap) | Formalisation of the Kelley-Meka bound on Roth numbers | Apache-2.0 | 2026-04-27 | ✗ | -| 22 | [YaelDillies/apap](https://github.com/YaelDillies/apap) | Formalisation of the Kelley-Meka bound on Roth numbers | Apache-2.0 | 2026-05-04 | – | | 21 | [frenzymath/Anderson-Conjecture](https://github.com/frenzymath/Anderson-Conjecture) | | Apache-2.0 | 2026-05-07 | – | | 21 | [kiranandcode/cleango](https://github.com/kiranandcode/cleango) | Bindings to libclingo for the lean4 prover and programming language! | MIT | 2026-01-12 | – | | 21 | [leanprover/SHerLOC](https://github.com/leanprover/SHerLOC) | A StableHLO analyzer in Lean | Apache-2.0 | 2026-02-24 | ✗ | @@ -342,18 +283,15 @@ Do not edit the autogenerated section by hand. | 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 | 2026-04-20 | ✓ | | 18 | [google-deepmind/putnam_like](https://github.com/google-deepmind/formal-putnam-like) | Lean formalizations of Putnam-like problems | Apache-2.0 | 2026-04-23 | ✗ | -| 18 | [katydid/regex-deriv-lean](https://github.com/katydid/regex-deriv-lean) | Proofs written in Lean4 for the core katydid validation algorithm | Apache-2.0 | 2026-02-19 | – | | 18 | [katydid/regexderiv](https://github.com/katydid/regex-deriv-lean) | Proofs written in Lean4 for the core katydid validation algorithm | Apache-2.0 | 2026-02-19 | ✗ | | 18 | [rzeta0/Lean-First-Steps](https://github.com/rzeta0/Lean-First-Steps) | | GPL-2.0 | 2025-09-04 | – | | 18 | [Trequetrum/Game](https://github.com/Trequetrum/lean4game-logic) | Make/Encode some basic logic puzzles | MIT | 2026-01-18 | ✗ | | 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 | 2026-04-22 | – | | 17 | [658060/topos](https://github.com/658060/topos) | Topos theory in Lean 4 | | 2026-02-20 | – | | 17 | [adomani/mA4N1](https://github.com/adomani/MA4N1_Theorem_proving_with_Lean) | MA4N1 Theorem Proving with Lean | MIT | 2025-12-19 | ✗ | -| 17 | [adomani/MA4N1_Theorem_proving_with_Lean](https://github.com/adomani/MA4N1_Theorem_proving_with_Lean) | MA4N1 Theorem Proving with Lean | MIT | 2025-12-19 | – | | 17 | [auto-res/FoML](https://github.com/auto-res/lean-rademacher) | Lean Formalization of Generalization Error Bound by Rademacher Complexity | MIT | 2026-04-28 | ✗ | | 17 | [digama0/ast_export](https://github.com/digama0/ast_export) | AST export from Lean 4 | Apache-2.0 | 2026-01-28 | – | | 17 | [dwrensha/rupert](https://github.com/dwrensha/Rupert.lean) | Formalization of the Rupert Problem for convex polyhedra. | Apache-2.0 | 2026-04-05 | ✗ | -| 17 | [dwrensha/Rupert.lean](https://github.com/dwrensha/Rupert.lean) | Formalization of the Rupert Problem for convex polyhedra. | Apache-2.0 | 2026-04-05 | – | | 17 | [ElifUskuplu/stlc](https://github.com/ElifUskuplu/Stlc_deBruijn) | Simply Typed Lambda Calculus with de Bruijn indices | MIT | 2026-03-03 | ✗ | | 17 | [fpvandoorn/LeanCourse25](https://github.com/fpvandoorn/LeanCourse25) | | Apache-2.0 | 2026-02-06 | ✗ | | 17 | [kovach/etch](https://github.com/kovach/etch) | | Apache-2.0 | 2026-04-11 | ✗ | @@ -366,7 +304,6 @@ Do not edit the autogenerated section by hand. | 17 | [UCSCFormalMethods/LeanLTL](https://github.com/UCSCFormalMethods/LeanLTL) | A unifying framework for linear temporal logics in Lean | | 2026-04-12 | – | | 17 | [ValorZard/SDL3](https://github.com/ValorZard/lean-sdl3) | | MIT | 2026-02-24 | ✓ | | 17 | [Vilin97/Clawristotle](https://github.com/Vilin97/Clawristotle) | OpenClaw-style theorem proving | | 2026-04-28 | – | -| 17 | [Vilin97/Clawristotle](https://github.com/Vilin97/Clawristotle) | OpenClaw-style theorem proving | | 2026-04-28 | – | | 16 | [algebraic-dev/melp](https://github.com/algebraic-dev/melp) | 🕸️ \| Incomplete HTTP/1.1 Server in Lean4 for Rinha de backends | | 2024-08-14 | – | | 16 | [alok/LeanPlot](https://github.com/alok/LeanPlot) | Interactive React-powered charting library for Lean 4 in VS Code's infoview | Apache-2.0 | 2026-02-28 | ✗ | | 16 | [arthurpaulino/FxyLang](https://github.com/arthurpaulino/FxyLang) | | Apache-2.0 | 2025-10-05 | ✓ | @@ -388,11 +325,7 @@ Do not edit the autogenerated section by hand. | 15 | [aetilley/banach-tarski](https://github.com/aetilley/banach-tarski) | A formalization of the Banach-Tarski theorem in Lean | Apache-2.0 | 2026-05-01 | – | | 15 | [apnelson1/Matroid](https://github.com/apnelson1/Matroid) | | Apache-2.0 | 2026-04-29 | ✗ | | 15 | [argumentcomputer/RustFFI.lean](https://github.com/argumentcomputer/RustFFI.lean) | Template for Lean<->Rust FFI | MIT | 2026-03-26 | ✗ | -| 15 | [argumentcomputer/RustFFI.lean](https://github.com/argumentcomputer/RustFFI.lean) | Template for Lean<->Rust FFI | MIT | 2026-03-26 | – | -| 15 | [argumentcomputer/RustFFI.lean](https://github.com/argumentcomputer/RustFFI.lean) | Template for Lean<->Rust FFI | MIT | 2026-03-26 | – | -| 15 | [argumentcomputer/RustFFI.lean](https://github.com/argumentcomputer/RustFFI.lean) | Template for Lean<->Rust FFI | MIT | 2026-03-26 | – | | 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 | 2026-04-22 | ✗ | -| 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 | 2026-04-22 | – | | 15 | [frenzymath/Archon-FirstProof-Results](https://github.com/frenzymath/Archon-FirstProof-Results) | | Apache-2.0 | 2026-04-11 | – | | 15 | [hanwenzhu/premise-selection](https://github.com/hanwenzhu/premise-selection) | | Apache-2.0 | 2026-03-28 | – | | 15 | [hargoniX/pfmt](https://github.com/hargoniX/pfmt) | A basic Lean implementation of https://arxiv.org/pdf/2310.01530.pdf | | 2026-01-26 | – | @@ -405,19 +338,16 @@ Do not edit the autogenerated section by hand. | 14 | [ammkrn/timelib](https://github.com/ammkrn/timelib) | A date and time library for Lean 4 | Apache-2.0 | 2026-01-30 | ✗ | | 14 | [andrejbauer/partial-combinatory-algebras](https://github.com/andrejbauer/partial-combinatory-algebras) | A Lean 4 formalization of partial combinatory algebras. | MIT | 2025-06-23 | ✗ | | 14 | [argumentcomputer/FFaCiL.lean](https://github.com/argumentcomputer/FFaCiL.lean) | Finite Fields and Curves in Lean | MIT | 2025-12-17 | ✗ | -| 14 | [argumentcomputer/FFaCiL.lean](https://github.com/argumentcomputer/FFaCiL.lean) | Finite Fields and Curves in Lean | MIT | 2025-12-17 | – | | 14 | [arthurpaulino/LeanREPL](https://github.com/arthurpaulino/LeanREPL) | | Apache-2.0 | 2025-12-10 | ✓ | | 14 | [bergmannjg/Curl](https://github.com/bergmannjg/leanCurl) | Lean 4 bindings to libcurl | MIT | 2026-03-31 | ✓ | | 14 | [Deducteam/Lean4Less](https://github.com/Deducteam/Lean4Less) | A translation framework for eliminating definitional equalities in Lean | | 2026-02-11 | – | | 14 | [FormalizedFormalLogic/arithmetization](https://github.com/FormalizedFormalLogic/Arithmetization) | Formalization of Arithmetization of Mathematics/Metamathematics | Apache-2.0 | 2026-04-08 | ✗ | -| 14 | [FormalizedFormalLogic/Arithmetization](https://github.com/FormalizedFormalLogic/Arithmetization) | Formalization of Arithmetization of Mathematics/Metamathematics | Apache-2.0 | 2026-04-08 | – | | 14 | [FWuermse/Postgres](https://github.com/FWuermse/lean-postgres) | | Apache-2.0 | 2026-01-30 | ✗ | | 14 | [iasakura/lean-yjs](https://github.com/iasakura/lean-yjs) | Lean-Yjs: Formal Verification of Yjs Integration Algorithm | MIT | 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 | 2026-04-28 | ✓ | | 14 | [math-inc/FormalQualBench](https://github.com/math-inc/FormalQualBench) | | Apache-2.0 | 2026-03-21 | ✓ | | 14 | [sven-manthe/borel_det](https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean) | | Apache-2.0 | 2026-02-26 | ✗ | | 13 | [arademaker/fad](https://github.com/arademaker/fad) | Functional Algorithms Design | Apache-2.0 | 2026-03-09 | ✗ | -| 13 | [arademaker/fad](https://github.com/arademaker/fad) | Functional Algorithms Design | Apache-2.0 | 2026-03-09 | – | | 13 | [AviCraimer/relational-calculus-library-lean4](https://github.com/AviCraimer/relational-calculus-library-lean4) | | | 2026-05-04 | – | | 13 | [brettkoonce/lean4-jax](https://github.com/brettkoonce/lean4-mlir) | Use Lean4 to build and train image recognition networks in MLIR. | BSD-3-Clause | 2026-04-29 | ✓ | | 13 | [eshelyaron/bdd](https://github.com/eshelyaron/lean4-bdd) | Binary Decision Diagrams in Lean 4 | Apache-2.0 | 2026-03-17 | ✗ | @@ -440,13 +370,10 @@ Do not edit the autogenerated section by hand. | 12 | [ah1112/synthetic_euclid_4](https://github.com/ah1112/synthetic_euclid_4) | | Apache-2.0 | 2026-02-16 | ✗ | | 12 | [anoma/goose](https://github.com/anoma/goose-lean) | GOOSE in Lean4 | ISC | 2025-12-19 | ✗ | | 12 | [argumentcomputer/Http.lean](https://github.com/argumentcomputer/Http.lean) | Basic Http functionality in Lean (unfinished) | MIT | 2025-12-02 | ✗ | -| 12 | [argumentcomputer/Http.lean](https://github.com/argumentcomputer/Http.lean) | Basic Http functionality in Lean (unfinished) | MIT | 2025-12-02 | – | -| 12 | [argumentcomputer/Http.lean](https://github.com/argumentcomputer/Http.lean) | Basic Http functionality in Lean (unfinished) | MIT | 2025-12-02 | – | | 12 | [b-mehta/AharoniKorman](https://github.com/b-mehta/AharoniKorman) | Disproof of the Aharoni–Korman conjecture | Apache-2.0 | 2025-12-01 | ✗ | | 12 | [Bergschaf/banach_tarski](https://github.com/Bergschaf/banach-tarski) | | Apache-2.0 | 2026-01-19 | ✗ | | 12 | [chenjulang/rubikcubegroup](https://github.com/chenjulang/rubikcubegroup) | rubikcubegroup魔方定理证明+视频分享。discuss here: https://lean4daydayup.zulipchat.com/join/45reytdk5yv7t7sheywhulw3/ | | 2025-06-19 | – | | 12 | [crabbo-rave/Soup](https://github.com/crabbo-rave/Soup) | Extra and extended datatypes for Lean 4 | | 2025-10-01 | – | -| 12 | [crabbo-rave/Soup](https://github.com/crabbo-rave/Soup) | Extra and extended datatypes for Lean 4 | | 2025-10-01 | – | | 12 | [dannypsnl/violet](https://github.com/dannypsnl/violet-legacy) | A programming language, half theorem prover | BSD-3-Clause | 2024-09-20 | ✗ | | 12 | [fpvandoorn/bonnAnalysis](https://github.com/fpvandoorn/BonnAnalysis) | repository for the collaborative formalization seminar in Analysis in Bonn | Apache-2.0 | 2026-04-01 | ✗ | | 12 | [hhu-adam/i18n](https://github.com/hhu-adam/lean-i18n) | i18n library for Lean. | Apache-2.0 | 2026-04-25 | ✓ | @@ -471,7 +398,6 @@ Do not edit the autogenerated section by hand. | 11 | [AxiomMath/Deadends](https://github.com/AxiomMath/dead-ends) | | MIT | 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 | 2026-04-07 | – | | 11 | [BRonen/sqlite](https://github.com/BRonen/sqlite-lean) | Sqlite3 bindings for lean4 | MIT | 2025-11-19 | ✓ | -| 11 | [BRonen/sqlite-lean](https://github.com/BRonen/sqlite-lean) | Sqlite3 bindings for lean4 | MIT | 2025-11-19 | – | | 11 | [dupuisf/BibtexQuery](https://github.com/dupuisf/BibtexQuery) | A simple command-line bibtex query utility written in Lean 4 | Apache-2.0 | 2026-04-17 | ✓ | | 11 | [ecyrbe/lean-units](https://github.com/ecyrbe/lean-units) | lean physical unit system, SI international | MIT | 2026-01-10 | ✗ | | 11 | [GasStationManager/ArtificialAlgorithms](https://github.com/GasStationManager/ArtificialAlgorithms) | Verified algorithms in Lean, implemented and proved by AIs | Apache-2.0 | 2026-04-28 | ✗ | @@ -480,7 +406,6 @@ Do not edit the autogenerated section by hand. | 11 | [ImperialCollegeLondon/M1F-explained](https://github.com/ImperialCollegeLondon/M1F-explained) | A computer formalisation of parts of Martin Liebeck's book "a concise introduction to pure mathematics" | Apache-2.0 | 2025-05-29 | ✗ | | 11 | [Izzimach/pteffects](https://github.com/Izzimach/EffSpec-lean) | Effect monads with specifications (DIjkstra Monads) in Lean 4 | MIT | 2025-06-19 | ✗ | | 11 | [leanprover-community/mathlib3port](https://github.com/leanprover-community/mathlib3port) | Synport output from mathport for mathlib3 | | 2025-08-15 | – | -| 11 | [leanprover-community/mathlib3port](https://github.com/leanprover-community/mathlib3port) | Synport output from mathport for mathlib3 | | 2025-08-15 | – | | 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 | 2026-04-27 | – | | 11 | [mhuisi/Uniq](https://github.com/mhuisi/Uniq) | Static Uniqueness Analysis for the Lean 4 Theorem Prover | MIT | 2026-01-09 | ✗ | @@ -501,10 +426,8 @@ Do not edit the autogenerated section by hand. | 10 | [DavePearce/LeanEVM](https://github.com/DavePearce/LeanEVM) | A toy implementation of the EVM in Lean4. | Apache-2.0 | 2024-05-29 | ✗ | | 10 | [gdncc/cryptography](https://github.com/gdncc/Cryptography) | Lean 4 programming language and theorem prover cryptography experiments | MIT | 2026-02-13 | ✓ | | 10 | [hargoniX/Flame](https://github.com/hargoniX/Flame) | | MIT | 2025-10-09 | ✗ | -| 10 | [hargoniX/Flame](https://github.com/hargoniX/Flame) | | MIT | 2025-10-09 | – | | 10 | [hrmacbeth/metaprogramming](https://github.com/hrmacbeth/metaprogramming) | Tutorials for metaprogramming in Lean | | 2026-04-01 | – | | 10 | [ianjauslin-rutgers/pythagoras4](https://github.com/ianjauslin-rutgers/pythagoras4) | Many proofs of the Pythagoras theorem - Lean 4 | | 2026-01-09 | – | -| 10 | [katydid/regex-deriv-reproving-agda-in-lean](https://github.com/katydid/regex-deriv-reproving-agda-in-lean) | Symbolic and Automatic Differentiation of Languages in Lean | Apache-2.0 | 2025-05-08 | – | | 10 | [katydid/sadol](https://github.com/katydid/regex-deriv-reproving-agda-in-lean) | Symbolic and Automatic Differentiation of Languages in Lean | Apache-2.0 | 2025-05-09 | ✓ | | 10 | [kebekus/VD](https://github.com/kebekus/ProjectVD) | Formalizing Value Distribution Theory | Apache-2.0 | 2026-04-29 | ✓ | | 10 | [Kiiyya/lean-wgpu](https://github.com/Kiiyya/lean-wgpu) | | | 2026-04-10 | – | @@ -523,7 +446,6 @@ Do not edit the autogenerated section by hand. | 10 | [urkud/DeRhamCohomology](https://github.com/urkud/DeRhamCohomology) | Formalization of de Rham cohomologies of a smooth manifold | | 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 | 2026-04-29 | ✗ | | 10 | [YaelDillies/gibbs-measure](https://github.com/YaelDillies/gibbs-measure) | ASCI Summer Research Lean | Apache-2.0 | 2026-04-05 | – | -| 10 | [YaelDillies/gibbs-measure](https://github.com/YaelDillies/gibbs-measure) | ASCI Summer Research Lean | Apache-2.0 | 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 | 2026-04-10 | ✗ | | 10 | [ykonstant1/InfinitePrimes](https://github.com/ykonstant1/InfinitePrimes) | A proof of the infinitude of primes in Lean 4 from first principles | | 2025-04-20 | – | | 9 | [adamtopaz/NodeGraph](https://github.com/adamtopaz/NodeGraph) | | Apache-2.0 | 2025-05-20 | ✗ | @@ -532,11 +454,9 @@ Do not edit the autogenerated section by hand. | 9 | [ammkrn/printiest](https://github.com/ammkrn/printiest) | A pretty printer for Lean 4 | Apache-2.0 | 2026-03-15 | ✗ | | 9 | [argumentcomputer/Lurk.lean](https://github.com/argumentcomputer/Lurk.lean) | A Lean 4 implementation of the Lurk Language for recursive zkSNARKS | MIT | 2026-01-30 | ✗ | | 9 | [argumentcomputer/YatimaStdLib](https://github.com/argumentcomputer/YatimaStdLib.lean) | | MIT | 2026-02-24 | ✗ | -| 9 | [argumentcomputer/YatimaStdLib.lean](https://github.com/argumentcomputer/YatimaStdLib.lean) | | MIT | 2026-02-24 | – | | 9 | [arthurpaulino/LeanMusic](https://github.com/arthurpaulino/LeanMusic) | | Apache-2.0 | 2025-10-01 | ✓ | | 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 | 2026-04-23 | – | | 9 | [b-mehta/PrimeCert](https://github.com/b-mehta/PrimeCert) | Formal prime certificates in Lean 4 | MIT | 2026-04-29 | – | -| 9 | [b-mehta/PrimeCert](https://github.com/b-mehta/PrimeCert) | Formal prime certificates in Lean 4 | MIT | 2026-04-29 | – | | 9 | [Beneficial-AI-Foundation/FloatSpec](https://github.com/Beneficial-AI-Foundation/FloatSpec) | Formally Verified Float Implementation with lean4 | Apache-2.0 | 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 | 2026-04-19 | ✗ | | 9 | [enricozb/logic](https://github.com/enricozb/logic) | Lean 4 logic | | 2025-02-06 | – | @@ -544,7 +464,6 @@ Do not edit the autogenerated section by hand. | 9 | [goens/lost-pop-lean](https://github.com/goens/lost-pop-lean) | POP Memory Model in Lean | MIT | 2026-04-20 | ✓ | | 9 | [google-deepmind/minif2f](https://github.com/google-deepmind/miniF2F) | A fork of openai/miniF2F adapted to Lean 4, with corrections to formalizations and informal descriptions. for human rea… | Apache-2.0 | 2026-04-29 | ✗ | | 9 | [Hagb/lean-groebner](https://github.com/Hagb/lean-groebner) | Lean4 formalization of Gröbner basis (WIP) | Apache-2.0 | 2025-07-28 | ✗ | -| 9 | [Hagb/lean-groebner](https://github.com/Hagb/lean-groebner) | Lean4 formalization of Gröbner basis (WIP) | Apache-2.0 | 2025-07-28 | – | | 9 | [jaalonso/Calculemus2](https://github.com/jaalonso/Calculemus2) | Proof exercises in Lean4 and Isabelle/HOL | GPL-3.0 | 2026-04-27 | ✓ | | 9 | [jthulhu/2ltt](https://github.com/jthulhu/2ltt) | | | 2026-05-01 | – | | 9 | [LeanMachineLearning/LeanMachineLearning](https://github.com/LeanMachineLearning/LML) | The Lean Machine Learning Library | Apache-2.0 | 2026-04-27 | ✗ | @@ -570,11 +489,8 @@ Do not edit the autogenerated section by hand. | 9 | [typednotes/lean-pq](https://github.com/typednotes/lean-pq) | Lean binding for libpq | Apache-2.0 | 2026-04-20 | – | | 8 | [alainchmt/RingOfIntegersProject](https://github.com/alainchmt/RingOfIntegersProject) | Certifying rings of integers in number fields with Lean | Apache-2.0 | 2026-03-20 | – | | 8 | [argumentcomputer/Ipld.lean](https://github.com/argumentcomputer/Ipld.lean) | a Lean4 implementation of the IPLD format | MIT | 2023-12-13 | ✗ | -| 8 | [argumentcomputer/Ipld.lean](https://github.com/argumentcomputer/Ipld.lean) | a Lean4 implementation of the IPLD format | MIT | 2023-11-03 | – | -| 8 | [argumentcomputer/Ipld.lean](https://github.com/argumentcomputer/Ipld.lean) | a Lean4 implementation of the IPLD format | MIT | 2023-11-03 | – | | 8 | [argumentcomputer/Poseidon.lean](https://github.com/argumentcomputer/Poseidon.lean) | A Lean 4 implementation of the Poseidon zkSNARK-friendly hash function | MIT | 2024-11-19 | ✗ | | 8 | [argumentcomputer/ZKSnark.lean](https://github.com/argumentcomputer/ZKSnark.lean) | https://yatima-inc.github.io/ZKSnark.lean/ | MIT | 2025-12-14 | ✗ | -| 8 | [argumentcomputer/ZKSnark.lean](https://github.com/argumentcomputer/ZKSnark.lean) | https://yatima-inc.github.io/ZKSnark.lean/ | MIT | 2025-12-14 | – | | 8 | [avigad/LeanSudoku](https://github.com/avigad/LeanSudoku) | Playing Sudoku in the Lean 4 proof assistant | Apache-2.0 | 2025-10-01 | ✗ | | 8 | [bollu/llama.lean](https://github.com/bollu/llama.lean) | Reimplementation of llama.cpp in Lean4 | | 2024-12-31 | – | | 8 | [CAIMEOX/json-schema](https://github.com/CAIMEOX/json-schema-lean) | Json Schema lean implementation | MIT | 2026-03-11 | ✗ | @@ -589,7 +505,6 @@ Do not edit the autogenerated section by hand. | 8 | [intgrah/qdt](https://github.com/intgrah/qdt) | Query-based Dependent Type Elaborator | Apache-2.0 | 2026-04-24 | ✗ | | 8 | [JamesGallicchio/Http](https://github.com/JamesGallicchio/http) | Basic HTTP definitions and parsing for Lean | Apache-2.0 | 2025-01-29 | ✗ | | 8 | [javra/iit](https://github.com/javra/iit) | Lean 4 IITs | | 2022-02-23 | – | -| 8 | [jeswr/RDF.lean](https://github.com/jeswr/RDF.lean) | An RDF Library for Lean4 | MIT | 2026-02-15 | – | | 8 | [jeswr/RustFFI](https://github.com/jeswr/RDF.lean) | An RDF Library for Lean4 | MIT | 2026-02-15 | ✗ | | 8 | [joelriou/topcat-model-category](https://github.com/joelriou/topcat-model-category) | | | 2026-04-18 | – | | 8 | [jonhanke/quadratic_forms_in_lean](https://github.com/jonhanke/quadratic_forms_in_lean) | | | 2025-09-07 | – | @@ -598,7 +513,6 @@ Do not edit the autogenerated section by hand. | 8 | [kbuzzard/IISc-experiments](https://github.com/kbuzzard/IISc-experiments) | Some material for Lean 4 lectures at IISc | | 2024-09-15 | – | | 8 | [kmill/LeanTeX_Mathlib](https://github.com/kmill/LeanTeX-mathlib) | LeanTeX pretty printers for mathlib | Apache-2.0 | 2026-03-23 | ✗ | | 8 | [leanprover/lean-eval](https://github.com/leanprover/lean-eval) | Comparator-based Lean formal mathematics eval | | 2026-05-07 | – | -| 8 | [leanprover/lean-eval](https://github.com/leanprover/lean-eval) | Comparator-based Lean formal mathematics eval | | 2026-05-07 | – | | 8 | [lecopivo/leanblas](https://github.com/lecopivo/LeanBLAS) | Bindings and specification for BLAS | Apache-2.0 | 2026-02-12 | ✗ | | 8 | [math-xmum/GameTheory](https://github.com/math-xmum/gametheory) | | Apache-2.0 | 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 | 2026-04-20 | – | @@ -609,7 +523,6 @@ Do not edit the autogenerated section by hand. | 8 | [Seasawher/mk-exercise](https://github.com/Seasawher/mk-exercise) | Simple and intuitive tool to manage exercises in textbooks written in Lean. | MIT | 2025-12-23 | ✗ | | 8 | [siddhartha-gadgil/Polylean](https://github.com/siddhartha-gadgil/Polylean) | | Apache-2.0 | 2025-06-02 | ✗ | | 8 | [sivukhin/sqlite3-lean-proofs](https://github.com/sivukhin/sqlite3-lean-proofs) | | | 2026-04-25 | – | -| 8 | [tani/literate-lean](https://github.com/tani/literate-lean) | literate programming for lean4 | Unlicense | 2026-03-12 | – | | 8 | [tani/LiterateLean](https://github.com/tani/literate-lean) | literate programming for lean4 | Unlicense | 2026-03-12 | ✓ | | 8 | [Timeroot/CircuitComp](https://github.com/Timeroot/CircuitComp) | Circuit complexity in Lean | | 2026-04-23 | – | | 8 | [vasnesterov/HadwigerNelson](https://github.com/vasnesterov/HadwigerNelson) | Hadwiger-Nelson Problem Formalization in Lean 4 | Apache-2.0 | 2024-12-09 | ✗ | @@ -629,7 +542,6 @@ Do not edit the autogenerated section by hand. | 7 | [fplaunchpad/sal](https://github.com/fplaunchpad/sal) | Multimodal verification of Replicated Data Types in Lean | MIT | 2026-04-29 | ✗ | | 7 | [GasStationManager/FormalizeWithTest](https://github.com/GasStationManager/FormalizeWithTest) | Autoformalization of coding problems, verified with test cases | GPL-3.0 | 2026-01-05 | ✗ | | 7 | [girafe-ai/formalising-mathematics](https://github.com/girafe-ai/lean-course) | Course on theorem proving with Lean | Apache-2.0 | 2025-12-24 | ✗ | -| 7 | [hanwenzhu/miller-rabin](https://github.com/hanwenzhu/miller-rabin) | Miller–Rabin primality test in Lean | Apache-2.0 | 2026-04-27 | – | | 7 | [hanwenzhu/MillerRabin](https://github.com/hanwenzhu/miller-rabin) | Miller–Rabin primality test in Lean | Apache-2.0 | 2026-04-27 | ✗ | | 7 | [haskell-spec/veriflex](https://github.com/haskell-spec/veriflex) | Verified lexer for Lean 4 | MIT | 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 | 2026-04-29 | ✗ | @@ -649,7 +561,6 @@ Do not edit the autogenerated section by hand. | 7 | [mseri/BET](https://github.com/mseri/BET) | Project for "Machine-Checked Mathematics" at the Lorentz Center | Apache-2.0 | 2026-04-28 | ✓ | | 7 | [nomeata/lean-mini-kernel](https://github.com/nomeata/lean-mini-kernel) | | | 2026-04-24 | – | | 7 | [objectionary/phi-calculus](https://github.com/objectionary/proof) | Proof of 𝜑-calculus confluence | MIT | 2026-04-29 | ✗ | -| 7 | [oOo0oOo/LeanSerde](https://github.com/oOo0oOo/LeanSerde) | Type-safe serialization for Lean | MIT | 2026-05-04 | – | | 7 | [Paul-Lez/Stacks-project](https://github.com/Paul-Lez/Stacks-project) | Formalizing Fibered Categories and Stacks in Lean | | 2025-12-30 | – | | 7 | [rahul3613/miniF2F-lean4](https://github.com/rahul3613/miniF2F-lean4) | miniF2F dataset ported into Lean 4 | MIT | 2025-12-16 | ✓ | | 7 | [riyazahuja/lean-m2](https://github.com/riyazahuja/lean-m2) | A proof-forming Lean-Macaulay2 interface | | 2025-12-23 | – | @@ -659,8 +570,6 @@ Do not edit the autogenerated section by hand. | 7 | [SchrodingerZhu/lean-gccjit](https://github.com/SchrodingerZhu/lean-gccjit) | libgccjit bindings for Lean4 | Apache-2.0 | 2023-10-26 | ✗ | | 7 | [siddhartha-gadgil/LeanLangur](https://github.com/siddhartha-gadgil/LeanLangur) | Expositions and demos for Lean Prover | MIT | 2026-04-24 | ✗ | | 7 | [SrGaabriel/lapis](https://github.com/SrGaabriel/lapis) | ✏️ \| A cutting-edge, concurrent & performant Language Server Protocol (LSP) framework for Lean 4. | Apache-2.0 | 2026-04-15 | ✓ | -| 7 | [sysghent/learn-lean-riddles](https://github.com/sysghent/learn-lean-riddles) | Riddles solved in Lean4 for educational purposes | Apache-2.0 | 2025-12-21 | – | -| 7 | [sysghent/learn-lean-riddles](https://github.com/sysghent/learn-lean-riddles) | Riddles solved in Lean4 for educational purposes | Apache-2.0 | 2025-12-21 | – | | 7 | [sysghent/riddle-proofs](https://github.com/sysghent/learn-lean-riddles) | Riddles solved in Lean4 for educational purposes | Apache-2.0 | 2025-12-21 | ✗ | | 7 | [T-Brick/controlflow](https://github.com/T-Brick/ControlFlow) | A control flow graph library for Lean | GPL-3.0 | 2025-11-17 | ✓ | | 7 | [taeyool/lean-flag-algebras](https://github.com/taeyool/lean-flag-algebras) | | | 2026-05-09 | – | @@ -675,11 +584,7 @@ Do not edit the autogenerated section by hand. | 6 | [Antoine-dSG/frieze_patterns](https://github.com/Antoine-dSG/frieze_patterns) | A project to formalise Coxeter's frieze patterns | | 2025-03-18 | – | | 6 | [anurudhp/aoc2022](https://github.com/anurudhp/aoc2022) | Advent of Code 2022 solutions: Lean4 | MIT | 2024-12-26 | ✗ | | 6 | [argumentcomputer/Blake3](https://github.com/argumentcomputer/Blake3.lean) | Lean4 bindings to Blake3 | MIT | 2026-04-16 | ✓ | -| 6 | [argumentcomputer/Blake3.lean](https://github.com/argumentcomputer/Blake3.lean) | Lean4 bindings to Blake3 | MIT | 2026-04-16 | – | -| 6 | [argumentcomputer/Blake3.lean](https://github.com/argumentcomputer/Blake3.lean) | Lean4 bindings to Blake3 | MIT | 2026-04-16 | – | | 6 | [argumentcomputer/Straume](https://github.com/argumentcomputer/straume) | State-of-the-art streams for Lean 4 | MIT | 2025-06-19 | ✗ | -| 6 | [argumentcomputer/straume](https://github.com/argumentcomputer/straume) | State-of-the-art streams for Lean 4 | MIT | 2025-06-19 | – | -| 6 | [argumentcomputer/straume](https://github.com/argumentcomputer/straume) | State-of-the-art streams for Lean 4 | MIT | 2025-06-19 | – | | 6 | [bergmannjg/time](https://github.com/bergmannjg/time) | Port of the haskell time library to Lean 4 and verification of date calculations | MIT | 2025-06-10 | ✗ | | 6 | [Bergschaf/LeanBanachTarski](https://github.com/Bergschaf/lean-banach-tarski) | | MIT | 2025-12-11 | ✓ | | 6 | [chrisflav/bruhat-tits](https://github.com/chrisflav/bruhat-tits) | A formalisation of the Bruhat-Tits tree in Lean4 | Apache-2.0 | 2026-02-17 | ✗ | @@ -726,7 +631,6 @@ Do not edit the autogenerated section by hand. | 5 | [AlexeyMilovanov/kolmogorov-complexity-lean](https://github.com/AlexeyMilovanov/kolmogorov-complexity-lean) | Formalization of Algorithmic Information Theory in Lean 4 | | 2026-04-07 | – | | 5 | [alexoltean61/hybrid_logic_lean](https://github.com/alexoltean61/hybrid_logic_lean) | | | 2025-09-18 | – | | 5 | [algebraic-dev/Colorized](https://github.com/algebraic-dev/colorized) | 🌈 \| A Lean 4 library designed to enhance terminal output with vibrant ANSI escape sequences. | Apache-2.0 | 2026-02-05 | ✓ | -| 5 | [algebraic-dev/colorized](https://github.com/algebraic-dev/colorized) | 🌈 \| A Lean 4 library designed to enhance terminal output with vibrant ANSI escape sequences. | Apache-2.0 | 2026-02-05 | – | | 5 | [alja123/hyperstabilityES](https://github.com/alja123/hyperstabilityES) | | | 2024-12-17 | – | | 5 | [AntoineChambert-Loir/DividedPowers4](https://github.com/AntoineChambert-Loir/DividedPowers4) | DividedPowers in Lean / Mathlib 4 | | 2026-04-10 | – | | 5 | [arademaker/vizagrams](https://github.com/arademaker/vizagrams) | A visualization library for Lean | Apache-2.0 | 2026-04-08 | ✓ | @@ -760,14 +664,12 @@ Do not edit the autogenerated section by hand. | 5 | [Lean-zh/protobuf](https://github.com/Lean-zh/protobuf) | protobuf implementation for Lean 4 | MIT | 2026-03-10 | – | | 5 | [lecopivo/SciLeanDemo](https://github.com/lecopivo/SciLeanDemo) | Demo project for SciLean | | 2025-01-06 | – | | 5 | [lf-lang/reactor-model](https://github.com/lf-lang/reactor-model) | A Lean-based formalization of the Reactor model. | Apache-2.0 | 2025-10-08 | ✗ | -| 5 | [lf-lang/reactor-model](https://github.com/lf-lang/reactor-model) | A Lean-based formalization of the Reactor model. | Apache-2.0 | 2025-10-08 | – | | 5 | [marcusrossel/model-checking](https://github.com/marcusrossel/model-checking) | Lean-formalizations of material from "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen | | 2025-01-12 | – | | 5 | [markusdemedeiros/Eileen](https://github.com/markusdemedeiros/Eileen) | Reimplementing some data structures from Iris in Lean | | 2025-09-09 | – | | 5 | [matematiflo/leanproject](https://github.com/matematiflo/CompAssistedMath2024) | GitHub repository for the seminar on Computer-assisted mathematics held at the University of Heidelberg during the Summ… | Apache-2.0 | 2025-07-10 | ✗ | | 5 | [mdr/aoc-2024](https://github.com/mdr/aoc-2024) | Solutions for Advent of Code 2024 in Lean 4 | | 2025-12-23 | – | | 5 | [mfornet/project-euler-lean](https://github.com/mfornet/project-euler-lean) | Proofs of Project Euler problems in LEAN | | 2025-12-31 | – | | 5 | [MichaelStollBayreuth/Heights](https://github.com/MichaelStollBayreuth/Heights) | An attempt at formalizing the theory of heights in Lean | GPL-2.0 | 2026-04-28 | ✓ | -| 5 | [monsterkrampe/Existential-Rules-in-Lean](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 | 2026-05-05 | – | | 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 | 2026-04-23 | ✗ | | 5 | [nileshtrivedi/lean-detective](https://github.com/nileshtrivedi/lean-detective) | A Lean4 library to formalize and proof-check murder mysteries like Murdle, KnivesOut and Drishyam | MIT | 2026-05-09 | – | | 5 | [ocfnash/lie-classification](https://github.com/ocfnash/LieClassification) | Classification of Lie algebras in Lean | Apache-2.0 | 2026-04-03 | ✗ | @@ -802,9 +704,7 @@ Do not edit the autogenerated section by hand. | 4 | [alok/AsciiPlot](https://github.com/alok/AsciiPlot) | ASCII/Unicode plotting library for Lean 4 with legends and braille rendering | Apache-2.0 | 2025-07-09 | ✗ | | 4 | [anlucia/chromatic_polynomial](https://github.com/anlucia/ChromaticPolynomial) | Chromatic polynomial in Lean4 | Apache-2.0 | 2025-03-24 | ✓ | | 4 | [argumentcomputer/OpenSSL.lean](https://github.com/argumentcomputer/OpenSSL.lean) | OpenSSL bindings for Lean | MIT | 2023-05-19 | ✗ | -| 4 | [argumentcomputer/OpenSSL.lean](https://github.com/argumentcomputer/OpenSSL.lean) | OpenSSL bindings for Lean | MIT | 2023-05-19 | – | | 4 | [argumentcomputer/Vero](https://github.com/argumentcomputer/Vero) | | MIT | 2023-03-23 | ✗ | -| 4 | [argumentcomputer/Vero](https://github.com/argumentcomputer/Vero) | | MIT | 2023-03-23 | – | | 4 | [arienmalec/axler](https://github.com/arienmalec/axler) | | | 2024-05-28 | – | | 4 | [AtticusKuhn/Transition-System-Ranking-Function](https://github.com/AtticusKuhn/Transition-System-Ranking-Function) | | | 2026-01-12 | – | | 4 | [avigad/lafny-experiments](https://github.com/avigad/lafny-experiments) | A repository for experimenting on methods of code verification in Lean | | 2025-10-07 | – | @@ -813,7 +713,6 @@ Do not edit the autogenerated section by hand. | 4 | [bustercopley/lean-float](https://github.com/bustercopley/lean-float) | Lemmas on floating-point arithmetic, in Lean 4 | | 2025-08-05 | – | | 4 | [CBirkbeck/ModularForms_Lean4](https://github.com/CBirkbeck/ModularForms_Lean4) | | | 2024-11-08 | – | | 4 | [ccodel/verus-lean](https://github.com/ccodel/verus-lean) | | | 2026-04-19 | – | -| 4 | [ccodel/verus-lean](https://github.com/ccodel/verus-lean) | | | 2026-04-19 | – | | 4 | [Command-Master/pseudorandom](https://github.com/Command-Master/lean-bourgain) | | Apache-2.0 | 2024-11-05 | ✗ | | 4 | [Dominique-Lawson/lean_4](https://github.com/Dominique-Lawson/Directed-Topology-Lean-4) | | MIT | 2026-03-26 | ✓ | | 4 | [doxtor6/MerLean_FormalQualBench](https://github.com/doxtor6/MerLean_FormalQualBench) | | | 2026-05-08 | – | @@ -839,7 +738,6 @@ Do not edit the autogenerated section by hand. | 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). | | 2026-03-26 | – | | 4 | [juanjomadrigal/denotational-lean](https://github.com/juanjomadrigal/denotational-lean) | | | 2025-12-03 | – | | 4 | [kim-em/lean-finmap](https://github.com/kim-em/lean-finmap) | | Apache-2.0 | 2025-10-01 | ✗ | -| 4 | [kim-em/lean-finmap](https://github.com/kim-em/lean-finmap) | | Apache-2.0 | 2025-10-01 | – | | 4 | [kiranandcode/lean-fuzz](https://github.com/kiranandcode/lean-fuzz) | Grammar Based Fuzzing For Lean 4 Prover | | 2026-05-01 | – | | 4 | [leanprover-community/hopscotch](https://github.com/leanprover-community/hopscotch) | hopscotch is an interactive validation tool to assist in keeping your Lean dependencies up to date | Apache-2.0 | 2026-04-27 | – | | 4 | [lecopivo/SciLeanExamples](https://github.com/lecopivo/SciLeanExamples) | SciLean examples mainly running through widgets | Apache-2.0 | 2024-04-15 | – | @@ -947,7 +845,6 @@ Do not edit the autogenerated section by hand. | 3 | [JOSHCLUNE/DuperDemo](https://github.com/JOSHCLUNE/DuperDemo) | | | 2025-04-13 | – | | 3 | [juhp/curljson](https://github.com/juhp/curl-json-lean) | curljson: a small Lean4 library to fetch JSON with libCurl | Apache-2.0 | 2026-03-29 | ✓ | | 3 | [Jun2M/Main-theorem-of-polytopes](https://github.com/Jun2M/Main-theorem-of-polytopes) | Proving the main theorem of polytopes using Lean 4 | | 2024-05-22 | – | -| 3 | [Jun2M/Main-theorem-of-polytopes](https://github.com/Jun2M/Main-theorem-of-polytopes) | Proving the main theorem of polytopes using Lean 4 | | 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 | [kbuzzard/MweSkeletons](https://github.com/kbuzzard/MweSkeletons) | Mathlib4 hierarchy skeletons for making mathlib-free MWEs in Lean 4 | | 2024-05-12 | – | | 3 | [kim-em/AoC2025](https://github.com/kim-em/AoC2025) | Advent of Code 2025 solutions in Lean 4 with proofs | | 2026-03-18 | – | @@ -956,16 +853,11 @@ Do not edit the autogenerated section by hand. | 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 | 2024-11-12 | ✓ | | 3 | [lambda-fairy/taleve](https://github.com/lambda-fairy/taleve) | Formal model of stacker games in Lean | Apache-2.0 | 2026-03-07 | ✗ | | 3 | [lean-phys-community/Notes](https://github.com/lean-phys-community/PhysLean_notes) | Notes in PhysLean | Apache-2.0 | 2025-05-07 | ✗ | -| 3 | [lean-phys-community/PhysLean_notes](https://github.com/lean-phys-community/PhysLean_notes) | Notes in PhysLean | Apache-2.0 | 2025-05-07 | – | | 3 | [leanprover/versowebcomponents](https://github.com/leanprover/verso-web-components) | A collection of reusable components from the Lean website designed build related sites with the same look and feel. | Apache-2.0 | 2026-04-18 | ✓ | | 3 | [LeastAuthority/STIR](https://github.com/LeastAuthority/STIR) | SC: Ethereum - zk(E)VM Verification - STIR Lean Blueprint | Apache-2.0 | 2025-05-05 | ✗ | | 3 | [LennyTaelman/TautoSet](https://github.com/LennyTaelman/TautoSet) | Lean 4 tactic to automatically prove set-theoretical tautologies. | | 2025-01-22 | – | -| 3 | [LennyTaelman/TautoSet](https://github.com/LennyTaelman/TautoSet) | Lean 4 tactic to automatically prove set-theoretical tautologies. | | 2025-01-22 | – | | 3 | [LodeVermeulen/Lean4_Bogdanovs_lemma](https://github.com/LodeVermeulen/Lean4_Bogdanovs_lemma) | | | 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 | 2025-06-20 | ✗ | -| 3 | [lua-vr/pointwise-birkhoff](https://github.com/lua-vr/pointwise-birkhoff) | A proof of Pointwise Birkhoff Ergodic Theorem in Lean | Apache-2.0 | 2025-06-19 | – | -| 3 | [lua-vr/pointwise-birkhoff](https://github.com/lua-vr/pointwise-birkhoff) | A proof of Pointwise Birkhoff Ergodic Theorem in Lean | Apache-2.0 | 2025-06-19 | – | -| 3 | [lua-vr/pointwise-birkhoff](https://github.com/lua-vr/pointwise-birkhoff) | A proof of Pointwise Birkhoff Ergodic Theorem in Lean | Apache-2.0 | 2025-06-19 | – | | 3 | [LucDuponcheelAtGitHub/PSBP](https://github.com/LucDuponcheelAtGitHub/PSBP) | PSBP implemented using Lean | | 2025-12-19 | – | | 3 | [lunsong/JaxProof](https://github.com/lunsong/JaxProof) | | | 2026-05-08 | – | | 3 | [manuelpuebla/amo-lean](https://github.com/manuelpuebla/amo-lean) | | MIT | 2026-04-23 | – | @@ -989,7 +881,6 @@ Do not edit the autogenerated section by hand. | 3 | [PatrickMassot/MDD154](https://github.com/PatrickMassot/MDD154) | | | 2026-04-01 | – | | 3 | [PatrickMassot/proofs_with_lean](https://github.com/PatrickMassot/proofs_with_lean) | An introduction to proofs with Lean using controled natural language | | 2026-03-31 | – | | 3 | [peabrainiac/CatDG](https://github.com/peabrainiac/lean-catdg) | Aspects of categorical differential geometry, formalised in lean 4. | Apache-2.0 | 2026-04-14 | ✗ | -| 3 | [peabrainiac/lean-catdg](https://github.com/peabrainiac/lean-catdg) | Aspects of categorical differential geometry, formalised in lean 4. | Apache-2.0 | 2026-04-14 | – | | 3 | [PratherConid/LeanLambda](https://github.com/PratherConid/LeanLambda) | | | 2026-02-23 | – | | 3 | [provables/special-numbers](https://github.com/provables/special-numbers) | Special Numbers (Chapter 6 from Knuth's Concrete Mathematics) | MIT | 2025-06-10 | ✗ | | 3 | [riccardobrasca/math2001](https://github.com/riccardobrasca/demontrer2025) | | Apache-2.0 | 2025-06-16 | ✗ | @@ -1026,7 +917,6 @@ Do not edit the autogenerated section by hand. | 2 | [adamtopaz/lean_embedding](https://github.com/adamtopaz/lean_embedding) | A small interface between lean4 and openai's embedding API | | 2023-06-14 | – | | 2 | [ADedecker/ProperAction](https://github.com/ADedecker/ProperAction) | | | 2024-05-14 | – | | 2 | [AdrienChampion/loadTerms](https://github.com/AdrienChampion/loadTerms.lean) | Testing dynamic term loading in Lean 4. | Apache-2.0 | 2023-12-12 | ✗ | -| 2 | [AdrienChampion/loadTerms.lean](https://github.com/AdrienChampion/loadTerms.lean) | Testing dynamic term loading in Lean 4. | Apache-2.0 | 2023-12-12 | – | | 2 | [AdrienChampion/safeIdx](https://github.com/AdrienChampion/safeIdx) | Type-safe indexing library. | Apache-2.0 | 2025-11-30 | ✗ | | 2 | [AlexBrodbelt/DicksonsClassificationTheorem](https://github.com/AlexBrodbelt/DicksonsClassificationTheorem) | | | 2026-01-08 | – | | 2 | [AlexBrodbelt/Game](https://github.com/AlexBrodbelt/metric-spaces-and-topology-game) | | MIT | 2024-10-01 | ✗ | @@ -1089,13 +979,11 @@ Do not edit the autogenerated section by hand. | 2 | [jstoobysmith/Anomaly_Cancellation_in_Lean](https://github.com/jstoobysmith/Anomaly_Cancellation_in_Lean) | | | 2025-03-24 | – | | 2 | [jtristan/lffi](https://github.com/jtristan/lffi) | | Apache-2.0 | 2024-07-16 | ✗ | | 2 | [Julian/Generatingfunctionology](https://github.com/Julian/generatingfunctionology.lean) | | MIT | 2025-10-24 | ✗ | -| 2 | [Julian/generatingfunctionology.lean](https://github.com/Julian/generatingfunctionology.lean) | | MIT | 2025-10-24 | – | | 2 | [jzxia/WhiteheadTheorem](https://github.com/jzxia/WhiteheadTheorem) | Proving the Whitehead theorem for Mathlib's homotopy groups. | | 2026-03-12 | – | | 2 | [kaiarasanen/lean4-collatz-proof-template](https://github.com/kaiarasanen/lean4-collatz-proof-template) | | | 2025-07-17 | – | | 2 | [kckennylau/EllipticCurve](https://github.com/kckennylau/EllipticCurve) | Towards a general definition of elliptic curve over schemes | Apache-2.0 | 2025-11-04 | ✗ | | 2 | [kevinsullivan/cs2120f24](https://github.com/kevinsullivan/cs2120f24) | CS 2120 (Sullivan) F24 | | 2025-11-20 | – | | 2 | [kim-em/lean-monadic-list](https://github.com/kim-em/lean-monadic-list) | Further development of the Lean `MLList` monadic lazy list type. | | 2025-09-02 | – | -| 2 | [kim-em/lean-monadic-list](https://github.com/kim-em/lean-monadic-list) | Further development of the Lean `MLList` monadic lazy list type. | | 2025-09-02 | – | | 2 | [kim-em/mathlib-minimizer](https://github.com/kim-em/mathlib-minimizer) | | | 2026-01-28 | – | | 2 | [kiranandcode/BetterFind.lean](https://github.com/kiranandcode/BetterFind.lean) | A better #find for lean. | | 2025-08-14 | – | | 2 | [kiranandcode/leanslop](https://github.com/kiranandcode/leanslop) | LeanSlop: LLM-slop black box automation for the Lean4 theorem prover | MIT | 2026-01-16 | – | @@ -1122,7 +1010,6 @@ Do not edit the autogenerated section by hand. | 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 | 2026-03-29 | ✗ | | 2 | [misaka10987/archimedes](https://github.com/misaka10987/archimedes) | Don't disturb my circle! | MIT | 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 | 2026-04-29 | ✗ | -| 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 | 2026-05-09 | – | | 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 | 2026-04-14 | ✗ | | 2 | [mrdouglasny/jacobian-challenge](https://github.com/mrdouglasny/jacobian-challenge) | Lean 4 attempt at Kevin Buzzard's Jacobian Challenge (Apr 2026) | | 2026-04-29 | – | | 2 | [nasqret/fineqs](https://github.com/nasqret/fineqs) | Lean4 formalization with Artistotle of the arXiv paper 1906.11174 | Apache-2.0 | 2026-01-26 | ✗ | @@ -1192,7 +1079,6 @@ Do not edit the autogenerated section by hand. | 1 | [benjaminfjones/reckonlean](https://github.com/benjaminfjones/reckonlean) | Notes on the Handbook of Practical Logic -- Lean Edition | | 2026-03-22 | – | | 1 | [bjoernkjoshanssen/deontic](https://github.com/bjoernkjoshanssen/deontic) | Classification and deontic explosion for contrary-to-duty obligations | | 2026-02-28 | – | | 1 | [bjoernkjoshanssen/jaccard](https://github.com/bjoernkjoshanssen/jaccard) | Lean 4 version of my Jaccard repository | | 2026-02-13 | – | -| 1 | [bjoernkjoshanssen/jaccard](https://github.com/bjoernkjoshanssen/jaccard) | Lean 4 version of my Jaccard repository | | 2026-02-13 | – | | 1 | [bjoernkjoshanssen/wollic25](https://github.com/bjoernkjoshanssen/wollic25) | A Lean 4 proof that there exists a subdirectly irreducible lattice (N₅) that is not simple. | | 2026-02-13 | – | | 1 | [bneb/perqed](https://github.com/bneb/perqed) | | | 2026-04-07 | – | | 1 | [bollu/polyscope.lean](https://github.com/bollu/polyscope.lean) | A polyscope (https://polyscope.run/) like interface for Lean, built on Proofwidgets4 | Apache-2.0 | 2024-06-17 | – | @@ -1260,7 +1146,6 @@ Do not edit the autogenerated section by hand. | 1 | [kaito2/lean-pq](https://github.com/kaito2/lean-pq) | | MIT | 2026-04-13 | – | | 1 | [kim-em/autograder_false](https://github.com/kim-em/autograder_false) | | | 2025-05-25 | – | | 1 | [kim-em/lean-crypto-hash](https://github.com/kim-em/lean-crypto-hash) | | Apache-2.0 | 2025-09-17 | – | -| 1 | [kim-em/lean-crypto-hash](https://github.com/kim-em/lean-crypto-hash) | | Apache-2.0 | 2025-09-17 | – | | 1 | [kim-em/scratch-comparator-unknown-constant](https://github.com/kim-em/scratch-comparator-unknown-constant) | | | 2026-01-04 | – | | 1 | [kmill/kmill-aoc2023](https://github.com/kmill/kmill-aoc2023) | Advent of Code 2023 | Apache-2.0 | 2023-12-13 | – | | 1 | [koly777/GeometricGroupTheoryLean](https://github.com/koly777/GeometricGroupTheoryLean) | Formalization of geometric group theory in Lean 4, with coarse geometry as the foundational framework. | | 2026-02-22 | – | diff --git a/aggregator/candidates/manual.txt b/aggregator/candidates/manual.txt index a0420d7b1f..b282d10eac 100644 --- a/aggregator/candidates/manual.txt +++ b/aggregator/candidates/manual.txt @@ -43,7 +43,6 @@ https://github.com/adomasbaliuka/AdventOfCode2023 https://github.com/adomasbaliuka/lean4-hacking https://github.com/adri326/rubin-lean4 https://github.com/adrianmartir/categorical-logic -https://github.com/AdrienChampion/loadTerms.lean https://github.com/aetilley/banach-tarski https://github.com/aim-cyber-workshop-2023/lean-sage https://github.com/AishwaryaS-561/Lean-setup @@ -76,7 +75,6 @@ https://github.com/AnandGokhale/LeanForControl https://github.com/anandijain/DocTest3.lean https://github.com/anandijain/is_rectangular_cuboid.lean https://github.com/Anderssorby/LeanPlay -https://github.com/Anderssorby/SDL.lean https://github.com/AnirudhG07/LeanBWT-Bzip2 https://github.com/anishrajeev/ModelTheoryFun https://github.com/AntanasKal/Advent-of-Code-2023 @@ -88,7 +86,6 @@ https://github.com/AnvitAggarwal/barrington-theorem-lean https://github.com/anzenlang/arrow.lean https://github.com/anzenlang/zen https://github.com/aochagavia/tic-tac-toe-lean -https://github.com/argumentcomputer/Blake3.lean https://github.com/arienmalec/axler https://github.com/arienmalec/mwe https://github.com/arnavdandu/dfs-lean @@ -113,7 +110,6 @@ https://github.com/avoair/Hausdorff https://github.com/Avshrek/KakeyaAutoform https://github.com/axiomed/Colorized.lean https://github.com/axiomed/http -https://github.com/axiomed/Http.lean https://github.com/axiomed/specs https://github.com/AxiomMath/putnam2025 https://github.com/AydenLamp/FinDFA @@ -242,9 +238,7 @@ https://github.com/dupuisf/aoc2023 https://github.com/dupuisf/aoc24 https://github.com/dupuisf/Lean4_AoC2022 https://github.com/dupuisf/LFTCM2024TraceClass -https://github.com/dwrensha/Chess.lean https://github.com/dwrensha/math-puzzles-in-lean4 -https://github.com/dwrensha/Rupert.lean https://github.com/EdAyers/ProofWidgets4 https://github.com/EdAyers/WidgetKit https://github.com/edegeltje/CwFTT @@ -346,7 +340,6 @@ https://github.com/hargoniX/nest-slimcheck https://github.com/hargoniX/nest-unit https://github.com/hargoniX/pfmt https://github.com/hargoniX/SlimCheck -https://github.com/hargoniX/socket.lean https://github.com/harmonic-ai/IMO2025 https://github.com/hediet/lean-cellular-automata https://github.com/HEPLean/HepLean @@ -406,7 +399,6 @@ https://github.com/jeffrey-dot-li/lean-homology https://github.com/jeremysalwen/advent_of_lean_2022 https://github.com/jeremysalwen/Lean4-Translate-Tactic https://github.com/jeswr/lean_sys_test -https://github.com/jeswr/RDF.lean https://github.com/jjaassoonn/GAGA https://github.com/jjdishere/EG https://github.com/jjdishere/neukirch @@ -439,7 +431,6 @@ https://github.com/jt496/Turan_4 https://github.com/jthulhu/2ltt https://github.com/juanjomadrigal/denotational-lean https://github.com/juanjomadrigal/lean-crafter -https://github.com/Julian/generatingfunctionology.lean https://github.com/Jun2M/Kura https://github.com/Jun2M/Main-theorem-of-polytopes https://github.com/Jun2M/MasterDiss @@ -480,7 +471,6 @@ https://github.com/KisaraBlue/ec-tate-lean https://github.com/KislyjKisel/lean4-gameOfLife https://github.com/KislyjKisel/mwe-require-externlib https://github.com/KislyjKisel/mwe-require-externlib2 -https://github.com/KislyjKisel/Raylib.lean https://github.com/klockeph/AdventOfCode2023 https://github.com/kmill/arrow_poly https://github.com/kmill/kmill-aoc2023 diff --git a/python/lean_pool/aggregator/render.py b/python/lean_pool/aggregator/render.py index 194614e273..a073c03f0e 100644 --- a/python/lean_pool/aggregator/render.py +++ b/python/lean_pool/aggregator/render.py @@ -38,6 +38,53 @@ _DESCRIPTION_LIMIT = 120 +_GITHUB_URL_RE = re.compile( + r"github\.com/(?P[^/\s]+)/(?P[^/\s#?]+?)(?:\.git)?/?(?:[\s?#]|$)", + re.IGNORECASE, +) + +# Suffixes commonly tacked onto Lean repo names that shouldn't affect +# whether two URLs refer to the same repo (Lake project naming convention, +# git clone URL convention). +_REPO_NAME_SUFFIXES = (".lean", ".git") + + +def canonical_key(owner: str, name: str) -> str: + """Reduce ``owner/name`` to a case- and suffix-insensitive key. + + Two URLs that point at the same GitHub repo should produce the same + key even when one uses ``Repo.lean`` and the other uses ``Repo``, + or when casing differs. + """ + lowered = name.lower() + for suffix in _REPO_NAME_SUFFIXES: + if lowered.endswith(suffix): + lowered = lowered[: -len(suffix)] + break + return f"{owner.lower()}/{lowered}" + + +def package_key(package: Package) -> str | None: + """Return the canonical GitHub key for a package, if derivable. + + Tries each ``sources[*].repoUrl``/``gitUrl`` first because Reservoir + sets ``fullName`` to the lakefile package name, which can differ + from the GitHub repo path (e.g. ``argumentcomputer/Straume`` for + the repo at ``argumentcomputer/straume``). Falls back to splitting + ``fullName`` only if no source URL is present. + """ + for source in package.get("sources") or []: + for url_field in ("repoUrl", "gitUrl"): + url = source.get(url_field) or "" + match = _GITHUB_URL_RE.search(url + " ") + if match: + return canonical_key(match["owner"], match["name"]) + full_name = package.get("fullName") or "" + if "/" in full_name: + owner, _, name = full_name.partition("/") + return canonical_key(owner, name) + return None + def _escape_cell(value: str) -> str: """Make a string safe to embed in a markdown table cell. @@ -103,19 +150,33 @@ def _row(package: Package) -> str: def render_table(manifest: ReservoirManifest) -> str: """Render the manifest as a markdown table. - Packages are sorted by star count descending, with ties broken by - ``fullName`` to keep diffs stable. The returned string includes a - trailing newline. + Packages are deduplicated by :func:`package_key` first (the first + occurrence wins, so callers should put authoritative entries — + typically Reservoir packages — before the fallback list), then + sorted by star count descending with ``fullName`` tiebreak. Args: - manifest: The full Reservoir manifest. + manifest: The full Reservoir manifest with packages in priority + order. Returns: A markdown table including header, separator, and one row per - package. + unique package. """ + seen: set[str] = set() + deduped: list[Package] = [] + for package in manifest["packages"]: + key = package_key(package) + if key is None: + deduped.append(package) + continue + if key in seen: + continue + seen.add(key) + deduped.append(package) + packages = sorted( - manifest["packages"], + deduped, key=lambda p: (-p.get("stars", 0), p["fullName"].lower()), ) rows = "\n".join(_row(p) for p in packages) diff --git a/python/tests/aggregator/test_render.py b/python/tests/aggregator/test_render.py index 546c53c5e6..7bc4fe6674 100644 --- a/python/tests/aggregator/test_render.py +++ b/python/tests/aggregator/test_render.py @@ -9,10 +9,14 @@ from lean_pool.aggregator.render import ( BEGIN_MARKER, END_MARKER, + canonical_key, + package_key, render_table, update_readme, ) +_UNSET = object() + def _package( *, @@ -20,12 +24,20 @@ def _package( stars: int = 0, description: str | None = "A demo package.", license_name: str | None = "MIT", - repo_url: str | None = "https://github.com/acme/demo", + repo_url: str | None = _UNSET, # type: ignore[assignment] versions: list[dict] | None = None, builds: list[dict] | None = None, ) -> dict: - """Build a minimal package fixture.""" + """Build a minimal package fixture. + + By default ``repo_url`` is derived from ``full_name`` so each + fixture corresponds to a distinct GitHub repo (and therefore a + distinct canonical key). Pass ``repo_url=None`` to omit sources, or + a string to override. + """ owner, name = full_name.split("/") + if repo_url is _UNSET: + repo_url = f"https://github.com/{full_name}" sources = [] if repo_url is not None: sources.append( @@ -170,6 +182,73 @@ def test_update_readme_is_idempotent(tmp_path: Path) -> None: assert after_first == after_second +def test_canonical_key_lowercases_and_strips_suffixes() -> None: + """Owner/name comparison must ignore case and Lake/git URL suffixes.""" + assert canonical_key("Acme", "Demo") == "acme/demo" + assert canonical_key("acme", "Demo.lean") == "acme/demo" + assert canonical_key("acme", "demo.git") == "acme/demo" + assert canonical_key("acme", "Demo.LEAN") == "acme/demo" + assert canonical_key("acme", "no-suffix") == "acme/no-suffix" + + +def test_package_key_prefers_source_url_over_full_name() -> None: + """The source URL beats fullName, which uses the lakefile name.""" + package = _package( + full_name="argumentcomputer/Straume", + repo_url="https://github.com/argumentcomputer/straume", + ) + assert package_key(package) == "argumentcomputer/straume" + + +def test_package_key_falls_back_to_full_name_when_no_sources() -> None: + """Manual entries with no sources still produce a usable key.""" + package = _package(full_name="acme/demo", repo_url=None) + assert package_key(package) == "acme/demo" + + +def test_render_table_dedupes_keeping_first_occurrence() -> None: + """Two packages pointing at the same GitHub repo collapse to one row.""" + reservoir_entry = _package( + full_name="argumentcomputer/Straume", + stars=99, + repo_url="https://github.com/argumentcomputer/straume", + ) + manual_entry = _package( + full_name="argumentcomputer/straume", + stars=6, + repo_url="https://github.com/argumentcomputer/straume", + ) + manifest = _manifest([reservoir_entry, manual_entry]) + + table = render_table(manifest) + + rows = [line for line in table.splitlines() if "argumentcomputer" in line] + assert len(rows) == 1, f"expected one row, got {rows}" + # The first occurrence (reservoir) should win, so stars=99 not stars=6. + assert "| 99 |" in rows[0] + + +def test_render_table_dedupes_lean_suffix_collisions() -> None: + """A repo named ``Foo.lean`` and one named ``Foo`` are the same repo.""" + reservoir_entry = _package( + full_name="argumentcomputer/Blake3", + stars=50, + repo_url="https://github.com/argumentcomputer/Blake3.lean", + ) + manual_entry = _package( + full_name="argumentcomputer/Blake3.lean", + stars=2, + repo_url="https://github.com/argumentcomputer/Blake3.lean", + ) + manifest = _manifest([reservoir_entry, manual_entry]) + + table = render_table(manifest) + + rows = [line for line in table.splitlines() if "Blake3" in line] + assert len(rows) == 1 + assert "| 50 |" in rows[0] + + def test_update_readme_raises_when_markers_missing(tmp_path: Path) -> None: """Refuse to clobber a README that does not have the markers.""" readme_path = tmp_path / "README.md"