Agentic AI news, research notes, and industry analysis.
Tag
6 stories in this tag.
Thomas Hales writes on Tao's blog about Lean's reliability under AI-generated proof loads, describing a "Summer of Soundness Bugs" where AI security tools found kernel flaws that let fabricated proofs slip through — including an accepted Lean disproof of the Collatz conjecture. As AI writes more formal proofs at scale, the correctness of the verification infrastructure matters more than ever, and that infrastructure is itself imperfect.
Read more →OpenAI posted 372 AI-generated math proofs to GitHub — Lean-checked and likely correct, covering problems from the 4D Kakeya conjecture to progress on the Riemann hypothesis. Terence Tao says this marks the end of "Math 1.0" and calls for a rethinking of what mathematics is for in the age of AI.
Read more →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 →Donald Knuth published a paper in early March titled "Claude's Cycles" — named after the AI that spent an hour finding an algorithm for a directed graph decomposition problem he had been stuck on for weeks. Knuth wrote the formal proof himself; Claude did the search. Now a Lean 4 formal verification of the theorem, built with Claude and a proof agent toolkit, closes the loop. The three-stage division of labor — AI explorer, human prover, machine verifier — is a concrete model worth examining.
Read more →