About
Lean Code Over Time
39,684
2
Total Lean lines at the end of each day with Lean-editing activity, from Feb 17, 2026 to May 04, 2026 (54 snapshots).
-
Mar 09, 2026
Theorem 1.1 — Closed graphs characterised by a quadratic Gröbner basis.
The bulk of the work that followed went into Theorem 2.1, which required importing substantial Gröbner-basis infrastructure from a Mathlib pull request.
- Mar 29, 2026 Theorem 3.2 and Corollary 2.2 — Prime decomposition of J_G and radicality.
-
Apr 06, 2026
Section 4 bridge — Conditional independence ideals identified with binomial edge ideals.
Closing Proposition 1.6 then required porting and extending a large amount of Cohen–Macaulay machinery into the project — the costliest infrastructure work of the formalisation.
- Apr 24, 2026 Paper formalization complete — All paper results (Sections 1–4) proved axiom-clean — including Proposition 1.6 (2026-04-22), Corollary 3.4, and the Cohen–Macaulay branch of Corollary 3.7. The decline that follows reflects the fat-proof carving pass that began 2026-05-02.
By The Numbers
67
tracked Lean files
37,832
Lean lines
510
total commits
371
commits in the last 30 days
Lean Code By Directory
| Directory | Files | Lines | Nonblank lines |
|---|---|---|---|
| BEI/ | 38 | 25,815 | 24,207 |
| toMathlib/ | 27 | 10,890 | 9,938 |
| Supplement/ | 1 | 1,102 | 1,037 |
| repo root | 1 | 25 | 25 |
Recent Commit Activity
| Month | Commits |
|---|---|
| Feb 2026 | 12 |
| Mar 2026 | 83 |
| Apr 2026 | 347 |
| May 2026 | 68 |
First commit: 2026-02-17. Latest commit: 2026-05-04.