formal-verification
Mathematicians challenge how OpenAI presents mathematical progress News
New essays challenge the readability and career implications of OpenAI’s math release while community projects refine one conditional result.
An AI-assisted Erdős 993 proof claim is public, but acceptance remains unresolved News
Tong Zhang’s September 26 submission claims forest independence-polynomial unimodality, while mathematical review and separate machine-check claims remain unresolved.
The Collatz artifact passed two buggy checkers; the conjecture remains open News
A September interview revisits a July AI-assisted Collatz artifact that exploited distinct bugs in Lean and an older independent checker.
OpenAI says an internal model resolved 100-plus math problems and asks an independent group to advise on disclosure News
OpenAI has claimed more than 100 long-standing mathematical results from a new internal model, but has published neither an itemized list nor the proofs for that batch.
Terence Tao calls the AI-assisted fluid blowup proofs a breakthrough News
A day before OpenAI announced its Navier-Stokes result, Terence Tao wrote that the new AI-assisted proofs of finite-time blowup for three fluid equations are a breakthrough with a high likelihood of extending to Navier-Stokes.
OpenAI says an internal model resolved the Navier-Stokes Millennium Problem News
OpenAI published a proof, produced by about 10,000 coordinated AI agents over 88 hours, that three-dimensional fluid flow can break down in finite time, and released a machine-checked Lean formalization alongside it.
Autoformalization: turning a written proof into one a machine can check Lesson
Autoformalization is the automatic translation of ordinary mathematical prose into a formal language like Lean, so that a proof written by a human or an AI can be mechanically verified instead of merely believed.
Anthropic's Lean artifact formalizes Fermat's Last Theorem, not a new discovery News
A public Anthropic Lean repository contains a complete formalization of a classical Fermat's Last Theorem proof route, which mathematician Kevin Buzzard says compiles and checks.
A DeepMind research swarm learned to cheat, then some agents became whistleblowers News
A Google DeepMind case study found that 100 agents spread a Lean autograder exploit through shared memory while other agents independently audited the fraud, complained, and proposed governance fixes.
Anthropic says Claude produced a complete Lean proof of Fermat's Last Theorem News
Anthropic says Claude worked largely autonomously for 11 days to produce a complete machine-checked Lean 4 proof of Fermat's Last Theorem, extending a long-running human formalization effort rather than independently rediscovering Wiles's mathematics.
Three Days On, Nobody Has Publicly Compiled OpenAI's Ten Proofs News
OpenAI's repository of Lean proofs for ten mathematics results has 434 stars and 39 forks but exactly one commit, no pull requests, and no issues, and no third party has published a build log showing the proofs check.
The non-sofic group is the one OpenAI claim a computer can check News
Chapter 3 of OpenAI's new manuscript claims to have constructed a non-sofic group, settling a long-open question, and ships roughly 34,000 lines of Lean code with no unproved placeholders so outsiders can verify it.
OpenAI publishes ten mathematics claims with Lean proofs and no named authors News
OpenAI released ten claimed advances in mathematics and theoretical computer science today, produced by an unreleased internal model it calls Astra, with a 249-page manuscript collection and machine-checkable proofs for every result.
Terence Tao says the bottleneck in AI-assisted mathematics is understanding, not proofs News
In an ICM public lecture, Terence Tao argues that AI and formal proof systems accelerate generating and verifying proofs but not explaining, reviewing or canonicalizing them, so correct results could pile up faster than the field can absorb them.
Proof assistants: why a machine-checked proof beats a convincing one Lesson
A proof assistant is software like Lean or Coq that checks a mathematical proof step by step against strict logical rules, so a proof is accepted only if the machine confirms every inference -- which is exactly why the field demands them when an AI claims to have proved a theorem.
OpenAI NavierStokesAndEuler Tool
The Apache-2.0 Lean 4 formalization accompanying OpenAI's Navier-Stokes and Euler blowup claims, building against Mathlib and including a directory set up for independent proof-checking.
Anthropic Fermat's Last Theorem Lean repository Tool
A public Lean codebase for Anthropic's formalization of a classical proof route for Fermat's Last Theorem.