Topic · 5 stories
5 stories tagged formal-verification on AI Tamer, newest first.
Axiom Math released a sorry-free Lean proof of the classification of finite simple groups, built by agent swarms, and says it found 34 notable deviations.
Xiangpeng Hao says LLMs wrote all of bbtree while he steers and answers for it. Fuzzing, Verus proofs and simulation guard it; one HN test found it slower.
Anthropic's red team and Theorem used Claude to write Rocq proofs for 123 open-source libraries. The proofs carry real assumptions and cost many tokens.
doubleAI's Maxwell optimizes programs while they run and says it formally proves each rewrite equivalent. It launched with a $200M Series A disclosure.
A 17 October guest post on Terence Tao's blog proposes a math journal that requires proofs formally verified in Lean, citing errors in LLM-assisted proofs.
