The Lean research ecosystem, in one directory.

Machine-verified proof (0 sorries, 2 axioms) that P ≠ NP via exponential circuit lower bounds for Hamiltonian Cycle. Lean 4 formalization with Mathlib. Proves SIZE(HAM_n) ≥ 2^{Ω(n)} using frontier analysis, switch blocks, cross-pattern mixing, recursive funnel magnification, continuation packets, rooted descent, and signature rigidity.

Formalising the Erdős-Stone-Simonovits theorem and the Kővári–Sós–Turán theorem in Lean

This repo formalizes (possibly) infinite trees of finite degree in Lean. So far this is mainly a dependency for one of my other projects and tailored towards this purpose. The repo features a formalization of (a special case of) König's Lemma.

Lean 4 formalization of strongly continuous semigroups, Hille-Yosida theorem, and BCR Bochner semigroup-to-group extension

Lean4 formalization with Artistotle of the arXiv paper 1906.11174

Lean 4 + Mathlib formalization of the Creative Determinant framework - 15 theorems proved with zero sorry, CI-enforced via lake build --wfail

Formalisation of some facts about event structures and reversibility

Formalisation of forbidden matrix theory