Projects

Formalizes Maynard's multidimensional sieve and the part of Polymath8b that brings the bound to $246$, on top of Mathlib and Kontorovich and Tao's PrimeNumberTheoremAnd. The Lean code is released as PrimeGapsLib.

Every finite simple group is cyclic of prime order, alternating, of Lie type, or one of the 26 sporadic groups. The original proof runs to some 15,000 journal pages written over several decades; the formalization is about 43 million lines of Lean, produced over 24 days.

Formalizing the first-generation argument turned up counterexamples to a closure assertion used in a published route to the Unbalanced Group Theorem. That and the other departures from the literature are recorded in the errata.

The Stacks Project is the standard open-source reference on algebraic geometry, a collaboratively written work of some 7,500 pages covering commutative algebra, schemes, cohomology and the theory of algebraic stacks, with every definition, lemma, proposition and theorem carrying a stable four-character tag. The formalization runs to 663,090 Lean declarations across about 15.75 million lines, built on Mathlib, with Lean's kernel checking every completed proof and each tag linked to its Lean code and its dependencies.

The emphasis throughout is on code quality: definitions and statements are written to Mathlib standards and at the generality their consumers need, so that the library is something to build on and to upstream from, rather than a pile of individually verified theorems.

Deligne's theorem is about as deep as algebraic geometry gets, and the étale cohomology it runs on is exactly what the Stacks Project in Lean supplies. All four conjectures — rationality, the functional equation, the Riemann hypothesis and the Betti-number statement — are proved in 213,000 lines of new Lean, following Freitag and Kiehl.

The point is reuse. The library imports 730 modules of the Stacks formalization against 557 of Mathlib, more than half its files depend on Stacks directly, and it cites 283 Stacks tags; Deligne's theorem itself falls out of the Stacks weight bound at Tag 03VH rather than being proved again.

Quality carries over with the code. The library takes the Stacks conventions — the same étale site, the same $\ell$-adic sheaves — pins the same Mathlib commit, and is written to the same standard.