Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Iowa Type Theory Commute
Autoformalization of Fermat's Last Theorem
•
Aaron Stump
•
Season 8
•
Episode 1
Use Left/Right to seek, Home/End to jump to start or end. Hold shift to jump forward or backward.
In this episode, I reflect on the recent announcement that Anthropic researchers have autoformalized the proof of Fermat's Last Theorem. That is, they instructed an LLM to create a computer-checkable proof, in the Lean prover, of this theorem, following existing paper proofs in the literature. The resulting proof weighs in at 13 million lines of Lean, a staggering amount.