Applied Case: The Proof Was 166 Pages Long

After Chair44, Proof-to-Theory needed a worse problem.

Applied Case: The Mathematician Still Has a Job

Proof-to-Theory ran blind on Chair44. It found the engine. Chaim Goodman-Strauss found the three colors.

Modal Path EthicsAidan Lawson

Chair44 had been ideal for a first external calibration. There was a large proof package. Proof-to-Theory recovered the engine. Chaim Goodman-Strauss later supplied the small human representation the machine had correctly identified as missing.

Suspiciously tidy.

So the next target was OpenAI's Navier–Stokes submission.

One hundred sixty-six pages.

A large Lean repository.

A Millennium Prize problem in the blast radius.

A theorem whose public shorthand can become wrong in about six words.

Perfect.

The first job was therefore to establish what the hell the proof was even claiming.

What The Hell The Source Actually Claims.

The OpenAI paper does not claim a zero-force Navier–Stokes blowup.

It does not claim that every initial condition blows up.

It does not claim one universal forcing term works for every viscosity.

It does not turn viscosity off and infer Euler.

It does not show that global weak solutions disappear.

The source claims the following.

For every viscosity ν > 0, there exists a smooth force f, compactly supported in space and positive time, and a smooth solution u,p on R³ up to time 1 with zero initial velocity.

Before time 1, u and p stay inside one fixed compact spatial region. The kinetic energy remains uniformly bounded.

The speed does not. As t approaches 1, the L∞ norm of u becomes unbounded.

The force remains smooth.

That last sentence is one of the reasons the proof is hard.

If the forcing term were allowed to become singular at the same time as the velocity, a large part of the terminal regularity problem would disappear. The source instead has to arrange a violent presingular flow whose exact Navier–Stokes residual extends as a smooth compactly supported force through the singular time.

The paper also claims that there is no global-in-time smooth solution with the same force, the same zero initial datum, and uniformly bounded whole-space kinetic energy. It is not enough to show that the constructed compactly supported flow cannot continue in the same compact set. A competing global solution is allowed to spread out.

Then the paper carries the result to a periodic three-torus version.

This is aimed at the forced breakdown alternatives (C) and (D) in the Clay Mathematics Institute's official Navier–Stokes problem statement.

That is different from the unforced universal-regularity problem most people picture when they hear "solve Navier–Stokes."

Proof-to-Theory began there.

What exact theorem is on the table, and which parts of the construction are carrying it?

PTT-042.

PTT-042 was prospective.

The worker received only three source objects:

1. OpenAI's 166-page paper.
2. The exact pinned OpenAI NavierStokesAndEuler repository.
3. The Clay Mathematics Institute's official problem statement.

No later commentary.

No forum explanations.

No secondary walkthrough.

No human simplification supplied as an answer key.

The run froze before comparison.

Candidate SHA-256:

9a5d4220f22ad535f5e1528bd01cef89f8bf446549191f517d20ef724073a203

The source-bound verdict was deliberately conservative:

THEOREM / SCOPE: PASS

DEPENDENCY RECONSTRUCTION: PARTIAL

HUMAN MECHANISM: PARTIAL

REPRESENTATION COMPRESSION: PARTIAL

SOURCE / FORMAL ALIGNMENT: PARTIAL

INTERVENTIONS: PARTIAL

That is exactly what should happen when a source already contains a serious explanation and PTT has not earned a simpler one.

The source had already done substantial theoretical work.

Proof-to-Theory's job was to stop that work from collapsing back into "a vortex concentrates."

The Residual Must Survive.

The proof is a residual-to-force transfer.

Start with a presingular flow you want.

Then solve the much harder problem of making everything that prevents it from being an exact Navier–Stokes solution become a smooth allowed force instead of an uncontrolled error.

That requires several constraints to hold at once.

• The carrier has to grow fast enough to blow up.
• It has to occupy little enough volume to keep energy finite.
• Its leading tangential residual has to be representable by physical oscillatory waves with positive squared amplitudes.
• The nonlinear errors produced by those waves have to be corrected.
• The pressure has to remain compatible.
• The flow has to stay divergence-free.
• The corrections have to remain localizable.
• The complete residual has to become flat in all Cartesian derivatives near the singular time so the force extends smoothly.
• The final localized solution has to retain the growth path.
• Its full energy has to stay bounded.
• And the uniqueness argument has to compare it against every global smooth finite-energy competitor in the actual whole-space theorem class.

