On September 4, 2026, Anthropic published a complete Lean 4 proof of Fermat's Last Theorem: 13 million lines, written largely by Claude agents in 11 days, and checked by a machine rather than by referees. The mathematician who has led the human effort to do the same thing since 2024 confirmed that it checks out, and then wrote that it tells us "essentially nothing" about mathematics. Both are true, and the gap between them is the interesting part for anyone who writes software that has to be cor...