Faltings’ Theorem Formalized
A curve that gives, and then stops
Notes from the frontier.
Cluster Algebras, Formalized in Lean
Axiom has translated the foundations of a gorgeous and surprising mathematical theory into proofs that a computer can check and researchers can reuse.
The Weil conjectures formalized in Lean
From the work of Grothendieck and Deligne to a reusable formal proof
The Stacks Project, formalized in Lean
A unified library for modern algebraic geometry, built on decades of human scholarship and engineered for the next era of mathematical discovery.
Formalizing the Enormous Theorem
Axiom has formalized in Lean the classification of finite simple groups, the longest proof in the history of mathematics.
Faster Is Not Nearer
Speeding up a polygon's random symmetries never leaves it farther from balance when distance is measured with an even power — nudge the power to 4.001, and some polygon, somewhere, drifts farther.
The Purpose of the Object
A formula was proven before anyone knew what it counted — and the question, once found, had to be asked in order before this paper could answer it.
Cut to the Same Measure
Corrected, the higher Dyson systems meet an object from Jacobi's theory at exactly the same elliptic law — and the correction is finite enough to write down in full.
The Weight Comes Last
The leading terms cancel modulo q, and the degree left behind is settled by whether an addition in base q carries — the reduction Evan Chen and Ken Ono use to prove Thakur's three hypotheses, open since 2009.
The Address Before the Room
One family is a third the size of the other — but that third is a doorway, not the matching that has to be built behind it.
The Same Ground
In the right coordinate, Kaprekar's process is not a different puzzle in every base — it is one operation: doubling.
The Figure and the Remainder
A multiplicity that reads as the blur of cancellation comes into focus, in natural families, as an exact count of bounded Dyck-path structures.