Lose any of those interfaces and you may still have a beautiful violent fluid picture. You no longer have the theorem being claimed.

Four Registers.

Proof-to-Theory compressed the construction into four registers. It did not claim that these four boxes replace the proof. They are the four contracts a reader has to keep alive while moving through it.

G — Growth.

The asymmetric shrinking carrier concentrates toward time 1.

Its radial length is on the order of

(1−t)^(1/2).

Its axial scale is slightly longer.

Its leading velocity grows slightly faster than

(1−t)^(-1/2).

The occupied volume shrinks fast enough that this growth is compatible with bounded energy.

Compatible is the important word.

The scaling check does not itself prove the full energy estimate. The paper has to do that later for the complete corrected flow.

S — Stress.

The background carrier is not an exact solution. Its leading tangential residual is rewritten as the divergence of an annular stress.

That stress then has to lie inside a positive covariance cone generated by two realizable wave families.

Positive because wave amplitudes enter through squares. You cannot ask a squared amplitude to realize an arbitrary signed coefficient.

This is where much of the geometric asymmetry and profile engineering earns its right to exist.

F — Force.

The waves cancel the leading stress only after averaging.

The exact physical equation still contains oscillatory terms, linear terms, quadratic terms, pressure corrections, evaluation errors, cutoff errors, and new mean defects.

So the construction iterates correction cycles. It keeps recomputing the full residual.

The required endpoint is:

every relevant derivative of the exact residual becomes flat enough near time 1 that, after localization, the residual can be declared to be the forcing term and extended smoothly through the singular time.

The theorem allows a prescribed smooth force.

That changes the terminal obligation.

The construction needs a residual with the right smoothness, support, and compatibility properties, not a zero residual.

T — Terminal theorem.

Now the object has to become the theorem.

• Localization is done through potentials before taking curl so incompressibility survives.
• The full localized flow needs a uniform energy bound.
• A whole-space uniqueness argument has to handle an arbitrary smooth same-force competitor with bounded energy, not one conveniently trapped inside the construction's compact support.
• Then viscosity scaling has to preserve the theorem for every ν > 0.
• The periodic version has to shrink the spatial support into a fundamental cube before periodization so nonlinear cross-terms do not appear between overlapping copies.

Finally, the exact solution classes have to line up with Clay alternatives (C) and (D).

• G.
• S.
• F.
• T.
  • Growth.
  • Stress.
  • Force.
  • Terminal closure.

The Five Radial Equations Are Still There, Still Waiting.

This is where the scoreboard stays honest.

The paper itself already contains a detailed proof outline, diagrams, stress equations, correction cycles, and the physical story.

Proof-to-Theory did not discover a hidden one-page proof anywhere in there. It reorganized the source around theorem-facing obligations.

The hard analytical bridges did not evaporate.

A strong PDE analyst still needs to understand

• why the asymmetric carrier gives the required positive stress cone across the whole annulus.
• Why the specific radial moments are the correct obstructions.
• How shear amplification and viscous damping coexist in the two wave families.
• Why each correction cycle gains enough regularity despite derivative losses.
• Why the complete locally finite sum is flat in every Cartesian jet needed by the force extension.
• Why the full corrected localized field has uniformly bounded energy.
• Why the whole-space uniqueness estimate works against an unbounded-support finite-energy competitor.
  • And then somebody still has to compile the pinned Lean repository and inspect the actual declaration dependencies instead of taking metadata as a sacrament.

Proof-to-Theory called that representation debt.

A four-box diagram is useful when it tells you which hard questions belong in which box. It becomes bullshit when it pretends the boxes answered them.

Break It.

A useful explanation should predict how the construction fails.

PTT-042 produced several interventions.

Remove one of the two wave families while keeping a generic target stress.

The stress representation fails in general because one positive covariance ray cannot span the two tangential components the construction needs.

Delete the zero radial moments.

The radial anti-derivative stress leaks outside the annulus and the exterior matching breaks.

Stop after finitely many correction cycles and define the force from that residual.

The force is no longer certified smooth through time 1 at all derivative orders.

Keep only averaged wave cancellation and ignore the evaluation, curl, and nonlinear correction terms.

