6 verified stories covering Formal Verification, product updates and industry developments.
Axiom says its AxiomProver agent swarm produced the first complete machine-checked proof of the classification of finite simple groups in Lean in 24 days, with 34 mathematical discrepancies found along the way.
Anthropic's Frontier Red Team used Claude to prove 239 entry points across 123 open-source libraries will not crash on inputs under 64 MB, with proofs landing on compiled RISC-V binaries.
Anthropic released an Apache 2.0, machine-checked Lean 4 proof of Fermat's Last Theorem built on Mathlib, spanning 60,475 modules and verified by three independent kernels.
Berkeley's new Vero benchmark has AI agents write code and formal proofs together across whole repositories — even the best model fully solves only 27 of 43 projects.
OpenBMB open-sourced MathForm-8B, an 8B model for autoformalizing math into Lean 4, plus a 367,000-sample verified dataset and evaluation code, outperforming several 32B formalization models.
OpenAI used Astra's first public research signal to release ten math and theoretical computer science results, with a 249-page paper, Lean certificates and reasoning walkthroughs.