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.
Podden och tillhörande omslagsbild på den här sidan tillhör
Aaron Stump. Innehållet i podden är skapat av Aaron Stump och inte av,
eller tillsammans med, Poddtoppen.