You have an averaged story instead of an exact Navier–Stokes equation.

Multiply the velocity directly by a spatial cutoff.

Incompressibility generally breaks because the cutoff contributes a divergence term.

Periodize before shrinking supports into disjoint fundamental cells.

The nonlinear term creates cross-interactions between translated copies.

Drop the bounded-energy condition on the competitor class.

The source's whole-space uniqueness argument no longer automatically applies.

Those are good interventions because they attack specific interfaces.

They show the proof is not one long incantation.

Different components are protecting different theorem clauses.

The Machine Still Did Not "Understand Navier–Stokes".

The frozen result says

HUMAN MECHANISM: PARTIAL

and

REPRESENTATION COMPRESSION: PARTIAL.

As it should. The paper itself had already explained much of the architecture.

Proof-to-Theory's contribution here was a theorem map, a dependency map, a cleaner separation between construction machinery and proof engine, a set of scope guards, and a list of places where a human explanation still has to earn its simplification.

That is enough for this benchmark.

PTT-041 asked:

Can the machine recover the engine of a proof and recognize when the human representation is still missing?

PTT-042 asks something harder:

Can the machine enter a frontier proof before the community has settled on the preferred explanation and produce a source-bound map useful enough to interrogate later?

That is why this one is prospective.

There is no Goodman-Strauss answer key waiting five days later in the protocol here. Just a frozen object. Later explanations can beat it, later audits can contradict it, and later formal checks can expose a bad bridge.

The Exact Wrong Question.

The public question around machine mathematics keeps arriving in one form:

Did the AI solve the problem?

Sometimes that question matters. It is still too coarse to govern the handoff.

• A proof can be correct and badly understood.
• A proof can be wrong in one bridge while the mechanism around it remains valuable.
• A formalization can verify exactly the proposition written while the human field still has to determine whether the proposition captures the intended theorem.
• A source can contain a very good explanation that gets buried under the size of its own verification machinery.
• A machine can reconstruct the dependency graph and still fail to invent the representation people ultimately prefer.

Those are different outcomes. Proof-to-Theory is being built to keep them different.

The Navier–Stokes benchmark is useful because the distinction becomes impossible to avoid.

• The source claim is enormous.
• The proof apparatus is enormous.
• The human question cannot be reduced to a green check.
  • You need to know what the green check is attached to,
  • which bridge is carrying the force,
  • which bridge is carrying bounded energy,
  • which bridge turns local blowup into global nonexistence,
  • which parts are source explanation and which parts are new compression,
  • And when the machine has not earned a simpler representation.

PTT Continues.

The PTT-042 candidate is frozen. The exact bytes remain the benchmark object. Later human work gets compared against it.

If somebody produces a short conceptual account of the five radial obstructions, the stress cone, or the all-jet force extension, that does not embarrass the benchmark. That is the event the benchmark is waiting for.

If independent checking finds a mathematical failure in the source, the frozen map should show which dependencies survive and which ones fall with it.

That is also useful.

Proof-to-Theory does not need to be the final mathematician in the room. It just needs to leave the room in a better state than it found it.

FINITE TIME BLOWUP FOR NAVIER–STOKES, From Proof to Theory.

Sources.

1. OpenAI, “Finite time blowup for Navier–Stokes,” 2026.

https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf

2. OpenAI, NavierStokesAndEuler repository, PTT-042 pinned commit:

f9e8bc5b38b6e212696e8a30e3e91517af887bbd

https://github.com/openai/NavierStokesAndEuler

3. Charles L. Fefferman, “Existence and Smoothness of the Navier–Stokes Equation,” Clay Mathematics Institute problem statement.

https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf

PTT-042 frozen candidate SHA-256:

9a5d4220f22ad535f5e1528bd01cef89f8bf446549191f517d20ef724073a203

Status note. This article reports the theorem claimed by the OpenAI paper, the pinned formal source declarations, and the frozen PTT-042 source-bound reconstruction. PTT-042 did not independently verify the 166-page proof, compile the full Lean dependency chain, or establish an external peer-review verdict.

Provenance note. The PTT-042 candidate froze with the correct bytes and hash, but Console v0.2.0 wrote the file under the stale filename PTT041_CANDIDATE.md. The bytes were preserved, the incident was recorded, and the benchmark was not rerun.