From 97c5cf3433cbf8928c8868f6307b91b5a131bc26 Mon Sep 17 00:00:00 2001 From: justincasher Date: Sat, 9 May 2026 15:31:46 -0700 Subject: [PATCH] Filter low-star rows from rendered candidates table The candidates README hit GitHub's markdown rendering threshold once the toolchain column landed, and the page fell back to plain-text-with- autolinks. Add a render-time --min-stars filter (default 2, matching Reservoir's own inclusion floor) so the markdown stays small enough to render. The underlying raw_data/ files still keep every package, and --min-stars=0 brings them all back. --- aggregator/candidates/README.md | 465 +----------------------- python/lean_pool/aggregator/__main__.py | 27 +- python/lean_pool/aggregator/render.py | 19 +- python/tests/aggregator/test_render.py | 37 ++ 4 files changed, 82 insertions(+), 466 deletions(-) diff --git a/aggregator/candidates/README.md b/aggregator/candidates/README.md index a97926f579..2d55c78f35 100644 --- a/aggregator/candidates/README.md +++ b/aggregator/candidates/README.md @@ -13,9 +13,12 @@ Tracking which Lean packages we are considering for inclusion in `python -m lean_pool.aggregator fetch`: the Reservoir manifest plus GitHub metadata for each entry in `manual.txt`. - The summary table below is regenerated from those files by - `python -m lean_pool.aggregator render`. Inclusion decisions are not - yet tracked here; when we start making them we will add a separate - `decisions.jsonl` rather than per-package files. + `python -m lean_pool.aggregator render`. By default it shows only + packages with at least 2 stars (matching Reservoir's own floor) so + GitHub keeps rendering the markdown — `raw_data/` still holds every + package, and `--min-stars=0` renders the full list. Inclusion + decisions are not yet tracked here; when we start making them we + will add a separate `decisions.jsonl` rather than per-package files. Do not edit the autogenerated section by hand. @@ -1055,460 +1058,4 @@ Do not edit the autogenerated section by hand. | 2 | [YaelDillies/MeanFourier](https://github.com/YaelDillies/mean-fourier) | Formalisation of mean Fourier analysis in Lean 4 | Apache-2.0 | v4.30.0-rc2 | 2026-04-14 | ✗ | | 2 | [YijunYuan/HarderNarasimhan](https://github.com/YijunYuan/HarderNarasimhan) | Formalization of Harder-Narasimhan theory | Apache-2.0 | v4.29.1 | 2026-04-12 | ✗ | | 2 | [ykonstant1/esiv](https://github.com/ykonstant1/esiv) | Sieve of Eratosthenes in Lean for performance testing | GPL-3.0 | v4.7.0-rc2 | 2026-03-31 | – | -| 1 | [a-dangelo/Lean-AG](https://github.com/a-dangelo/Lean-AG) | Lean formalisation project in algebraic geometry. | Apache-2.0 | v4.24.0 | 2025-10-17 | – | -| 1 | [A-M-Berns/Formalized-Agent-Foundations](https://github.com/A-M-Berns/Formalized-Agent-Foundations) | | | v4.28.0-rc1 | 2026-05-03 | – | -| 1 | [adamtopaz/hw_template_test](https://github.com/adamtopaz/hw_template_test) | | | v4.0.0 | 2023-09-13 | – | -| 1 | [adamtopaz/lean4_advent_2021](https://github.com/adamtopaz/lean4_advent_2021) | | | nightly-2021-12-01 | 2023-02-27 | – | -| 1 | [adamtopaz/lean_pdist](https://github.com/adamtopaz/lean_pdist) | | | v4.11.0-rc3 | 2024-09-01 | – | -| 1 | [adamtopaz/lean_pinecone](https://github.com/adamtopaz/lean_pinecone) | A barebones interface between lean4 and pinecone databases | | nightly-2023-06-01 | 2023-06-07 | – | -| 1 | [adrianmartir/categorical-logic](https://github.com/adrianmartir/categorical-logic) | Categorical Logic in Lean | Apache-2.0 | v4.28.0 | 2026-03-13 | – | -| 1 | [akp2003/prob-book](https://github.com/akp2003/prob-book) | Formalization of the Grinstead and Snell's Introduction to Probability. | GPL-3.0 | v4.10.0 | 2025-06-05 | – | -| 1 | [alex-wellbelove/lean_sqlite](https://github.com/alex-wellbelove/lean_sqlite) | Lean 4 bindings to libSqlite. WIP. | | 4.0.0 | 2025-10-15 | – | -| 1 | [alexf91/LTest](https://github.com/alexf91/LTest) | A unit testing framework for Lean 4 | Apache-2.0 | nightly-2023-09-17 | 2023-04-01 | – | -| 1 | [alexjbest/ant-lorentz](https://github.com/alexjbest/ant-lorentz) | | | nightly-2023-07-12 | 2023-08-07 | – | -| 1 | [alexkeizer/lean-naming-lint](https://github.com/alexkeizer/lean-naming-lint) | A linter for Lean 4 that checks whether definitions conform with Mathlib4's naming convention | | nightly-2023-02-22 | 2023-04-22 | – | -| 1 | [AmosNico/validator](https://github.com/AmosNico/validator) | Formally Verified Validator for Unsolvability Certificates for Automated Planning in Lean 4 | Apache-2.0 | v4.27.0 | 2026-04-15 | – | -| 1 | [AnandGokhale/LeanForControl](https://github.com/AnandGokhale/LeanForControl) | The intent of this repository is to build a database of control theoretic proofs in lean. | MIT | v4.30.0-rc2 | 2026-05-09 | – | -| 1 | [anandijain/is_rectangular_cuboid.lean](https://github.com/anandijain/is_rectangular_cuboid.lean) | | | v4.13.0-rc3 | 2024-11-13 | – | -| 1 | [AnvitAggarwal/barrington-theorem-lean](https://github.com/AnvitAggarwal/barrington-theorem-lean) | | | v4.25.0-rc2 | 2025-12-19 | – | -| 1 | [arnavdandu/dfs-lean](https://github.com/arnavdandu/dfs-lean) | Formalization of depth-first search in Lean | | v4.29.0-rc6 | 2026-03-21 | – | -| 1 | [arthur-adjedj/logrel-lean](https://github.com/arthur-adjedj/logrel-lean) | | | master | 2024-10-17 | – | -| 1 | [avigad/EquationalTest](https://github.com/avigad/EquationalTest) | A test of Duper with an example from the Equational Theories project | | v4.20.0-rc2 | 2025-05-17 | – | -| 1 | [Avshrek/KakeyaAutoform](https://github.com/Avshrek/KakeyaAutoform) | | | v4.28.0 | 2026-03-19 | – | -| 1 | [b-mehta/ExponentialRamsey](https://github.com/b-mehta/ExponentialRamsey) | | | v4.29.0-rc6 | 2026-03-17 | – | -| 1 | [benjaminfjones/reckonlean](https://github.com/benjaminfjones/reckonlean) | Notes on the Handbook of Practical Logic -- Lean Edition | | v4.29.0-rc6 | 2026-03-22 | – | -| 1 | [bjoernkjoshanssen/deontic](https://github.com/bjoernkjoshanssen/deontic) | Classification and deontic explosion for contrary-to-duty obligations | | v4.27.0-rc1 | 2026-02-28 | – | -| 1 | [bjoernkjoshanssen/jaccard](https://github.com/bjoernkjoshanssen/jaccard) | Lean 4 version of my Jaccard repository | | v4.15.0-rc1 | 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. | | v4.22.0-rc3 | 2026-02-13 | – | -| 1 | [bneb/perqed](https://github.com/bneb/perqed) | | | v4.30.0-rc2 | 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 | nightly-2023-03-17 | 2024-06-17 | – | -| 1 | [bollu/quenya.lean](https://github.com/bollu/quenya.lean) | A Lean4 library to build and manipulate ELF files. | | nightly | 2025-10-12 | – | -| 1 | [BoltonBailey/levm](https://github.com/BoltonBailey/levm) | | | v4.7.0 | 2024-10-15 | – | -| 1 | [bridgerlogan9/riemann-hypothesis-lean](https://github.com/bridgerlogan9/riemann-hypothesis-lean) | Formal proof of the Riemann Hypothesis via the Zeta Resonator in Lean 4 | | 4.2.0 | 2026-04-10 | – | -| 1 | [cameronfreer/erdos124](https://github.com/cameronfreer/erdos124) | A complete Lean 4 formalization of Erdős Problem 124 using Mathlib. | MIT | v4.26.0 | 2025-12-17 | – | -| 1 | [CBirkbeck/FltRegulartest](https://github.com/CBirkbeck/FltRegulartest) | | Apache-2.0 | v4.10.0-rc2 | 2024-07-23 | – | -| 1 | [CBirkbeck/GLn_F_q](https://github.com/CBirkbeck/GLn_F_q) | | | v4.8.0-rc2 | 2024-07-10 | – | -| 1 | [CBirkbeck/power_residue_symbols](https://github.com/CBirkbeck/power_residue_symbols) | | | v4.7.0-rc2 | 2024-11-13 | – | -| 1 | [cduenasnavarro/PROOF101-miniproject-cduenasnavarro](https://github.com/cduenasnavarro/PROOF101-miniproject-cduenasnavarro) | | | v4.29.0-rc8 | 2026-04-17 | – | -| 1 | [chabulhwi/tpil-solutions](https://github.com/chabulhwi/tpil-solutions) | My solutions to the exercises in "Theorem Proving in Lean 4" | Apache-2.0 | v4.29.1 | 2026-04-24 | – | -| 1 | [chrisflav/polydim](https://github.com/chrisflav/polydim) | | | v4.15.0 | 2025-07-10 | – | -| 1 | [codyroux/compact-php](https://github.com/codyroux/compact-php) | A proof of a finitary pigeon hole principle via compactness and the infinitary version, in Lean. | | v4.6.0-rc1 | 2024-04-11 | – | -| 1 | [colbyaustinbrown/sigal](https://github.com/colbyaustinbrown/sigal) | Formalization of Sheaves in Geometry and Logic by Mac Lane and Moerdijk | | v4.24.0-rc1 | 2025-10-12 | – | -| 1 | [cruisesong7/formal_ramsey](https://github.com/cruisesong7/formal_ramsey) | | | v4.28.0 | 2026-04-05 | – | -| 1 | [cs-lean/cs-lean.github.io](https://github.com/cs-lean/cs-lean.github.io) | | Apache-2.0 | v4.26.0-rc2 | 2026-04-28 | – | -| 1 | [ctchou/my_lean](https://github.com/ctchou/my_lean) | My Lean playground | Apache-2.0 | v4.27.0-rc1 | 2026-01-05 | – | -| 1 | [david-christiansen/failing-example-envext](https://github.com/david-christiansen/failing-example-envext) | Failing to create a Lean environment extension | | stable | 2025-04-17 | – | -| 1 | [DavidJWebb/Formalization_of_Computability](https://github.com/DavidJWebb/Formalization_of_Computability) | An ongoing effort to formalize computability theory notions involving subsets of ℕ. | | v4.28.0 | 2026-02-24 | – | -| 1 | [davidmunozlahoz/veclat](https://github.com/davidmunozlahoz/veclat) | Lean project to formalize the theory of vector lattices. | MIT | v4.26.0-rc2 | 2026-02-16 | – | -| 1 | [DebarghaG/LEAN-Autoformalization-Uncertainty](https://github.com/DebarghaG/LEAN-Autoformalization-Uncertainty) | Grammars of Formal Uncertainty [NeurIPS 2025] - Adapted for LEAN. Unofficial Implementation. Potentially unstable. | | lean4 | 2026-01-22 | – | -| 1 | [dunhamsteve/aoc2023](https://github.com/dunhamsteve/aoc2023) | | | 4.4.0 | 2024-12-24 | – | -| 1 | [dupuisf/aoc2023](https://github.com/dupuisf/aoc2023) | Advent of Code 2023 in Lean 4 | | v4.5.0-rc1 | 2023-12-25 | – | -| 1 | [dupuisf/LFTCM2024TraceClass](https://github.com/dupuisf/LFTCM2024TraceClass) | Project for LFTCM2024: Trace class operators | | v4.7.0-rc2 | 2024-08-17 | – | -| 1 | [edrx/LuaTreeLean](https://github.com/edrx/LuaTreeLean) | A Lean library that calls luatree.lua. | | | 2024-06-26 | – | -| 1 | [edwin1729/bppl-logic](https://github.com/edwin1729/bppl-logic) | Program Logic for Bayesian Probabilistic Programs | Apache-2.0 | v4.28.0 | 2026-05-03 | – | -| 1 | [edwin1729/semantics](https://github.com/edwin1729/semantics) | | | v4.18.0-rc1 | 2025-11-10 | – | -| 1 | [eisbaw/Clift](https://github.com/eisbaw/Clift) | WIP! Parse and lift C code to LEAN 4, AutoCorres2-inspired | BSD-2-Clause | v4.30.0-rc1 | 2026-04-15 | – | -| 1 | [emap-20242-nlp/cs](https://github.com/emap-20242-nlp/cs) | examples in Lean | | v4.10.0 | 2024-09-27 | – | -| 1 | [ericluap/OrderedSemigroups](https://github.com/ericluap/OrderedSemigroups) | Formalization of Holder's Theorem for Ordered Semigroups and Groups | | v4.27.0-rc1 | 2025-12-27 | – | -| 1 | [faenuccio-teaching/M1_ENS_26](https://github.com/faenuccio-teaching/M1_ENS_26) | This is the repository for the Master course "Formalisation Mathématique" ENS-Paris in Spring 2026 | | v4.27.0-rc1 | 2026-04-15 | – | -| 1 | [fgdorais/lean4-ascii](https://github.com/fgdorais/lean4-ascii) | | Apache-2.0 | v4.28.0-rc1 | 2026-03-24 | – | -| 1 | [FrankieeW/QuadraticNumberFields](https://github.com/FrankieeW/QuadraticNumberFields) | A formalization of quadratic number fields in Lean 4 | Apache-2.0 | v4.29.0-rc2 | 2026-03-25 | – | -| 1 | [FrederickPu/pullback](https://github.com/FrederickPu/pullback) | Formally verified code to code translation using LLMs and Lean4 | MIT | v4.29.0-rc2 | 2026-05-08 | – | -| 1 | [funexists/jessicacantswim](https://github.com/funexists/jessicacantswim) | Jessica Can't Swim Game | Zlib | v4.20.1 | 2025-08-17 | – | -| 1 | [gabriel128/analysis_in_lean](https://github.com/gabriel128/analysis_in_lean) | Real Analysis in Lean4 | Apache-2.0 | nightly-2023-07-31 | 2025-06-02 | – | -| 1 | [GasStationManager/WakingUp](https://github.com/GasStationManager/WakingUp) | Experiments on detecting and recovering from hallucinations in AI coding models | GPL-3.0 | v4.15.0 | 2025-04-30 | – | -| 1 | [gebner/inundation](https://github.com/gebner/inundation) | Stress test for Lake. | | nightly-2022-12-04 | 2023-08-24 | – | -| 1 | [ggranberry/ToeplitzHausdorff](https://github.com/ggranberry/ToeplitzHausdorff) | | | v4.15.0 | 2025-03-14 | – | -| 1 | [ghseeli/lean-club](https://github.com/ghseeli/lean-club) | Lean files for ICERM Fall 2025 Lean club | | v4.26.0-rc1 | 2025-12-01 | – | -| 1 | [grunweg/QuotientManifolds](https://github.com/grunweg/QuotientManifolds) | | | v4.27.0-rc1 | 2026-05-06 | – | -| 1 | [hanwenzhu/lean-demo-20250502](https://github.com/hanwenzhu/lean-demo-20250502) | MWE of a Lean v4.9.0 feature/bug | | v4.9.0 | 2025-05-03 | – | -| 1 | [Happyves/Lean_Games](https://github.com/Happyves/Lean_Games) | Combinatorial and positional games formalised in Lean | Apache-2.0 | v4.5.0-rc1 | 2024-11-06 | – | -| 1 | [hargoniX/fil-rb](https://github.com/hargoniX/fil-rb) | A Red-Black-Tree Formalisation for LMU's Formalisation in Lean 2024 | GPL-2.0 | v4.15.0-rc1 | 2026-03-12 | – | -| 1 | [hargoniX/lean4-statvfs](https://github.com/hargoniX/lean4-statvfs) | A statvfs FFI API for Lean 4 | MIT | nightly-2021-10-16 | 2021-10-22 | – | -| 1 | [hargoniX/SlimCheck](https://github.com/hargoniX/SlimCheck) | A temporary home for slimcheck | | v4.13.0-rc3 | 2024-10-23 | – | -| 1 | [hediet/lean-cellular-automata](https://github.com/hediet/lean-cellular-automata) | | | v4.26.0-rc2 | 2026-05-01 | – | -| 1 | [homeowmorphism/FinitelyPresentedGroups](https://github.com/homeowmorphism/FinitelyPresentedGroups) | | | v4.26.0-rc2 | 2025-12-22 | – | -| 1 | [ianm1129/Polytime-Formalizations](https://github.com/ianm1129/Polytime-Formalizations) | Attempting to define some complexity primitives in Lean | | v4.22.0-rc2 | 2026-01-14 | – | -| 1 | [IlPreteRosso/LEANearized-RadiiPolynomial](https://github.com/IlPreteRosso/LEANearized-RadiiPolynomial) | | | v4.28.0-rc1 | 2026-03-29 | – | -| 1 | [ItsMeForLua/ln_messagepack](https://github.com/ItsMeForLua/ln_messagepack) | A MessagePack serialization library for Lean 4 | | v4.21.0-rc3 | 2025-08-15 | – | -| 1 | [James-Oswald/Functional-Programming-In-Lean](https://github.com/James-Oswald/Functional-Programming-In-Lean) | My solutions for selected exercises in Christiansen's Book "Functional Programming In Lean" | | | 2023-11-19 | – | -| 1 | [jamesdabbs/advent-2023](https://github.com/jamesdabbs/advent-2023) | Advent of Code in L∃∀N | | stable | 2023-12-05 | – | -| 1 | [JamesGallicchio/lean_rms](https://github.com/JamesGallicchio/lean_rms) | | | nightly-2023-05-16 | 2021-10-28 | – | -| 1 | [jano-wol/aristotle](https://github.com/jano-wol/aristotle) | Shell scripts to simplify working with the Aristotle API | MIT | v4.28.0 | 2026-03-19 | – | -| 1 | [JarodAlper/RegularLocalRings](https://github.com/JarodAlper/RegularLocalRings) | Formalization of regular local rings and regular sequences | GPL-3.0 | v4.23.0-rc2 | 2025-09-10 | – | -| 1 | [jeffrey-dot-li/lean-homology](https://github.com/jeffrey-dot-li/lean-homology) | | | v4.28.0-rc1 | 2026-04-11 | – | -| 1 | [joelriou/k-injective](https://github.com/joelriou/k-injective) | | | v4.6.0-rc1 | 2024-08-13 | – | -| 1 | [joelriou/lean-derived-categories](https://github.com/joelriou/lean-derived-categories) | Formalization of derived categories in Lean/mathlib | | v4.21.0-rc3 | 2025-06-25 | – | -| 1 | [jsm28/IMOShortlist2024Lean](https://github.com/jsm28/IMOShortlist2024Lean) | IMO Shortlist 2024 problem statements and some solutions in Lean | Apache-2.0 | v4.22.0-rc3 | 2025-07-22 | – | -| 1 | [jt496/AESBrandt](https://github.com/jt496/AESBrandt) | | | v4.20.0-rc5 | 2025-10-17 | – | -| 1 | [Jun2M/Kura](https://github.com/Jun2M/Kura) | | | v4.20.0-rc5 | 2025-09-11 | – | -| 1 | [Kairose-master/mu_eq_pi](https://github.com/Kairose-master/mu_eq_pi) | | MIT | v4.21.0-rc3 | 2025-08-25 | – | -| 1 | [kaito2/lean-pq](https://github.com/kaito2/lean-pq) | | MIT | v4.27.0 | 2026-04-13 | – | -| 1 | [kim-em/autograder_false](https://github.com/kim-em/autograder_false) | | | v4.15.0 | 2025-05-25 | – | -| 1 | [kim-em/lean-crypto-hash](https://github.com/kim-em/lean-crypto-hash) | | Apache-2.0 | nightly-2025-08-21 | 2025-09-17 | – | -| 1 | [kim-em/scratch-comparator-unknown-constant](https://github.com/kim-em/scratch-comparator-unknown-constant) | | | v4.25.0-rc2 | 2026-01-04 | – | -| 1 | [kmill/kmill-aoc2023](https://github.com/kmill/kmill-aoc2023) | Advent of Code 2023 | Apache-2.0 | v4.4.0-rc1 | 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. | | v4.26.0 | 2026-02-22 | – | -| 1 | [Komyyy/legacy-cc](https://github.com/Komyyy/legacy-cc) | This repository preserves the `cc` tactic that was once in Mathlib | Apache-2.0 | v4.28.0-rc1 | 2026-02-02 | – | -| 1 | [kyleellefsen/lean_aoc_2023](https://github.com/kyleellefsen/lean_aoc_2023) | | | v4.11.0-rc3 | 2024-11-23 | – | -| 1 | [LakshitSinghBishtTM/xLaDe](https://github.com/LakshitSinghBishtTM/xLaDe) | A Lean 4 Ecosystem Framework! | GPL-3.0 | stable | 2026-05-01 | – | -| 1 | [lean-summer-research/finalized](https://github.com/lean-summer-research/finalized) | Finalized Lean for Mathlib (with Blueprint) | | v4.25.0-rc2 | 2026-04-23 | – | -| 1 | [leanprover-community/lean3port](https://github.com/leanprover-community/lean3port) | Stub for downloading mathport artifacts for Lean 3 | | v4.10.0-rc2 | 2025-08-15 | – | -| 1 | [leanprover-community/test-mathport](https://github.com/leanprover-community/test-mathport) | | | nightly-2021-10-02 | 2023-07-02 | – | -| 1 | [lecopivo/lean-cpp-ffi](https://github.com/lecopivo/lean-cpp-ffi) | test of using c++ in lean ffi | | nightly-2023-08-17 | 2023-09-21 | – | -| 1 | [lorenzosaraiva/DLDSBooleanCircuit](https://github.com/lorenzosaraiva/DLDSBooleanCircuit) | | MIT | v4.29.0-rc7 | 2026-03-27 | – | -| 1 | [LumaKernel/lean4-cov-recursion](https://github.com/LumaKernel/lean4-cov-recursion) | Lean4 proof of course-of-values recursion on Nat | CC0-1.0 | v4.5.0-rc1 | 2024-01-05 | – | -| 1 | [maemre/automata-in-lean](https://github.com/maemre/automata-in-lean) | | | v4.13.0-rc3 | 2024-12-24 | – | -| 1 | [marcellop71/EM](https://github.com/marcellop71/EM) | | Apache-2.0 | v4.29.0 | 2026-05-09 | – | -| 1 | [marcusrossel/lean-ccs](https://github.com/marcusrossel/lean-ccs) | A definition of CCS and verified computable reduction to LTS in Lean. | | v4.5.0-rc1 | 2024-06-07 | – | -| 1 | [markkasaurus/gleason-busch-lean](https://github.com/markkasaurus/gleason-busch-lean) | Lean 4 formalization of Gleason's theorem via Busch's effects formulation | Apache-2.0 | v4.26.0 | 2026-04-29 | – | -| 1 | [markusdemedeiros/IrisLeanMath](https://github.com/markusdemedeiros/IrisLeanMath) | | | v4.25.0 | 2025-12-01 | – | -| 1 | [mbkybky/GaloisRamification](https://github.com/mbkybky/GaloisRamification) | Formalizing ramification theory in Galois extensions | | v4.14.0-rc3 | 2026-05-04 | – | -| 1 | [mdgeorge4153/cglean](https://github.com/mdgeorge4153/cglean) | Verified computational geometry in Lean | | v4.8.0-rc1 | 2025-03-22 | – | -| 1 | [mdnestor/LawvereFixedPoint](https://github.com/mdnestor/LawvereFixedPoint) | Proof of Lawvere's fixed point theorem in Lean 4 | | v4.11.0-rc3 | 2026-04-01 | – | -| 1 | [MetalCreator666/WhitneyGraustein](https://github.com/MetalCreator666/WhitneyGraustein) | | | v4.10.0 | 2024-12-16 | – | -| 1 | [michelsol/bounding-sphere-math](https://github.com/michelsol/bounding-sphere-math) | Bounding sphere mathematics in Lean. Contains a proof of Jung's theorem https://en.wikipedia.org/wiki/Jung%27s_theorem | Apache-2.0 | v4.27.0-rc1 | 2025-12-15 | – | -| 1 | [mistarro/local-rings](https://github.com/mistarro/local-rings) | Lean 4 formalization of my results on local rings and algebras | | v4.21.0 | 2025-07-20 | – | -| 1 | [mlyean/lean-coxeter](https://github.com/mlyean/lean-coxeter) | Coxeter groups in Lean 4 | | v4.30.0-rc2 | 2026-05-06 | – | -| 1 | [mpenciak/AdventOfCode](https://github.com/mpenciak/AdventOfCode) | Solving 2022 Advent of Code problems in Lean 4 | | nightly-2022-12-02 | 2022-12-14 | – | -| 1 | [mrdouglasny/hille-yosida](https://github.com/mrdouglasny/hille-yosida) | Lean 4 formalization of strongly continuous semigroups, Hille-Yosida theorem, and BCR Bochner semigroup-to-group extens… | Apache-2.0 | v4.29.0 | 2026-04-13 | – | -| 1 | [mukeshtiwari/raushan-paper-code](https://github.com/mukeshtiwari/raushan-paper-code) | | | v4.29.1 | 2026-05-05 | – | -| 1 | [nasa-jpl/L4YAML](https://github.com/nasa-jpl/L4YAML) | A YAML 1.2.2 parser in Lean 4 with the goal of **verified correctness** | | v4.30.0-rc2 | 2026-05-06 | – | -| 1 | [Nazgand/NazgandLean4](https://github.com/Nazgand/NazgandLean4) | My Lean4 math code | | v4.28.0-rc1 | 2026-02-04 | – | -| 1 | [NethermindEth/ExtTreeMapLemmas](https://github.com/NethermindEth/ExtTreeMapLemmas) | | | v4.22.0-rc2 | 2026-04-15 | – | -| 1 | [NicolasRouquette/YatimaGraphLib](https://github.com/NicolasRouquette/YatimaGraphLib) | Extracted Yatima's Lean4 Graph as a generic library | | nightly-2022-07-03 | 2022-08-10 | – | -| 1 | [nomeata/lean-constructions](https://github.com/nomeata/lean-constructions) | | | leanprover/lean4-pr-releases:pr-release-4474 | 2024-06-20 | – | -| 1 | [nomeata/rerolling-sixes](https://github.com/nomeata/rerolling-sixes) | | | nightly-2023-07-12 | 2023-05-16 | – | -| 1 | [or4nge19/SpinGlass](https://github.com/or4nge19/SpinGlass) | | Apache-2.0 | v4.28.0-rc1 | 2026-03-23 | – | -| 1 | [Philogy/lean-aoc-2024](https://github.com/Philogy/lean-aoc-2024) | | | v4.15.0-rc1 | 2024-12-04 | – | -| 1 | [pimotte/TutteLean](https://github.com/pimotte/TutteLean) | | | v4.17.0-rc1 | 2025-03-11 | – | -| 1 | [pitmonticone/DualOfLp](https://github.com/pitmonticone/DualOfLp) | | Apache-2.0 | v4.24.0 | 2026-02-28 | – | -| 1 | [pitmonticone/NewProject](https://github.com/pitmonticone/NewProject) | | Apache-2.0 | | 2025-09-02 | ✓ | -| 1 | [Pjotr5/ShearerTriangleFreeInd](https://github.com/Pjotr5/ShearerTriangleFreeInd) | Lean 4 proofs of Shearer’s bound on independence number and a new bound on the number of independent sets in triangle-f… | | v4.28.0 | 2026-02-27 | – | -| 1 | [PolyB/LeanPythonRaw](https://github.com/PolyB/LeanPythonRaw) | Raw Lean4 bindings to python C-API | | nightly-2022-05-09 | 2022-10-08 | – | -| 1 | [Quantumplation/cardano-lean-specification](https://github.com/Quantumplation/cardano-lean-specification) | An experimental formalization of the Cardano ledger, written in Lean, inspired by https://github.com/IntersectMBO/forma… | | v4.15.0 | 2025-02-13 | – | -| 1 | [QuijoticResearch/volterra-levy](https://github.com/QuijoticResearch/volterra-levy) | | | v4.28.0 | 2026-03-31 | – | -| 1 | [rdevshp/c_operational_semantics_lean4](https://github.com/rdevshp/c_operational_semantics_lean4) | A Lean 4 port of the CompCert C front-end operational semantics. | LGPL-2.1 | v4.30.0-rc2 | 2026-05-05 | – | -| 1 | [riccardobrasca/formally_real](https://github.com/riccardobrasca/formally_real) | | Apache-2.0 | nightly-2023-06-20 | 2025-01-09 | – | -| 1 | [Rida-Hamadani/LeanHS1960](https://github.com/Rida-Hamadani/LeanHS1960) | | Apache-2.0 | v4.8.0-rc1 | 2025-07-02 | – | -| 1 | [rish987/qsort](https://github.com/rish987/qsort) | Program synthesis experiments in Lean | | nightly-2026-01-26 | 2026-04-17 | – | -| 1 | [robin-carlier/SymmMonCoherence](https://github.com/robin-carlier/SymmMonCoherence) | Lean4 formalization of the coherence theorem for symmetric monoidal categories | Apache-2.0 | v4.29.0-rc6 | 2026-03-16 | – | -| 1 | [roman3017/FinLin](https://github.com/roman3017/FinLin) | | | v4.26.0 | 2026-01-07 | – | -| 1 | [Ruben-VandeVelde/flt4](https://github.com/Ruben-VandeVelde/flt4) | | | nightly-2023-03-17 | 2023-05-19 | – | -| 1 | [RustyYato/lean4-math](https://github.com/RustyYato/lean4-math) | | | v4.20.0-rc2 | 2025-07-04 | – | -| 1 | [RustyYato/zfc](https://github.com/RustyYato/zfc) | | | nightly | 2024-08-20 | – | -| 1 | [ryanmacl/Emergent](https://github.com/ryanmacl/Emergent) | Emergent Gravity | | v4.21.0-rc3 | 2025-08-22 | – | -| 1 | [SamuelSchlesinger/introduction-to-modern-cryptography](https://github.com/SamuelSchlesinger/introduction-to-modern-cryptography) | Introduction to modern cryptography | | v4.28.0 | 2026-04-06 | – | -| 1 | [septract/claudes-cycles-lean](https://github.com/septract/claudes-cycles-lean) | | | v4.28.0 | 2026-03-10 | – | -| 1 | [shetzl/autth](https://github.com/shetzl/autth) | lean4 formalisation of some results in automata theory | Apache-2.0 | v4.12.0-rc1 | 2025-12-26 | – | -| 1 | [Shreyas4991/LeanFlows](https://github.com/Shreyas4991/LeanFlows) | | | v4.26.0-rc2 | 2026-02-25 | – | -| 1 | [sinhp/displayed_categories](https://github.com/sinhp/displayed_categories) | A Lean 4 formalization of Displayed Categories | | v4.19.0-rc3 | 2025-05-01 | – | -| 1 | [smorel394/ASC](https://github.com/smorel394/ASC) | | | nightly-2023-07-12 | 2024-05-30 | – | -| 1 | [smorel394/JeCasseTout](https://github.com/smorel394/JeCasseTout) | | | v4.2.0-rc1 | 2023-09-29 | – | -| 1 | [somombo/supertype](https://github.com/somombo/supertype) | Lean Subtypes that have Super powers | Apache-2.0 | stable | 2024-04-03 | – | -| 1 | [SproutSeeds/sunflower-lean](https://github.com/SproutSeeds/sunflower-lean) | | | v4.26.0 | 2026-04-03 | – | -| 1 | [SteffenReith/Crypto](https://github.com/SteffenReith/Crypto) | Some experiments with Lean4 and cryptographic algorithms | GPL-3.0 | v4.29.0 | 2026-05-02 | – | -| 1 | [tautastic/real-analysis](https://github.com/tautastic/real-analysis) | Lean4 formalization of Real Analysis | | v4.12.0-rc1 | 2024-10-23 | – | -| 1 | [tghyde/math301spring2025](https://github.com/tghyde/math301spring2025) | Repository for Math 301 at Vassar College in the Spring 2025 semester. | Apache-2.0 | v4.15.0 | 2025-04-06 | – | -| 1 | [tom111/BEI-lean](https://github.com/tom111/BEI-lean) | An attempt to formalize Binomial Edge Ideals in lean | | v4.28.0 | 2026-05-04 | – | -| 1 | [TwoFX/HashMap](https://github.com/TwoFX/HashMap) | | Apache-2.0 | nightly-2024-06-27 | 2024-06-28 | – | -| 1 | [typhdotcom/diaspora](https://github.com/typhdotcom/diaspora) | Diaspora: A toy universe of topology, using discrete hodge theory and Lean 4 | | v4.25.0-rc2 | 2025-12-16 | – | -| 1 | [ultronozm/LinearAlgebraLemma](https://github.com/ultronozm/LinearAlgebraLemma) | | | v4.28.0-rc1 | 2026-03-16 | – | -| 1 | [uw-math-ai/central_limit_theorem](https://github.com/uw-math-ai/central_limit_theorem) | | | v4.13.0-rc3 | 2025-12-13 | – | -| 1 | [uw-math-ai/random_graphs](https://github.com/uw-math-ai/random_graphs) | | | v4.3.0-rc1 | 2025-12-13 | – | -| 1 | [vbeffara/Curvint](https://github.com/vbeffara/Curvint) | | | | 2026-01-20 | – | -| 1 | [VerifiedQC/Lean-QEC](https://github.com/VerifiedQC/Lean-QEC) | | | v4.30.0-rc2 | 2026-05-07 | – | -| 1 | [volfenstein1/EilenbergSteenrodAxioms](https://github.com/volfenstein1/EilenbergSteenrodAxioms) | A formalization of the Eilenberg-Steenrod axioms in Lean | | v4.29.0-rc6 | 2026-04-07 | – | -| 1 | [Vtec234/lean-sat](https://github.com/Vtec234/lean-sat) | | Apache-2.0 | nightly-2022-05-23 | 2023-01-27 | – | -| 1 | [wildwestrom/smoothstep-curve-proof](https://github.com/wildwestrom/smoothstep-curve-proof) | | | v4.28.0-rc1 | 2026-04-03 | – | -| 1 | [wwylele/biased-bisect-lean](https://github.com/wwylele/biased-bisect-lean) | | Apache-2.0 | v4.30.0-rc1 | 2026-04-05 | – | -| 1 | [wwylele/HahnEmbedding](https://github.com/wwylele/HahnEmbedding) | | | v4.20.0-rc5 | 2025-09-14 | – | -| 1 | [xubaiw/BaseN.lean](https://github.com/xubaiw/BaseN.lean) | RFC 4648 compliant Base-N encoding in Lean 4 | | nightly-2022-06-16 | 2023-03-16 | – | -| 1 | [zaxioms0/LeanAlg](https://github.com/zaxioms0/LeanAlg) | A WIP linear algebra library for Lean | | nightly-2022-07-24 | 2023-02-10 | – | -| 0 | [21eleven/drink-lean-for-christmas-2023](https://github.com/21eleven/drink-lean-for-christmas-2023) | | | nightly | 2023-12-03 | – | -| 0 | [adamtopaz/lean_constant_data](https://github.com/adamtopaz/lean_constant_data) | | | v4.20.0-rc5 | 2025-05-23 | – | -| 0 | [adomasbaliuka/AdventOfCode2023](https://github.com/adomasbaliuka/AdventOfCode2023) | Advent of Code 2023 in Lean4 | MIT | v4.3.0 | 2023-12-01 | – | -| 0 | [adomasbaliuka/lean4-hacking](https://github.com/adomasbaliuka/lean4-hacking) | An attempt at setting up CI that disallows proofs of False, to be challenged by PRs | Apache-2.0 | v4.5.0 | 2024-08-27 | – | -| 0 | [AishwaryaS-561/Lean-setup](https://github.com/AishwaryaS-561/Lean-setup) | Lean setup for testing | | v4.26.0-rc2 | 2025-12-08 | – | -| 0 | [ajhendel/PlatonicSolids](https://github.com/ajhendel/PlatonicSolids) | Freek #50: Exactly five Platonic solids, formalized in Lean 4 + Mathlib | | v4.29.1 | 2026-05-05 | – | -| 0 | [alainchmt/CertifyingInvariantsNF](https://github.com/alainchmt/CertifyingInvariantsNF) | Formally certifying invariants of number fields in Lean | | v4.30.0-rc1 | 2026-05-08 | – | -| 0 | [alainchmt/SturmTheorem](https://github.com/alainchmt/SturmTheorem) | A formalization in Lean of Sturm's theorem for counting roots of polynomials defined over a real closed field. | | v4.20.0-rc5 | 2025-11-22 | – | -| 0 | [AlexBrodbelt/LeanIMO](https://github.com/AlexBrodbelt/LeanIMO) | Formalisation of IMO problems in Lean | | v4.11.0-rc2 | 2024-08-27 | – | -| 0 | [AlexCai007/Nagata-Theorem](https://github.com/AlexCai007/Nagata-Theorem) | formalization of Nagata Theorem | | v4.25.0-rc2 | 2025-12-05 | – | -| 0 | [alexjbest/aoc](https://github.com/alexjbest/aoc) | advent of code | | nightly-2022-11-30 | 2022-12-01 | – | -| 0 | [alexjbest/lorentz](https://github.com/alexjbest/lorentz) | | | nightly-2023-06-20 | 2023-07-06 | – | -| 0 | [anandijain/DocTest3.lean](https://github.com/anandijain/DocTest3.lean) | | | v4.27.0-rc1 | 2026-01-01 | – | -| 0 | [Anderssorby/LeanPlay](https://github.com/Anderssorby/LeanPlay) | A play project using lean4 | | stable | 2022-03-08 | – | -| 0 | [AnirudhG07/LeanBWT-Bzip2](https://github.com/AnirudhG07/LeanBWT-Bzip2) | Lean Bzip2 compression library using Burrows Wheeler Transformation. | MIT | v4.29.0 | 2026-05-07 | – | -| 0 | [anishrajeev/ModelTheoryFun](https://github.com/anishrajeev/ModelTheoryFun) | | | v4.25.0-rc2 | 2025-12-25 | – | -| 0 | [AntanasKal/Advent-of-Code-2023](https://github.com/AntanasKal/Advent-of-Code-2023) | My Advent of Code 2023 solutions in Lean4 | | v4.4.0-rc1 | 2023-12-02 | – | -| 0 | [anzenlang/arrow.lean](https://github.com/anzenlang/arrow.lean) | Arrow's theorem. | Apache-2.0 | v4.7.0 | 2024-05-01 | – | -| 0 | [anzenlang/zen](https://github.com/anzenlang/zen) | Hopefully useful Lean 4 things. | | v4.16.0 | 2025-02-17 | – | -| 0 | [argumentcomputer/LightData](https://github.com/argumentcomputer/LightData) | A lightweight serialization format | MIT | nightly-2023-01-10 | 2023-03-23 | – | -| 0 | [arienmalec/mwe](https://github.com/arienmalec/mwe) | | | nightly-2023-01-04 | 2023-01-06 | – | -| 0 | [arthur-adjedj/AOC](https://github.com/arthur-adjedj/AOC) | | | nightly | 2024-12-03 | – | -| 0 | [ashanidasgupta1/mathlib-geometry](https://github.com/ashanidasgupta1/mathlib-geometry) | The intrinsic geometry of the Lean 4 Mathlib dependency graph: Tree of Cliques, Poincaré embeddings, and geometry-guide… | MIT | v4.29.0-rc3 | 2026-03-15 | – | -| 0 | [austinletson/warningtest](https://github.com/austinletson/warningtest) | | | stable | 2024-11-27 | – | -| 0 | [AviCraimer/lean-math-logic-exploration](https://github.com/AviCraimer/lean-math-logic-exploration) | My attempts to define and prove things about various concepts from math an logic using the Lean 4 theorem proving langu… | | v4.5.0-rc1 | 2024-09-24 | – | -| 0 | [avoair/Hausdorff](https://github.com/avoair/Hausdorff) | | | v4.20.0 | 2025-12-30 | – | -| 0 | [ayhon/iris-loogle](https://github.com/ayhon/iris-loogle) | A loogle instance with `iris-lean` included. | Apache-2.0 | v4.29.0 | 2026-04-29 | – | -| 0 | [badly-drawn-wizards/impdf](https://github.com/badly-drawn-wizards/impdf) | Dataflow for Imp in Lean4 | | v4.7.0-rc2 | 2024-03-18 | – | -| 0 | [badly-drawn-wizards/sqlean](https://github.com/badly-drawn-wizards/sqlean) | Lean4 library for sqlite | | nightly | 2024-01-13 | – | -| 0 | [bglgwyng/lean-playground](https://github.com/bglgwyng/lean-playground) | | | 4.18.0 | 2025-04-21 | – | -| 0 | [bjoernkjoshanssen/biocalculus](https://github.com/bjoernkjoshanssen/biocalculus) | Lean4 formalized facts related to "Biocalculus" by Stewart and Day. | | v4.11.0-rc1 | 2024-08-30 | – | -| 0 | [bjoernkjoshanssen/jxm](https://github.com/bjoernkjoshanssen/jxm) | Protein folding by recursive backtracking: Lean 4 project | | v4.14.0-rc2 | 2024-11-10 | – | -| 0 | [bjoernkjoshanssen/marginis](https://github.com/bjoernkjoshanssen/marginis) | Marginis, the library of formal marginalia associated with the Journal of Logic and Analysis. | | v4.13.0-rc3 | 2026-02-13 | – | -| 0 | [blacksph3re/distribution_factors](https://github.com/blacksph3re/distribution_factors) | An attempt to formalize DC loadflow equations and distribution factors in lean | | v4.15.0-rc1 | 2025-02-16 | – | -| 0 | [boisgera/lean-tasks](https://github.com/boisgera/lean-tasks) | | | v4.26.0 | 2026-01-15 | – | -| 0 | [bollu/lean4_docs](https://github.com/bollu/lean4_docs) | The lean4 source code + documentation generated by leanprover/doc-gen4 | | nightly-2022-03-06 | 2022-02-15 | – | -| 0 | [BoltonBailey/moser](https://github.com/BoltonBailey/moser) | | | v4.30.0-rc2 | 2026-04-30 | – | -| 0 | [brittlewis12/witness-budgets](https://github.com/brittlewis12/witness-budgets) | | | v4.25.0-rc2 | 2025-11-27 | – | -| 0 | [bryangingechen/erdos707](https://github.com/bryangingechen/erdos707) | | | v4.24.0-rc1 | 2025-10-22 | – | -| 0 | [bryangingechen/shake-bug-inferInstanceAs](https://github.com/bryangingechen/shake-bug-inferInstanceAs) | | | v4.30.0-rc1 | 2026-04-15 | – | -| 0 | [bryangingechen/shake-bug-meta-import-flip](https://github.com/bryangingechen/shake-bug-meta-import-flip) | | | v4.30.0-rc2 | 2026-05-01 | – | -| 0 | [BuildCoherence/Blake3Lean4](https://github.com/BuildCoherence/Blake3Lean4) | BLAKE3 implementation in pure Lean. | MIT | v4.28.0 | 2026-03-02 | – | -| 0 | [Calculean/LeanCCS](https://github.com/Calculean/LeanCCS) | | | v4.9.0-rc1 | 2024-08-25 | – | -| 0 | [cameronfreer/infinitary-logic](https://github.com/cameronfreer/infinitary-logic) | | Apache-2.0 | v4.27.0 | 2026-05-08 | – | -| 0 | [CBirkbeck/DirichletNonvanishing](https://github.com/CBirkbeck/DirichletNonvanishing) | | Apache-2.0 | v4.13.0-rc3 | 2024-11-18 | – | -| 0 | [CBirkbeck/LeanModularForms](https://github.com/CBirkbeck/LeanModularForms) | | | v4.29.0-rc8 | 2026-04-07 | – | -| 0 | [CBirkbeck/WeilConverse](https://github.com/CBirkbeck/WeilConverse) | | Apache-2.0 | v4.11.0-rc2 | 2024-08-23 | – | -| 0 | [chrisathmedu/elligator](https://github.com/chrisathmedu/elligator) | | | v4.29.0-rc7 | 2026-04-11 | – | -| 0 | [ChrisHughes24/lean4stuff](https://github.com/ChrisHughes24/lean4stuff) | | | v4.2.0-rc4 | 2022-06-27 | – | -| 0 | [christiankithimaomba-cyber/spectral-reduction-framework](https://github.com/christiankithimaomba-cyber/spectral-reduction-framework) | Formalization of the Spectral Reduction Lemma and complexity class analysis in Lean 4. | | | 2026-04-03 | – | -| 0 | [Citronhat/PeanoRec](https://github.com/Citronhat/PeanoRec) | | | v4.21.0-rc3 | 2025-06-28 | – | -| 0 | [codeguru42/lean4-tutorial](https://github.com/codeguru42/lean4-tutorial) | | | v4.25.2 | 2026-05-01 | – | -| 0 | [cognivore/FuncDep.lean](https://github.com/cognivore/FuncDep.lean) | Functional dependencies in Lean 4 | | nightly-2022-05-29 | 2022-07-07 | – | -| 0 | [crabbo-rave/lean4-Hangman](https://github.com/crabbo-rave/lean4-Hangman) | UNFINISHED | | nightly-2022-01-04 | 2022-03-26 | – | -| 0 | [ctzurcanu/lean-measure](https://github.com/ctzurcanu/lean-measure) | Lean 4 lib for Quality, Quantity, Measure, Unit | GPL-3.0 | v4.10.0-rc2 | 2025-01-19 | – | -| 0 | [Danelnov/weak-nullstellensatz](https://github.com/Danelnov/weak-nullstellensatz) | | | v4.30.0-rc1 | 2026-04-14 | – | -| 0 | [dhyan-aranha/SorryDBTest422](https://github.com/dhyan-aranha/SorryDBTest422) | | | v4.22.0 | 2025-10-28 | – | -| 0 | [dhyan-aranha/tracingtest](https://github.com/dhyan-aranha/tracingtest) | | | v4.18.0 | 2025-04-16 | – | -| 0 | [doxtor6/MerLean_NumberTheory](https://github.com/doxtor6/MerLean_NumberTheory) | | | v4.28.0 | 2026-04-20 | – | -| 0 | [drhodes/minilib](https://github.com/drhodes/minilib) | A onefile lean library project | | stable | 2024-10-07 | – | -| 0 | [dupuisf/Lean4_AoC2022](https://github.com/dupuisf/Lean4_AoC2022) | My solutions to Advent of Code 2022 in Lean 4 | | | 2022-12-02 | – | -| 0 | [edegeltje/CwFTT](https://github.com/edegeltje/CwFTT) | | | v4.29.0-rc4 | 2026-03-05 | – | -| 0 | [edegeltje/Mathieu_12_simple](https://github.com/edegeltje/Mathieu_12_simple) | | | v4.6.0-rc1 | 2024-02-06 | – | -| 0 | [Eduardogbg/lean-play](https://github.com/Eduardogbg/lean-play) | | | v4.20.0-rc5 | 2025-06-18 | – | -| 0 | [elazarg/kraft](https://github.com/elazarg/kraft) | Proof of Kraft's inequality in Lean | | v4.26.0 | 2026-01-23 | – | -| 0 | [Eparoh/Functional_Analysis](https://github.com/Eparoh/Functional_Analysis) | | | v4.15.0-rc1 | 2024-12-20 | – | -| 0 | [Equilibris/Shrink](https://github.com/Equilibris/Shrink) | | | nightly-2025-06-27 | 2025-07-27 | – | -| 0 | [eric-wieser/navier-stokes-misformalization](https://github.com/eric-wieser/navier-stokes-misformalization) | Solving the* Navier Stokes Millenium problem in Lean | Apache-2.0 | v4.18.0-rc1 | 2026-01-03 | – | -| 0 | [ericluap/AutLinOrd](https://github.com/ericluap/AutLinOrd) | Automorphisms of Linear Orders | | v4.27.0-rc1 | 2025-12-27 | – | -| 0 | [ertwro/one_third_two_thirds](https://github.com/ertwro/one_third_two_thirds) | | | v4.28.0 | 2026-03-15 | – | -| 0 | [femtomc/pls.lean](https://github.com/femtomc/pls.lean) | | | v4.5.0-rc1 | 2023-12-28 | – | -| 0 | [FernandoChu/DisplayedComparison](https://github.com/FernandoChu/DisplayedComparison) | Comparison of notions of displayed categories in Lean | | v4.20.0-rc2 | 2025-05-03 | – | -| 0 | [fgdorais/GMLAlgebra](https://github.com/fgdorais/GMLAlgebra) | GML Algebra Package | CC0-1.0 | v4.16.0-rc2 | 2025-01-18 | – | -| 0 | [fgdorais/lean4-unicode-lemmas](https://github.com/fgdorais/lean4-unicode-lemmas) | Lemmas for UnicodeBasic | | v4.22.0-rc3 | 2025-07-22 | – | -| 0 | [FLDutchmann/Analytic](https://github.com/FLDutchmann/Analytic) | | Apache-2.0 | v4.25.0-rc2 | 2025-10-23 | – | -| 0 | [FMLJohn/HilbertPolynomial](https://github.com/FMLJohn/HilbertPolynomial) | | Apache-2.0 | v4.18.0-rc1 | 2026-04-01 | – | -| 0 | [fNBU/aoc23](https://github.com/fNBU/aoc23) | | | v4.3.0 | 2023-12-05 | – | -| 0 | [FormalizedFormalLogic/Summary](https://github.com/FormalizedFormalLogic/Summary) | Documentation of this project | | v4.16.0-rc2 | 2025-03-09 | – | -| 0 | [frankvegadelgado/GoldbachConjecture](https://github.com/frankvegadelgado/GoldbachConjecture) | Lean on Goldbach's conjecture | MIT | v4.27.0-rc1 | 2026-03-27 | – | -| 0 | [FrederickPu/AutoformalizationUtils](https://github.com/FrederickPu/AutoformalizationUtils) | | MIT | v4.28.0 | 2026-04-08 | – | -| 0 | [FrederickPu/TeryGrad](https://github.com/FrederickPu/TeryGrad) | | | v4.15.0-rc1 | 2024-12-27 | – | -| 0 | [frenzymath/openai_client](https://github.com/frenzymath/openai_client) | A clean OpenAI-compatible client for Lean 4 | Apache-2.0 | v4.26.0-rc1 | 2026-04-10 | – | -| 0 | [FruitfulApproach/Lean4TPC](https://github.com/FruitfulApproach/Lean4TPC) | A Lean4 project that formally proves the Twin Prime Conjecture (TPC) using properties of monoids. | CC0-1.0 | v4.29.0-rc6 | 2026-05-01 | – | -| 0 | [GeQi/project](https://github.com/GeQi/project) | | | v4.7.0 | 2024-04-26 | – | -| 0 | [gmcninch-prof/LeanAlg](https://github.com/gmcninch-prof/LeanAlg) | Lean project(s) in algebra | | v4.30.0-rc1 | 2026-04-12 | – | -| 0 | [godswealtholuwabunmi-crypto/Rim-depth-and-hilbertsmith-formalization](https://github.com/godswealtholuwabunmi-crypto/Rim-depth-and-hilbertsmith-formalization) | A Lean formalization of a new topological invariant named rdim and the hilbertsmith formalization in lean | | v4.29.0 | 2026-04-29 | – | -| 0 | [Gravifer/lean-mathlib-1stproj](https://github.com/Gravifer/lean-mathlib-1stproj) | Personal first project using Lean with Mathlib | | v4.24.0-rc1 | 2025-10-21 | – | -| 0 | [gterzian/lean_concurrency](https://github.com/gterzian/lean_concurrency) | From TLA+ to Lean | MIT | v4.28.0 | 2026-03-05 | – | -| 0 | [guptbot/free_will_lean](https://github.com/guptbot/free_will_lean) | | | v4.15.0-rc1 | 2024-12-13 | – | -| 0 | [gw90/ThesisProjectRepo](https://github.com/gw90/ThesisProjectRepo) | | | v4.27.0-rc1 | 2025-12-22 | – | -| 0 | [hargoniX/lean-ink-bug](https://github.com/hargoniX/lean-ink-bug) | | | nightly-2022-05-31 | 2022-06-09 | – | -| 0 | [hargoniX/lean4-c-bug](https://github.com/hargoniX/lean4-c-bug) | | | nightly-2022-03-30 | 2022-03-31 | – | -| 0 | [hhu-adam/i18n-demo](https://github.com/hhu-adam/i18n-demo) | | | v4.6.0 | 2024-03-01 | – | -| 0 | [hotdogontology/student_project](https://github.com/hotdogontology/student_project) | | | v4.7.0 | 2024-05-14 | – | -| 0 | [hyunsanghwang/matroid](https://github.com/hyunsanghwang/matroid) | | | nightly-2023-05-16 | 2023-06-25 | – | -| 0 | [ianjauslin-rutgers/lean-complex-has_primitives](https://github.com/ianjauslin-rutgers/lean-complex-has_primitives) | | Apache-2.0 | v4.4.0-rc1 | 2023-12-08 | – | -| 0 | [iarnoldy/UFT](https://github.com/iarnoldy/UFT) | | | v4.29.0-rc4 | 2026-03-22 | – | -| 0 | [imbrem/refined-ssa](https://github.com/imbrem/refined-ssa) | | | v4.16.0-rc2 | 2025-01-22 | – | -| 0 | [impermeable/waterproof-genre](https://github.com/impermeable/waterproof-genre) | | MIT | v4.29.0-rc3 | 2026-03-02 | – | -| 0 | [imran-tanrikolu/Napoleon-s-Theorem-in-Lean4](https://github.com/imran-tanrikolu/Napoleon-s-Theorem-in-Lean4) | | | v4.15.0 | 2026-04-16 | – | -| 0 | [irunkel/HopfAlgebras](https://github.com/irunkel/HopfAlgebras) | A project on Hopf algebras to try and learn about Lean4 | Apache-2.0 | v4.7.0-rc2 | 2024-03-20 | – | -| 0 | [JADekker/PiBaseTracking](https://github.com/JADekker/PiBaseTracking) | | | v4.6.0-rc1 | 2024-04-25 | – | -| 0 | [janemms/BanachAlaoglu](https://github.com/janemms/BanachAlaoglu) | | | v4.21.0-rc3 | 2025-07-27 | – | -| 0 | [jaredgreen2/polySat](https://github.com/jaredgreen2/polySat) | a solver | | v4.15.0 | 2025-01-21 | – | -| 0 | [jeremysalwen/advent_of_lean_2022](https://github.com/jeremysalwen/advent_of_lean_2022) | Verified solutions to Advent of Code in Lean4 | | nightly-2023-01-21 | 2023-01-03 | – | -| 0 | [jeremysalwen/Lean4-Translate-Tactic](https://github.com/jeremysalwen/Lean4-Translate-Tactic) | A prototype Lean4 tactic for translating propositions through isomorphisms. | | nightly-2023-05-16 | 2023-05-22 | – | -| 0 | [jeswr/lean_sys_test](https://github.com/jeswr/lean_sys_test) | | MIT | stable | 2024-02-24 | – | -| 0 | [jmoy/farkas_lean](https://github.com/jmoy/farkas_lean) | Theorems of the alternative etc. in Lean | MIT | v4.28.0 | 2026-03-05 | – | -| 0 | [joehendrix/lean-aes](https://github.com/joehendrix/lean-aes) | Experiements in coding up AES elegantly in Lean | | v4.7.0-rc2 | 2024-03-21 | – | -| 0 | [JonBannon/Junk-Test](https://github.com/JonBannon/Junk-Test) | | | v4.12.0-rc1 | 2026-01-15 | – | -| 0 | [joneugster/OptionTest](https://github.com/joneugster/OptionTest) | Tmp repo to play around with lake options | | v4.23.0 | 2025-09-28 | – | -| 0 | [joneugster/test_deprecation](https://github.com/joneugster/test_deprecation) | | | v4.8.0 | 2024-06-10 | – | -| 0 | [joneugster/testSrcDir2](https://github.com/joneugster/testSrcDir2) | | | v4.8.0 | 2024-06-10 | – | -| 0 | [josephmate/AdventOfCode2025](https://github.com/josephmate/AdventOfCode2025) | | | v4.26.0-rc2 | 2025-12-14 | – | -| 0 | [josephmckinsey/FleanBlogPost](https://github.com/josephmckinsey/FleanBlogPost) | | | v4.16.0 | 2025-03-06 | – | -| 0 | [jsmorph/FormalQualBench](https://github.com/jsmorph/FormalQualBench) | | Apache-2.0 | v4.28.0 | 2026-03-19 | – | -| 0 | [jt496/Turan_4](https://github.com/jt496/Turan_4) | | | v4.0.0-rc2 | 2023-08-29 | – | -| 0 | [katzenpost/lean-ffi](https://github.com/katzenpost/lean-ffi) | | | v4.13.0 | 2024-11-08 | – | -| 0 | [Kiiyya/lean-reflection](https://github.com/Kiiyya/lean-reflection) | For all inductive types, ... | | v4.5.0-rc1 | 2023-11-06 | – | -| 0 | [kim-em/lean-matroids4](https://github.com/kim-em/lean-matroids4) | | | nightly-2023-05-16 | 2025-05-25 | – | -| 0 | [kiranandcode/job-talk](https://github.com/kiranandcode/job-talk) | Kiran's Job Talk (in LeanTeX) | | v4.19.0-rc2 | 2025-05-26 | – | -| 0 | [KislyjKisel/mwe-require-externlib](https://github.com/KislyjKisel/mwe-require-externlib) | | | leanprover/lean4-nightly:nightly-2025-04-27 | 2025-04-28 | – | -| 0 | [KislyjKisel/mwe-require-externlib2](https://github.com/KislyjKisel/mwe-require-externlib2) | | | leanprover/lean4-nightly:nightly-2025-04-27 | 2025-04-28 | – | -| 0 | [klockeph/AdventOfCode2023](https://github.com/klockeph/AdventOfCode2023) | Advent of Code 2023 in Lean4 (noob) | Apache-2.0 | nightly | 2023-12-02 | – | -| 0 | [kuotsanhsu/lean4-dump](https://github.com/kuotsanhsu/lean4-dump) | | | stable | 2024-08-27 | – | -| 0 | [kuotsanhsu/lean4-tutorials](https://github.com/kuotsanhsu/lean4-tutorials) | | | v4.24.0 | 2025-10-29 | – | -| 0 | [laughinggas/padic-L-functions4](https://github.com/laughinggas/padic-L-functions4) | | | v4.19.0-rc3 | 2025-07-16 | – | -| 0 | [lauramonk/FriedmanStrongConv](https://github.com/lauramonk/FriedmanStrongConv) | Formalizing the new proof of Friedman's theorem using strong convergence | Apache-2.0 | v4.26.0-rc2 | 2026-04-09 | – | -| 0 | [leanprover/verso-website](https://github.com/leanprover/verso-website) | The Verso Website | Apache-2.0 | v4.28.0 | 2026-03-24 | – | -| 0 | [lecopivo/ForLoopSpeed](https://github.com/lecopivo/ForLoopSpeed) | Testing out Lean's for loop speed | | nightly-2023-03-15 | 2023-04-20 | – | -| 0 | [lecopivo/leanPluginTest](https://github.com/lecopivo/leanPluginTest) | | | nightly-2022-01-17 | 2022-01-18 | – | -| 0 | [lecopivo/LeanSAS](https://github.com/lecopivo/LeanSAS) | Lean Specialize and Simplify pre-compilation pass | | v4.27.0 | 2026-05-07 | – | -| 0 | [lecopivo/SimpleFFI](https://github.com/lecopivo/SimpleFFI) | Simple FFI project for Lean 4 | | v4.20.0-rc5 | 2025-05-30 | – | -| 0 | [LeGenAI/intersection-coding-theory-cohomology](https://github.com/LeGenAI/intersection-coding-theory-cohomology) | | | v4.29.0-rc6 | 2026-03-29 | – | -| 0 | [lephe/lean4-hbind](https://github.com/lephe/lean4-hbind) | Tests around a universe-polymorphic implementation of do notation in Lean 4. | | nightly-2022-07-13 | 2022-07-14 | – | -| 0 | [levzlotnik/lean4-dep-audit](https://github.com/levzlotnik/lean4-dep-audit) | | MIT | v4.29.0 | 2026-04-16 | – | -| 0 | [linesthatinterlace/xmss](https://github.com/linesthatinterlace/xmss) | | | v4.20.0-rc5 | 2025-05-08 | – | -| 0 | [loefflerd/ModularFormDimensions](https://github.com/loefflerd/ModularFormDimensions) | Finite-dimensionality of modular forms spaces | | v4.28.0-rc1 | 2026-02-12 | – | -| 0 | [loewenheim/projective-plane](https://github.com/loewenheim/projective-plane) | A toy axiomatization of projective planes in Lean4 | | nightly-2023-01-21 | 2023-01-25 | – | -| 0 | [loumaloulongtin/EpArch](https://github.com/loumaloulongtin/EpArch) | EpArch | MIT | v4.3.0 | 2026-04-24 | – | -| 0 | [lsqrl/LeanOraclePoC](https://github.com/lsqrl/LeanOraclePoC) | PoC for a Lean4 oracle which provides answers based on a specific environment | | v4.19.0-rc3 | 2025-07-09 | – | -| 0 | [madvorak/fractional](https://github.com/madvorak/fractional) | Fractional operations | Apache-2.0 | v4.13.0-rc2 | 2026-04-07 | – | -| 0 | [madvorak/lean-fft](https://github.com/madvorak/lean-fft) | | | | 2023-04-11 | – | -| 0 | [madvorak/lean-zcu](https://github.com/madvorak/lean-zcu) | Lean 4 ZČU | Unlicense | v4.29.0 | 2026-04-30 | – | -| 0 | [madvorak/lean4-course](https://github.com/madvorak/lean4-course) | Stand-alone pre-semester Lean 4 course at ISTA | | v4.1.0-rc1 | 2024-02-08 | – | -| 0 | [madvorak/lean4-exercises](https://github.com/madvorak/lean4-exercises) | | | nightly-2023-07-12 | 2024-02-08 | – | -| 0 | [madvorak/leanq](https://github.com/madvorak/leanq) | LINQ for Lean 4 | Unlicense | v4.21.0-rc3 | 2025-08-20 | – | -| 0 | [madvorak/leanters](https://github.com/madvorak/leanters) | Custom linters for Lean 4 | Apache-2.0 | v4.18.0 | 2025-06-22 | – | -| 0 | [madvorak/matrix-tu-experimental](https://github.com/madvorak/matrix-tu-experimental) | | Unlicense | v4.15.0-rc1 | 2025-01-13 | – | -| 0 | [madvorak/sup-lean](https://github.com/madvorak/sup-lean) | Attempt at importing multiple Lean projects | Apache-2.0 | v4.8.0-rc2 | 2024-05-31 | – | -| 0 | [malcin541/chi_boundedness](https://github.com/malcin541/chi_boundedness) | | | v4.29.0-rc6 | 2026-03-21 | – | -| 0 | [marcelolynch/LeanDownstreamPlayground](https://github.com/marcelolynch/LeanDownstreamPlayground) | A simulated mathlib downstream for experiments | | v4.30.0-rc2 | 2026-05-06 | – | -| 0 | [marcelolynch/timers](https://github.com/marcelolynch/timers) | Timing actions in Lean | | v4.27.0 | 2026-02-11 | – | -| 0 | [mariotrevi/cubic-frobenius-lean](https://github.com/mariotrevi/cubic-frobenius-lean) | A repo for formal proofs in Lean relating to a conjecture in explicit class field theory. | | v4.24.0 | 2026-02-13 | – | -| 0 | [markusdemedeiros/grind-extension-poc](https://github.com/markusdemedeiros/grind-extension-poc) | | | v4.28.0 | 2026-04-17 | – | -| 0 | [mattrobball/gb](https://github.com/mattrobball/gb) | | | nightly-2023-06-10 | 2023-06-23 | – | -| 0 | [mcdoll/DynamicalSystems](https://github.com/mcdoll/DynamicalSystems) | Library for formalization of dynamical systems | Apache-2.0 | v4.30.0-rc2 | 2026-05-04 | – | -| 0 | [mdnestor/SymbolicDynamics](https://github.com/mdnestor/SymbolicDynamics) | Formalization of the Curtis–Hedlund–Lyndon theorem in Lean 4 | | v4.11.0-rc3 | 2024-10-24 | – | -| 0 | [Menta2357/lean-menta-v6](https://github.com/Menta2357/lean-menta-v6) | Formalized functional equivalence HR ⇔ ζ̃_Q(s) ∈ F in Lean 4 | | v4.19.0 | 2025-05-15 | – | -| 0 | [MichaelStollBayreuth/JacobiSum](https://github.com/MichaelStollBayreuth/JacobiSum) | Results on Jacobi Sums | Apache-2.0 | v4.26.0-rc2 | 2025-12-02 | – | -| 0 | [miguelmarco/SmithForm](https://github.com/miguelmarco/SmithForm) | verified computable implementation of Smith form in Lean | | v4.27.0-rc1 | 2026-04-25 | – | -| 0 | [mo271/DocgenTest](https://github.com/mo271/DocgenTest) | | Apache-2.0 | v4.19.0-rc3 | 2025-04-16 | – | -| 0 | [mo271/mwe](https://github.com/mo271/mwe) | mwe for lean4 | | nightly-2023-03-31 | 2023-04-08 | – | -| 0 | [mo271/TestProject](https://github.com/mo271/TestProject) | Testing weird filenames with doc4-gen | Apache-2.0 | v4.7.0 | 2024-04-21 | – | -| 0 | [MohanadAhmed/dotProd_outside_math](https://github.com/MohanadAhmed/dotProd_outside_math) | | | nightly-2023-07-29 | 2023-07-29 | – | -| 0 | [monsterkrampe/Basic-Lean-Datastructures](https://github.com/monsterkrampe/Basic-Lean-Datastructures) | A collection of some definitions around basic data structures, e.g. Sets in Lean. This is in parts deviating from exist… | Apache-2.0 | v4.29.0 | 2026-04-14 | – | -| 0 | [monsterkrampe/Leaning-In-2025](https://github.com/monsterkrampe/Leaning-In-2025) | A template repo for the interactive part of my Leaning In 2025 presentation on Possibly Infinite Trees. | | v4.17.0 | 2025-03-14 | – | -| 0 | [mpenciak/FordhamSp2023](https://github.com/mpenciak/FordhamSp2023) | | | v4.2.0 | 2023-04-02 | – | -| 0 | [mrdouglasny/GFF4D](https://github.com/mrdouglasny/GFF4D) | A Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms | Apache-2.0 | v4.28.0 | 2026-02-26 | – | -| 0 | [nemustudies/attention-loop](https://github.com/nemustudies/attention-loop) | a mathematical object in which attention feeds back into itself. given the requirement that the loop be self-consistent… | | v4.28.0 | 2026-03-05 | – | -| 0 | [NicolasRouquette/dimensional-calculus.lean4](https://github.com/NicolasRouquette/dimensional-calculus.lean4) | | | ��leanprover/lean4:nightly | 2022-07-27 | – | -| 0 | [NicolasRouquette/oml.lean4](https://github.com/NicolasRouquette/oml.lean4) | Experiments in defining the Ontological Modeling Language in Lean4 | | nightly-2022-12-24 | 2022-12-23 | – | -| 0 | [NicolasRouquette/wip-graph-theory](https://github.com/NicolasRouquette/wip-graph-theory) | WIP on graph theory based on mathlib and or4nge19/MCMC | Apache-2.0 | v4.26.0-rc2 | 2026-01-13 | – | -| 0 | [NoneMore/model_theory_in_lean](https://github.com/NoneMore/model_theory_in_lean) | | | v4.27.0-rc1 | 2026-02-27 | – | -| 0 | [novaspivack/infinity-compression-lean](https://github.com/novaspivack/infinity-compression-lean) | The Infinity Compression Lean Library | | v4.29.0-rc6 | 2026-04-16 | – | -| 0 | [or4nge19/HopfieldNet](https://github.com/or4nge19/HopfieldNet) | | MIT | v4.20.0-rc5 | 2025-06-03 | – | -| 0 | [or4nge19/ThermodynamicsLean](https://github.com/or4nge19/ThermodynamicsLean) | | Apache-2.0 | v4.24.0-rc1 | 2025-10-26 | – | -| 0 | [palani-johnson/advent-lean4-2024](https://github.com/palani-johnson/advent-lean4-2024) | | | 4.15.0 | 2025-01-18 | – | -| 0 | [pandaman64/lean4-module-tests](https://github.com/pandaman64/lean4-module-tests) | | | v4.28.0 | 2026-03-06 | – | -| 0 | [pandaman64/program-verifications](https://github.com/pandaman64/program-verifications) | | | v4.25.1 | 2025-12-01 | – | -| 0 | [PatrickMassot/LspExperiments](https://github.com/PatrickMassot/LspExperiments) | | Apache-2.0 | v4.18.0-rc1 | 2025-03-16 | – | -| 0 | [PatrickMassot/verbose-lean-demo](https://github.com/PatrickMassot/verbose-lean-demo) | | | v4.26.0 | 2026-02-01 | – | -| 0 | [patrickrd/CLT-lindeberg](https://github.com/patrickrd/CLT-lindeberg) | | Apache-2.0 | v4.29.0-rc3 | 2026-04-15 | – | -| 0 | [petekos-math/HarFunctionsOnGroups](https://github.com/petekos-math/HarFunctionsOnGroups) | This is the repository for the Lean formalization of facts about harmonic functions on groups. | | v4.27.0-rc1 | 2026-02-22 | – | -| 0 | [phasetr/ising-model](https://github.com/phasetr/ising-model) | | | v4.29.0 | 2026-05-09 | – | -| 0 | [pimotte/fullstackalpha](https://github.com/pimotte/fullstackalpha) | | Apache-2.0 | nightly-2023-06-23 | 2023-07-09 | – | -| 0 | [pimotte/wp-lean-format-prototype](https://github.com/pimotte/wp-lean-format-prototype) | | | v4.20.0 | 2025-10-24 | – | -| 0 | [prodgang/prodproofs](https://github.com/prodgang/prodproofs) | | | v4.30.0-rc2 | 2026-05-09 | – | -| 0 | [project-numina/BrascampLieb](https://github.com/project-numina/BrascampLieb) | A Lean4 repository for formalization of results from "Effective Brascamp-Lieb Inequalities" | | v4.28.0 | 2026-04-10 | – | -| 0 | [PSchwahn/IncidenceGeometry](https://github.com/PSchwahn/IncidenceGeometry) | A Lean formalization project of incidence geometry, in particular affine and projective spaces. | | v4.24.0-rc1 | 2025-10-11 | – | -| 0 | [qawbecrdtey/magma](https://github.com/qawbecrdtey/magma) | | | v4.23.0-rc2 | 2025-11-21 | – | -| 0 | [QuijoticResearch/banach-levy-lean](https://github.com/QuijoticResearch/banach-levy-lean) | | | v4.28.0 | 2026-03-23 | – | -| 0 | [QuijoticResearch/operator-derivative-lean](https://github.com/QuijoticResearch/operator-derivative-lean) | | | v4.29.0-rc6 | 2026-03-23 | – | -| 0 | [quinnculver/MacaulayDuration](https://github.com/quinnculver/MacaulayDuration) | Lean4 code for financial math results about Macaulay & Modified duration | | v4.7.0 | 2024-10-09 | – | -| 0 | [R-Peleg/DPLib](https://github.com/R-Peleg/DPLib) | | | v4.26.0-rc2 | 2026-01-06 | – | -| 0 | [ramonfmir/FFIGMP](https://github.com/ramonfmir/FFIGMP) | | | nightly-2023-06-20 | 2023-06-27 | – | -| 0 | [rdeager/adinkra-lean4](https://github.com/rdeager/adinkra-lean4) | Adinkra formalization for mathlib | Apache-2.0 | v4.28.0-rc1 | 2026-02-05 | – | -| 0 | [requitefahrenheit/davenport-eta-cp3](https://github.com/requitefahrenheit/davenport-eta-cp3) | Lean 4 proof of η(C_p³) ≥ 8(p−1)+1 for odd primes — improving Harborth's bound | | v4.14.0 | 2026-03-22 | – | -| 0 | [rkirov/claude-cycles-lean](https://github.com/rkirov/claude-cycles-lean) | Formalization of Knuth's Claude Cycles paper | MIT | v4.28.0 | 2026-03-12 | – | -| 0 | [rkirov/jacobian-claude](https://github.com/rkirov/jacobian-claude) | Claude code trying to formalize Jacobians. I don't understand the math, and haven't reviewed any of this. | Apache-2.0 | v4.30.0-rc1 | 2026-04-25 | – | -| 0 | [rmhi/cts_cohomology](https://github.com/rmhi/cts_cohomology) | | | v4.17.0-rc1 | 2025-02-19 | – | -| 0 | [RobinPetit/graphs-in-lean](https://github.com/RobinPetit/graphs-in-lean) | Graphs. And Lean. | | v4.28.0 | 2026-05-06 | – | -| 0 | [roos-j/lean-oscillatory](https://github.com/roos-j/lean-oscillatory) | Formalization of oscillatory integral theory in Lean 4 | | v4.30.0-rc1 | 2026-04-11 | – | -| 0 | [RoyGBivens137/Reusable](https://github.com/RoyGBivens137/Reusable) | Repository for reusable LEAN theorems | Apache-2.0 | v4.28.0-rc1 | 2026-02-11 | – | -| 0 | [Ruben-VandeVelde/eqns](https://github.com/Ruben-VandeVelde/eqns) | | | nightly-2024-03-17 | 2024-03-17 | – | -| 0 | [runbikeswim/lean-math-puzzles](https://github.com/runbikeswim/lean-math-puzzles) | math puzzles with solutions in Lean | Apache-2.0 | v4.24.0 | 2025-11-19 | – | -| 0 | [runbikeswim/verso-test](https://github.com/runbikeswim/verso-test) | | | v4.26.0-rc1 | 2025-11-19 | – | -| 0 | [RustyYato/lean-root2](https://github.com/RustyYato/lean-root2) | | | nightly-2023-04-11 | 2023-04-17 | – | -| 0 | [rwst/lean-code](https://github.com/rwst/lean-code) | casual products of playing with Lean theorem prover, mostly intermediates of PRs to other projects, from 2026 on LLM-pr… | CC0-1.0 | v4.30.0-rc1 | 2026-04-17 | – | -| 0 | [sahanwijetunga/Hyperbolic](https://github.com/sahanwijetunga/Hyperbolic) | Lean Project formalizing Hyperbolic Spaces | | v4.22.0-rc4 | 2025-12-31 | – | -| 0 | [samueloettl/lean4_density](https://github.com/samueloettl/lean4_density) | | Apache-2.0 | v4.28.0-rc1 | 2026-02-10 | – | -| 0 | [SashaIr/qt-catalan](https://github.com/SashaIr/qt-catalan) | Formalization of the q,t-Catalan theorem by Garsia and Haglund | Apache-2.0 | v4.26.0-rc2 | 2025-12-12 | – | -| 0 | [satiscugcat/assertion-insecurity-lean](https://github.com/satiscugcat/assertion-insecurity-lean) | | | v4.21.0-rc3 | 2025-10-01 | – | -| 0 | [seanm27lol/Liquid-tft-lean-CM4CM-](https://github.com/seanm27lol/Liquid-tft-lean-CM4CM-) | Lean Proofs for start of a mini program | MIT | v4.28.0 | 2026-03-31 | – | -| 0 | [Seasawher/lean99](https://github.com/Seasawher/lean99) | まだWIP | Apache-2.0 | v4.25.0-rc2 | 2025-11-04 | – | -| 0 | [Seasawher/mathlib4-options](https://github.com/Seasawher/mathlib4-options) | all options in mathlib4 | | v4.2.0-rc4 | 2023-10-20 | – | -| 0 | [Seasawher/mwe-environment-error](https://github.com/Seasawher/mwe-environment-error) | | | v4.23.0 | 2025-10-09 | – | -| 0 | [Seasawher/SelectionSort.lean](https://github.com/Seasawher/SelectionSort.lean) | selection sort implemented and verified by lean | | v4.22.0-rc3 | 2025-07-05 | – | -| 0 | [Seasawher/Semver.lean](https://github.com/Seasawher/Semver.lean) | get latest (pre)release of Lean when list of versions is given | | 4.10.0 | 2024-08-26 | – | -| 0 | [sgraf812/LeanCorres](https://github.com/sgraf812/LeanCorres) | Vibe-coding a AutoCorres2 thing in Lean | | leanprover/lean4-nightly:nightly-2026-03-12 | 2026-04-07 | – | -| 0 | [shaazib-tanvir/ContextFree](https://github.com/shaazib-tanvir/ContextFree) | A lean formalization of some theorems related to Context Free Grammars | | v4.29.0-rc3 | 2026-03-21 | – | -| 0 | [sharky564/SharkyLeanStuff](https://github.com/sharky564/SharkyLeanStuff) | Just trying some stuff in Lean 4 | | v4.28.0 | 2026-03-06 | – | -| 0 | [shingtaklam1324/iva](https://github.com/shingtaklam1324/iva) | | | nightly-2022-06-11 | 2022-06-15 | – | -| 0 | [Shreyas4991/DiscreteMathLean](https://github.com/Shreyas4991/DiscreteMathLean) | | | v4.3.0 | 2023-12-12 | – | -| 0 | [Shreyas4991/Sorting-in-Lean](https://github.com/Shreyas4991/Sorting-in-Lean) | An attempt at building a collection of efficient sorting algorithms in lean | | v4.22.0 | 2025-08-25 | – | -| 0 | [Shreyas4991/Vibe-Code-Experiment-Consensus](https://github.com/Shreyas4991/Vibe-Code-Experiment-Consensus) | This repo is my first attempt to 100% vibe code a formal proof development. It is a failure. Make of it what you will | Apache-2.0 | v4.26.0 | 2026-02-04 | – | -| 0 | [siddhartha-gadgil/Leantegration](https://github.com/siddhartha-gadgil/Leantegration) | Symbolic integration in Lean: Data generation for AI prompting/fine tuning | Apache-2.0 | v4.6.1 | 2024-02-25 | – | -| 0 | [smorel394/Appendix](https://github.com/smorel394/Appendix) | | | v4.27.0-rc1 | 2026-01-26 | – | -| 0 | [SmwYin/Thue](https://github.com/SmwYin/Thue) | A formalised proof of "The only solutions in integers of the Thue equation x³-2y³=1 are (1,0) and (-1,-1)." | | v4.29.0 | 2026-04-25 | – | -| 0 | [SnO2WMaN/mwe-import-mathlib-order-propinstances](https://github.com/SnO2WMaN/mwe-import-mathlib-order-propinstances) | | | v4.22.0-rc3 | 2025-07-09 | – | -| 0 | [somombo/murder-mystery](https://github.com/somombo/murder-mystery) | a logic murder mystery word problem solved in lean prover | Apache-2.0 | nightly-2023-05-16 | 2023-03-07 | – | -| 0 | [somombo/try_math_exec](https://github.com/somombo/try_math_exec) | | | v4.0.0 | 2023-09-20 | – | -| 0 | [srghma/lean-glob-posix](https://github.com/srghma/lean-glob-posix) | | | v4.20.0-rc2 | 2025-07-08 | – | -| 0 | [ssar/euler_lean](https://github.com/ssar/euler_lean) | | | v4.16.0-rc2 | 2025-03-01 | – | -| 0 | [stagiralabs/agoralib](https://github.com/stagiralabs/agoralib) | | | v4.17.0 | 2025-12-30 | – | -| 0 | [SteamPunkPhysics/Polyhedral-Loop-Lean](https://github.com/SteamPunkPhysics/Polyhedral-Loop-Lean) | These are the lean files for the geometric proof paper: "The Golden-Ratio Polyhedral Journey: A Complete Forward Loop f… | MIT | v4.28.0-rc1 | 2026-02-11 | – | -| 0 | [SteamPunkPhysics/Primes-as-Forbidden-Harmonics](https://github.com/SteamPunkPhysics/Primes-as-Forbidden-Harmonics) | These are the lean files for the number theory proof paper: "Every Prime is a Forbidden Harmonic How Icosahedral Geomet… | MIT | v4.28.0-rc1 | 2026-02-19 | – | -| 0 | [StevenClontz/formalized-selection-games](https://github.com/StevenClontz/formalized-selection-games) | | | v4.13.0-rc3 | 2024-10-13 | – | -| 0 | [suhr/lambda](https://github.com/suhr/lambda) | A bit of simply typed lambda calculus in Lean | MIT | v4.25.1 | 2025-12-29 | – | -| 0 | [suhr/polygon](https://github.com/suhr/polygon) | | MIT | v4.16.0 | 2025-03-06 | – | -| 0 | [suhr/tintro](https://github.com/suhr/tintro) | | | v4.21.0-rc3 | 2025-06-17 | – | -| 0 | [sullyj3/big_bin_repro_repo](https://github.com/sullyj3/big_bin_repro_repo) | | | v4.10.0 | 2024-08-03 | – | -| 0 | [sweeneyde/1mfld](https://github.com/sweeneyde/1mfld) | Work on classifying 1-manifolds in lean | | v4.25.0 | 2025-11-16 | – | -| 0 | [tage64/lean_subprocess_test](https://github.com/tage64/lean_subprocess_test) | A small programming demonstrating why Lean's subprocess functionality doesn't seem to work very well. | | nightly-2023-04-20 | 2023-11-25 | – | -| 0 | [tangentstorm/fourcolor-lean](https://github.com/tangentstorm/fourcolor-lean) | ai port of four-color theorem from rocq to lean4 | | v4.28.0 | 2026-05-05 | – | -| 0 | [tangentstorm/JacobianChallenge](https://github.com/tangentstorm/JacobianChallenge) | auto-formalizing some old school math | MIT | v4.28.0 | 2026-05-09 | – | -| 0 | [tejoker/BDDM](https://github.com/tejoker/BDDM) | | | v4.29.0-rc7 | 2026-05-05 | – | -| 0 | [thomaskwaring/lattice-path](https://github.com/thomaskwaring/lattice-path) | | | v4.27.0-rc1 | 2026-01-03 | – | -| 0 | [thomaskwaring/learning](https://github.com/thomaskwaring/learning) | | | v4.21.0-rc3 | 2025-07-11 | – | -| 0 | [tim-br/lean-json-parser](https://github.com/tim-br/lean-json-parser) | | | v4.25.2 | 2026-01-05 | – | -| 0 | [TKojar/Regularity_Structures_Lean](https://github.com/TKojar/Regularity_Structures_Lean) | | | v4.22.0-rc4 | 2025-07-28 | – | -| 0 | [tkxue/func_algo](https://github.com/tkxue/func_algo) | | MIT | v4.26.0-rc2 | 2025-12-04 | – | -| 0 | [tomaz1502/cache-get-bug](https://github.com/tomaz1502/cache-get-bug) | | | v4.22.0-rc4 | 2025-08-12 | – | -| 0 | [TonalidadeHidrica/PiTranscendental](https://github.com/TonalidadeHidrica/PiTranscendental) | | MIT | v4.29.1 | 2026-05-06 | – | -| 0 | [toshiro881967-coder/DST-Vault](https://github.com/toshiro881967-coder/DST-Vault) | Axiomatic framework for Dual Sets Theory (DST) and Bio-Resonance in Lean 4 | | v4.30.0-rc2 | 2026-05-08 | – | -| 0 | [ToukoUrsin/oeis-a053819-lean](https://github.com/ToukoUrsin/oeis-a053819-lean) | Formal Lean 4 proof of OEIS A053819 (AI-assisted) | | v4.27.0-rc1 | 2026-01-23 | – | -| 0 | [umpolungfish/odd-perfect-numbers](https://github.com/umpolungfish/odd-perfect-numbers) | machine-verified proofs for euler's theorem and touchard's congruence | | v4.30.0-rc2 | 2026-05-02 | – | -| 0 | [UofSC-Fall-2022-Math-300-H01/homework10](https://github.com/UofSC-Fall-2022-Math-300-H01/homework10) | Proving properties of functions on paper and in Lean | | | 2022-10-25 | – | -| 0 | [UofSC-Fall-2022-Math-300-H01/homework5](https://github.com/UofSC-Fall-2022-Math-300-H01/homework5) | More proofs of propositional formulas in Lean | | stable | 2022-09-20 | – | -| 0 | [UofSC-Spring-2023-SCHC-411-H01/homework03](https://github.com/UofSC-Spring-2023-SCHC-411-H01/homework03) | Predicate logic through relations in Lean | | nightly-2023-01-29 | 2023-02-02 | – | -| 0 | [ValorZard/sdl3-lean-test](https://github.com/ValorZard/sdl3-lean-test) | Testing out SDL3 bindings for Lean4 | MIT | v4.22.0 | 2025-08-28 | – | -| 0 | [ValorZard/Test-Lean-Git-Submodule](https://github.com/ValorZard/Test-Lean-Git-Submodule) | Showcase if Lean 4 uses git submodules | | v4.23.0 | 2025-09-20 | – | -| 0 | [victorliu5296/newton-kantorovich-theorem](https://github.com/victorliu5296/newton-kantorovich-theorem) | Formalization of the Newton-Kantorovich theorem (1 constant version) in Lean 4 | Apache-2.0 | v4.10.0-rc2 | 2024-08-11 | – | -| 0 | [Vierkantor/docgen-tester](https://github.com/Vierkantor/docgen-tester) | Test repo for documentation generation. | | v4.24.0 | 2025-10-16 | – | -| 0 | [Vilin97/forward_euler](https://github.com/Vilin97/forward_euler) | | | v4.28.0-rc1 | 2026-02-27 | – | -| 0 | [vivek-rj/gauss_elim1](https://github.com/vivek-rj/gauss_elim1) | | | v4.8.0-rc1 | 2024-06-09 | – | -| 0 | [vjeranc/fixed-rtrt](https://github.com/vjeranc/fixed-rtrt) | Infinite families and full classification attempt related to TAoCP §7.2.1.6, Ex. 17. | GPL-3.0 | v4.28.0 | 2026-05-06 | – | -| 0 | [vlad902/misc-lean-proofs](https://github.com/vlad902/misc-lean-proofs) | | Apache-2.0 | v4.28.0-rc1 | 2026-02-13 | – | -| 0 | [WalrusGumboot/sorting-trees](https://github.com/WalrusGumboot/sorting-trees) | Lean project for finding optimal sorting trees | | v4.18.0-rc1 | 2025-03-18 | – | -| 0 | [WalrusGumboot/sorting-trees-new](https://github.com/WalrusGumboot/sorting-trees-new) | New attempt | | v4.18.0-rc1 | 2025-03-26 | – | -| 0 | [watersofoblivion/learning-lean](https://github.com/watersofoblivion/learning-lean) | Learning Lean 4 | | v4.2.0 | 2024-01-02 | – | -| 0 | [wechselstrom/cpu_sim](https://github.com/wechselstrom/cpu_sim) | Formal verification of a tiny simulated cpu | Apache-2.0 | v4.13.0-rc2 | 2024-10-04 | – | -| 0 | [wetpant93/pfs](https://github.com/wetpant93/pfs) | | | v4.25.0 | 2026-04-01 | – | -| 0 | [Wolfman56/lean-publish](https://github.com/Wolfman56/lean-publish) | Contributions to awesome Lean project | | v4.30.0-rc1 | 2026-04-07 | – | -| 0 | [wvhulle/heron](https://github.com/wvhulle/heron) | Linter for Lean, the proof assistant and programming language with auto-fixes and refactors. Issues and PRs on Codeberg | | | 2026-05-02 | – | -| 0 | [wwylele/Feuerbach](https://github.com/wwylele/Feuerbach) | | | v4.28.0-rc1 | 2026-01-30 | – | -| 0 | [wwylele/Poncelet](https://github.com/wwylele/Poncelet) | | Apache-2.0 | v4.30.0-rc2 | 2026-04-20 | – | -| 0 | [xaviershay/lean-proofs](https://github.com/xaviershay/lean-proofs) | | | v4.12.0-rc1 | 2024-09-28 | – | -| 0 | [xinhong3/PaxosProofLean](https://github.com/xinhong3/PaxosProofLean) | | Apache-2.0 | v4.22.0-rc3 | 2025-12-01 | – | -| 0 | [yanizhang233/Multi-Neuron-Expressivity](https://github.com/yanizhang233/Multi-Neuron-Expressivity) | | | v4.30.0-rc1 | 2026-04-21 | – | -| 0 | [Youjack/thermodynamics.lean](https://github.com/Youjack/thermodynamics.lean) | | | v4.5.0 | 2024-09-07 | – | -| 0 | [YuvalFilmus/Polymorphisms](https://github.com/YuvalFilmus/Polymorphisms) | | | v4.17.0-rc1 | 2025-04-14 | – | -| 0 | [zblore/csd-lean4](https://github.com/zblore/csd-lean4) | Lean4 formalisation of Constraint-Surface Dynamics, beginning with LF1: volume typicality and frequency convergence for… | Apache-2.0 | v4.29.0-rc8 | 2026-04-23 | – | -| 0 | [zeekmartin/topostability-lean4](https://github.com/zeekmartin/topostability-lean4) | Lean 4 formalization of Topostability framework - Papers 11-14 | | v4.30.0-rc2 | 2026-04-19 | – | -| 0 | [zeramorphic/lambda_calculi](https://github.com/zeramorphic/lambda_calculi) | | | v4.3.0-rc2 | 2023-11-20 | – | -| 0 | [zqy1018/compilation-vs-evalExpr](https://github.com/zqy1018/compilation-vs-evalExpr) | | | leanprover/lean4-nightly:nightly-2025-12-28 | 2026-01-03 | – | diff --git a/python/lean_pool/aggregator/__main__.py b/python/lean_pool/aggregator/__main__.py index 562bb84700..da41d4a211 100644 --- a/python/lean_pool/aggregator/__main__.py +++ b/python/lean_pool/aggregator/__main__.py @@ -183,6 +183,17 @@ def clone( "directory to leave that column blank." ), ) +@click.option( + "--min-stars", + type=int, + default=2, + show_default=True, + help=( + "Drop rows with fewer stars than this from the rendered table. " + "Underlying data files keep every package; this only affects " + "the markdown table size so GitHub keeps rendering it." + ), +) @click.option( "--readme", "readme_path", @@ -195,6 +206,7 @@ def render( manifest_path: Path, manual_data_path: Path, clones_dir: Path, + min_stars: int, readme_path: Path, ) -> None: """Render the candidates README table from a manifest.""" @@ -203,12 +215,19 @@ def render( manual_packages = load_manual_packages(manual_data_path) combined = {**manifest, "packages": list(manifest["packages"]) + manual_packages} effective_clones_dir = clones_dir if clones_dir.exists() else None - table = render_table(combined, clones_dir=effective_clones_dir) + table = render_table( + combined, + clones_dir=effective_clones_dir, + min_stars=min_stars, + ) update_readme(readme_path, table) + rendered_rows = sum(1 for line in table.splitlines() if line.startswith("| ")) + # Subtract the two header lines from the count. + rendered_rows = max(0, rendered_rows - 2) click.echo( - f"Rendered {len(combined['packages'])} packages " - f"({len(manifest['packages'])} reservoir + {len(manual_packages)} manual) " - f"into {readme_path}" + f"Rendered {rendered_rows} of {len(combined['packages'])} packages " + f"({len(manifest['packages'])} reservoir + {len(manual_packages)} manual; " + f"min-stars={min_stars}) into {readme_path}" ) diff --git a/python/lean_pool/aggregator/render.py b/python/lean_pool/aggregator/render.py index 7c4af889b1..d4ce5d5873 100644 --- a/python/lean_pool/aggregator/render.py +++ b/python/lean_pool/aggregator/render.py @@ -183,13 +183,18 @@ def _row(package: Package, toolchain: str | None) -> str: ) -def render_table(manifest: ReservoirManifest, clones_dir: Path | None = None) -> str: +def render_table( + manifest: ReservoirManifest, + clones_dir: Path | None = None, + min_stars: int = 0, +) -> str: """Render the manifest as a markdown table. 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. + optionally filtered by ``min_stars``, then sorted by star count + descending with ``fullName`` tiebreak. Args: manifest: The full Reservoir manifest with packages in priority @@ -198,10 +203,15 @@ def render_table(manifest: ReservoirManifest, clones_dir: Path | None = None) -> (produced by ``lean_pool.aggregator clone``). When present, each row's Lean column is read from the repo's ``lean-toolchain`` file; otherwise that column is blank. + min_stars: Drop rows with strictly fewer stars than this from + the rendered output. Used to keep the table small enough + for GitHub to render — the underlying data files still + contain every package, this only affects the markdown + table. Returns: A markdown table including header, separator, and one row per - unique package. + unique package that meets the threshold. """ seen: set[str] = set() deduped: list[Package] = [] @@ -215,6 +225,9 @@ def render_table(manifest: ReservoirManifest, clones_dir: Path | None = None) -> seen.add(key) deduped.append(package) + if min_stars > 0: + deduped = [p for p in deduped if (p.get("stars") or 0) >= min_stars] + packages = sorted( deduped, key=lambda p: (-p.get("stars", 0), p["fullName"].lower()), diff --git a/python/tests/aggregator/test_render.py b/python/tests/aggregator/test_render.py index ef0e2a67fd..9b435a7154 100644 --- a/python/tests/aggregator/test_render.py +++ b/python/tests/aggregator/test_render.py @@ -314,6 +314,43 @@ def test_render_table_fills_lean_column_from_clones_dir(tmp_path: Path) -> None: assert " v4.30.0 " in package_row +def test_render_table_filters_below_min_stars() -> None: + """``min_stars`` excludes low-star rows so GitHub still renders the table.""" + manifest = _manifest( + [ + _package(full_name="alpha/big", stars=42), + _package(full_name="beta/edge", stars=2), + _package(full_name="gamma/one", stars=1), + _package(full_name="delta/zero", stars=0), + ] + ) + + table = render_table(manifest, min_stars=2) + + body_lines = [line for line in table.splitlines() if line.startswith("| ")][2:] + package_cells = [line.split("|")[2] for line in body_lines] + rendered = " ".join(package_cells) + assert "alpha/big" in rendered + assert "beta/edge" in rendered + assert "gamma/one" not in rendered + assert "delta/zero" not in rendered + + +def test_render_table_min_stars_zero_keeps_everything() -> None: + """``min_stars=0`` is a no-op so existing callers keep current behaviour.""" + manifest = _manifest( + [ + _package(full_name="alpha/some", stars=3), + _package(full_name="beta/zero", stars=0), + ] + ) + + table = render_table(manifest, min_stars=0) + + assert "alpha/some" in table + assert "beta/zero" in table + + def test_render_table_lean_column_blank_without_clone(tmp_path: Path) -> None: """Repos without a local clone show an empty Lean cell, not an error.""" package = _package(stars=1)