formal verification

Axiom Math announced on October 27, 2026 that it is releasing what it calls the first complete computer-checked proof of the Classification of Finite Simple Groups (CFSG). According to the company, swarms of dozens of AI agents wrote approximately 43.1 million lines of Lean code over 24 days.

Anthropic published research on October 22, 2026, reporting that Claude produced machine-checked formal proofs of security properties at the RISC-V assembly level. The proofs cover 239 fuzz-test entry points across 123 open-source libraries, in a collaboration with Theorem.

Google DeepMind's AlphaProof Nexus solved nine of 353 open Erdős problems and proved 44 OEIS conjectures, according to a study published in Science. The system pairs Gemini 3.1 Pro with the Lean proof assistant, and the work went through peer review, unlike other recent AI-math releases.

OpenAI released 719 manuscripts claiming solutions to open math problems, but only 10 include the model's chain of thought. A Cambridge and King's College London paper also documents at least two discrepancies between the natural-language and Lean versions of OpenAI's Navier-Stokes-derived result.

OpenAI has published 372 mathematical results generated by an unnamed internal frontier model, hosted on GitHub instead of in peer-reviewed journals. The company claims each result solves or substantially advances an open problem, at an average of about three hours of ChatGPT Pro Thinking compute per result. Many include Lean formalizations, but independent validation of significance is still pending.

Axiom Math's AI system AxiomProver has formally verified the proof of the '246 theorem,' a landmark result from the Polymath8b collaboration on prime gaps. The company says the achievement builds a reusable library for future formalization work and points toward AI verification of software code.

Mistral AI released Leanstral 1.5, a free Apache-2.0 licensed model with 119B total parameters and 6B active parameters specialized for formal verification in Lean 4. The model achieves 100% on miniF2F benchmark, solves 587 of 672 PutnamBench problems at $4 per problem (versus $300+ for competitors), and reaches state-of-the-art 87% on FATE-H and 34% on FATE-X benchmarks.

AWS has released Automated Reasoning checks in Amazon Bedrock Guardrails, a feature that uses formal mathematical verification to validate AI outputs against defined rules. Unlike LLM-as-a-judge approaches that use one probabilistic model to validate another, Automated Reasoning provides mathematically proven, auditable compliance evidence for regulated industries.