Axiom formalizes Faltings’ theorem in Lean proof

Axiom has announced the first complete, machine-verified proof of Faltings' theorem using the Lean proof assistant. The formalization follows the Bombieri-Vojta approach to Mordell's conjecture, building on approximately 6.4 million lines of prior formalization from the Stacks Project and adding 110,000 lines of proof-specific code. Open article →