Agentic AI news, research notes, and industry analysis.
Tag
3 stories in this tag.
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 →