State of Proof

AI × math × what comes next

AI is doing math. Let’s see what holds up.

We examine mathematical claims, replay specific proof steps, and publish what remains unresolved.

See the newest papers See active examinations

A public research initiative of Material Shift.

Paper Watch

Big claims. A closer look.

Intake is not validation. These primary-source records are unexamined unless a separate proof docket records completed work.

Candidate · added · paper-2026-09-08-finite-time-blowup-for-navier-stokes

Schematic of inward-spiralling fluid filaments, a narrowing core, and axial outflow above and below the central plane.
Source-informed schematic · not simulation data

Navier–Stokes: can fluid equations hit a breaking point?

What it is
The paper reports a proof that smooth, forced three-dimensional Navier–Stokes flow can break down in finite time.
Who did it
OpenAI
What it could mean
Weather forecasts. Aircraft wings. Blood flow. Fluid equations underpin all three. This claim could expose a breaking point in forced, three-dimensional Navier–Stokes—even when the fluid starts perfectly still.

Examination not started

See the check plan

Evidence & validation

From announcement to evidence

Discovery recorded. State of Proof has not yet examined this claim.

  1. Read the original work
    Finite Time Blowup for Navier–Stokes ↗

    OpenAI.

  2. See the proposed checks

    Map the exact paper and Lean endpoints to Clay alternatives C and D, including force regularity, initial data, energy and periodic pressure; then perform an isolated formal replay with pinned external checker tools.

  3. No proof docket yet

    A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.

    Explore existing proof dockets →
How validation works →

Inside the proposed vortex

Forced Navier–Stokes · three dimensions

∂ₜu + (u · ∇)u − νΔu + ∇p = f; ∇ · u = 0

Fluid moves inward around the axis and escapes along it. In the paper’s proposed construction, the active core becomes narrower as its speed grows. The drawing illustrates that mechanism; it is not a computed solution.

Read the source · Equation (1.1), section 2.1 and figure 1 ↗
What it claims
OpenAI claims a finite-time breakdown of smooth, forced, three-dimensional incompressible Navier–Stokes flow from rest with bounded energy, asserting alternatives C and D of the Clay problem. This is the publisher's claim, not a State of Proof validation.
Why this could matter
Navier–Stokes: can fluid equations hit a breaking point? Wings, weather and blood flow all involve fluid equations. OpenAI claims that even smooth inputs can drive one idealized model beyond smooth behavior. This concerns the model's limits—not instantly better aircraft or forecasts.
If it holds up
It would resolve the forced breakdown alternatives of the Clay problem and sharpen research into when smooth fluid models stop applying.
If it does not
A gap would identify which assumption or proof step needs repair; ordinary engineering uses would not automatically become invalid.
Impact horizon
Foundational · Fluid models · Mathematical physics · AI-assisted proof
Version
Public manuscript retrieved 2026-09-08; PDF SHA-256 0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f. Discovery date is not a claim of first publication.
Why we tracked it
The September 8 fluid-mathematics announcements warrant distinct intake records for each equation, forcing assumption and proof-completion state.
Highest-risk dependency
Whether the formal statement matches the complete manuscript and official Clay assumptions remains unassessed. Formal replay and expert review have not been performed by State of Proof.
Available artifacts
A public formal-source repository is linked: https://github.com/openai/NavierStokesAndEuler/tree/8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538. OpenAI attributes the work to an internal AI-agent system. No manuscript-linked code was executed; source availability is not proof verification.
Current boundary
Intake record only; examination not started.

Docket-ready · added · paper-2026-09-04-formalizing-fermat-s-last-theorem

Schematic proof dependencies: blue lemma tiles connected through intermediate steps to one amber theorem tile.
Illustration · proof dependencies

A landmark proof becomes software machines can check

What it is
A reported Lean formalization turns the known proof of Fermat’s Last Theorem into steps a computer can check.
Who did it
Anthropic’s Claude agents, with research led by Tianyi Peng
What it could mean
Fermat is already proved. Imagine giving that proof a ‘verify’ button. If this scales, AI-assisted mathematics could arrive with independently checkable logic—catching errors before other research builds on them.

Examination not started

See the check plan

Evidence & validation

From announcement to evidence

Discovery recorded. State of Proof has not yet examined this claim.

  1. Read the original work
    Formalizing Fermat's Last Theorem ↗

    Anthropic; named research lead Tianyi Peng; Lean sources produced by Claude agents.

  2. See the proposed checks

    In an isolated high-memory environment, clone the exact source commit; verify source hashes and provenance; run the default lake build; run verification/comparator/run.sh against the Mathlib-only challenge; run verification/nanoda/run.sh; inspect the four nanoda performance patches; and have a formal-methods reviewer map PROOF-PATH.md and the encoded theorem to the intended Frey–Serre–Ribet–Wiles/Taylor-Wiles argument.

  3. No proof docket yet

    A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.

    Explore existing proof dockets →
