Agentic AI news, research notes, and industry analysis.
Tag
3 stories in this tag.
Anthropic released a complete, machine-verified formalization of Fermat's Last Theorem in Lean 4. Claude worked for 11 days and produced 13 million lines of proof code—five times the size of Mathlib—checked independently by three separate verifiers. The interesting story is less "AI does math" and more how multi-agent coordination over a theorem dependency graph made it tractable.
Read more →Terry Tao and the Lean FRO launched Palomar on August 18 — a registry that runs submitted Lean proof repositories through a verification pipeline and publishes the exact formal statement, library dependencies, and reviewer comments. The project is a direct response to the surge in AI-generated Lean proofs, where the bottleneck has shifted from producing proofs to trusting them.
Read more →An AI-assisted "disproof" of the Collatz conjecture turned out to be an adversarial proof object threading through two independent bugs in Lean's type kernel and its external verifier. The hole was patched in an hour, but the Lean creator's warning lands harder than the bug itself: AIs are getting good at finding and exploiting soundness issues in proof checkers, and that's not a one-time event.
Read more →