The Lean research ecosystem, in one directory.

Formalization and solution of knights and knaves puzzles in lean 4

Lean 4 linters for LLM-generated proof patterns

Towards a general definition of elliptic curve over schemes

A project to formalize Fisher-Tippett-Gnedenko theorem (default project of course MS-EV0029)

Notes on the Foundations of Lean

CSE 290Q: Topics in Interactive Theorem Provers

「The Lean Language Reference」の日本語訳（作業中）

LPBackend adapter for kim-em/soplex-ffi. Priority 10 (FFI band). The native backend kim-em/soplex defaults to.

Verification of the Wadray library

Verified Results about Gossip protocols in Lean 4

Semi-Thue systems a.k.a. string rewriting systems

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.

Don't disturb my circle!

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

Construction of phi^4_2 quantum field theory in Lean 4

The Seiberg-Witten solution of N=2 SU(2) super-Yang-Mills, formalized in Lean 4: physics as named postulates, machine-checked consequences, audited assumptions