How validation works →

How a long proof becomes checkable

Fermat’s Last Theorem

aⁿ + bⁿ ≠ cⁿ for positive integers a, b, c and integer n > 2

Each tile stands for a mathematical statement; the connections show which earlier statements it depends on. The announcement describes a dependency graph used to organize a Lean formalization of Fermat’s Last Theorem. This illustration explains that structure; it is not the project’s actual proof graph.

Read the source · Formalizing Fermat’s Last Theorem · Prove2Me dependency graph ↗
What it claims
Anthropic reports that Claude agents produced in eleven days the first complete end-to-end, computer-checked Lean proof of Fermat's Last Theorem. This is not a new solution to an open problem—Wiles and Taylor-Wiles proved the theorem in 1995—but a claim that their known mathematical route has been rebuilt as a fully machine-checkable formal artifact at unprecedented scale and speed.
Why this could matter
A landmark proof becomes software machines can check Fermat's Last Theorem was solved in 1995. The new achievement is different: turning that enormous human proof into code independent computers can replay. If this scales, AI-generated mathematics can arrive with a checkable receipt—helping researchers find errors and spend time understanding the truth.
If it holds up
A reproducible end-to-end Lean proof would show that AI can help turn landmark mathematics into independently checkable software, making formal verification a practical companion to human peer review as mathematical output accelerates.
If it does not
Fermat's theorem remains proved, but this artifact would not yet demonstrate a reliable new route for machine-checking large AI-assisted proofs; the verification workflow would need repair.
Impact horizon
Methods · Formal verification · AI mathematics · Research infrastructure
Version
Anthropic research announcement, published 2026-09-04; public proof repository pinned at unsigned commit aa2d8b34692b16c70f699536de0d8e75b9a3e9ef, authored 2026-09-03
Why we tracked it
Anthropic's complete Lean 4 formalization claim is pinned to a public source commit with three concrete replay routes; it remains source-locked and independently unvalidated by State of Proof, and no docket has been created.
Highest-risk dependency
The evidence is author-supplied and the repository's formalization.yaml labels review status self-assessed with no listed reviewers. Full replay is resource-heavy—the published route reports hundreds of gigabytes of working storage and up to roughly 300 GB of memory—and machine checking establishes formal inference, not by itself the semantic faithfulness of every named intermediate result or generated explanation.
Available artifacts
The pinned Apache-2.0 repository contains roughly 13 million lines of Lean, 29,511 theorem/proof modules, FinalCheck.lean, a human-readable PROOF-PATH.md, metadata declaring zero sorry terms and exactly Lean's three standard axioms, a Lean Comparator challenge, and an independent nanoda-kernel replay route. Lean 4.33.1 and Mathlib commit db584cd6d46c92f209a44c0f1c829460d327499d are pinned. The artifact builds on and attributes work from the Imperial College London FLT project, flt-regular, and Mathlib.
Current boundary
Intake record only; examination not started.

Candidate · added · paper-2026-09-08-finite-time-blowup-for-the-euler-equation

Three schematic stages showing localized blue oscillations at progressively finer scales within a background flow.
Source-informed schematic · not simulation data

Can an ideal fluid break down without an outside push?

What it is
The paper claims that smooth, unforced three-dimensional ideal-fluid flow can develop a finite-time breakdown.
Who did it
OpenAI
What it could mean
Even a frictionless, unforced fluid model could tie its own mathematics in knots. A verified result would show smooth motion breaking down without an outside shove.

Examination not started

See the check plan

Evidence & validation

From announcement to evidence

Discovery recorded. State of Proof has not yet examined this claim.

  1. Read the original work
    Finite Time Blowup for the Euler Equation ↗

    OpenAI.

  2. See the proposed checks

    Does the formal endpoint establish the same smooth-data, whole-space, unforced theorem as the paper?

  3. No proof docket yet

    A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.

    Explore existing proof dockets →
How validation works →

How finer structure is amplified

Unforced Euler · three dimensions

∂ₜu + (u · ∇)u + ∇p = 0; ∇ · u = 0

Each stage adds a localized oscillation to a background flow. In the paper’s construction, one stage helps amplify the next, producing increasingly large gradients. The panels illustrate the idea; they are not computed snapshots.

