About
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.