Read the source · Equation (1.1) and section 2 ↗
What it claims
The paper claims finite-time breakdown for smooth, compactly supported initial flow in the three-dimensional unforced incompressible Euler equations.
Why this could matter
Can an ideal fluid break down without an outside push? Take friction and external pushing out of the picture. Can a smooth ideal flow still develop unbounded gradients? This paper claims it can, probing a fundamental limit of the equations used to understand fluid motion.
If it holds up
It would establish a smooth-data, whole-space breakdown example for unforced Euler, changing the mathematical picture of ideal-fluid regularity.
If it does not
The proposed construction would need repair; the general smooth-data question would not be settled by this argument.
Impact horizon
Foundational · Fluid models · Mathematical physics · AI-assisted proof
Version
Public manuscript retrieved 2026-09-08; PDF SHA-256 a0c234518e6c489e16996805023eb2e75c00b7c03455f7a3a5be2c124954bfdd. Discovery date is not a claim of first publication.
Why we tracked it
The September 8 fluid-mathematics announcements warrant distinct intake records for each equation, forcing assumption and proof-completion state.
Highest-risk dependency
A separate unforced Euler claim, not the forced Navier–Stokes claim. No proof execution or semantic correspondence review by us.
Available artifacts
A public formal-source repository is linked: https://github.com/openai/NavierStokesAndEuler. OpenAI attributes the result to a coordinating AI-agent system and provides a Lean formalization. No manuscript-linked code was executed; source availability is not proof verification.
Current boundary
Intake record only; examination not started.

View all 67 tracked papers →

Active record

A claim with an examination route underway.

Active record · 2026-08-23-alpoge-s6 · Complex geometry

A completed (3,4,∞) modular family gives a compact complex threefold diffeomorphic to S⁶

The manuscript proposes a way to build a compact three-dimensional complex space whose underlying smooth shape is the six-sphere, S⁶. Some finite calculations have been reproduced, but the construction's key geometric and topological steps have not been independently settled.

Source lock · retrieved 2026-08-24 · 283bba10

Recorded result — defined scope

All encoded page-2 matrix identities and the conditional Theorem 7.17 integer/Smith arithmetic were reproduced locally.

Most important open step

Trace the relative meridian signs and toric zero-section independently before reusing the passing group arithmetic

Open the full evidence record →

Queued records

Claims mapped for a future examination.

No headline claim is presented as settled. Statuses apply only to the defined scope.

  1. Queued record · 2026-07-29-maxwell-conjecture · Potential theory

    Five positive point charges in R³ have at least 24 nondegenerate critical points, contradicting the proposed (5−1)² bound

    Source lock
    arXiv v1 · 4178ddc5
    Record state
    Queued record
    Open step
    Independently derive the exact rescaling, Taylor coefficients, and polynomial skeleton before testing the critical-point count
    Changed
    2026-08-27

  2. Queued record · 2026-02-14-openai-first-proof · Proof evaluation

    Ten independent First Proof attempts form a calibration corpus; attempt 2 is the first blinded examination target

    Source lock
    revised packet · 27e97e4f
    Record state
    Queued record
    Open step
    Freeze the blinded attempt-2 working bundle and version-delta record without leaking the known external comparator label
    Changed
    2026-08-27

  3. Queued record · 2025-10-27-nesterov-point-convergence · Optimization

    The stated Nesterov accelerated-gradient iterates converge to a minimizer for every L-smooth convex objective with a minimizer

    Source lock
    arXiv v2 · 31dafeda
    Record state
    Queued record
    Open step
    Independently derive the recurrence equivalence and discrete energy inequality under the exact tₖ hypotheses
    Changed
    2026-08-27

  4. Queued record · 2026-07-10-openai-cycle-double-cover · Graph theory

    Every finite bridgeless undirected graph has a cycle double cover

    Source lock
    PDF + Lean 577e9d9 · b4797f50
    Record state
    Queued record
    Open step
    Map the manuscript's theorem and graph conventions to the pinned Lean endpoint before drawing any inference from a build
    Changed
    2026-08-27

  5. Queued record · 2026-08-01-openai-nonsofic-group · Group theory

    The unit group of the binary Leavitt algebra L_F₂(1,2) is not sofic

    Source lock
    updated 2026-08-06 · ebc561ab
    Record state
    Queued record
    Open step
    Reconcile the substantively revised August 6 prose with the August 2 Lean commit before any formal replay is treated as relevant
    Changed
    2026-08-27

View all dockets →

How to trust the record

Exact sources. Examined steps. Visible uncertainty.

State of Proof preserves what ran, what it establishes, what it does not establish, and how the record changes over time.

  1. Lock the source. Pin the exact paper, version, and hash.
  2. Map the claim. Name the load-bearing steps and dependencies.
  3. Examine specific steps. Record the exact test, derivation, replay, or literature comparison—and its limits.
  4. Keep history visible. Append corrections, responses, and unresolved steps.

Machines can replay calculations and test more proof steps, faster.Experts still decide the questions that require mathematical judgment.

Read the method → · Corrections and conflicts →

Help build the public record

New mathematics is moving fast. The evidence should be able to keep up.

Send a public manuscript and tell us why its central claim matters. An unresolved question is an honest outcome; payment never purchases a favorable conclusion.

Submit a claim Contact the team