AI Proved What?

Episode 353, October 2026

Nine, then ten?

Two AI preprints claim affine Bernstein rigidity through dimension nine and a dimension-ten counterexample

Covers result 353 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.

4:15. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:09The claim
  3. 2:09How the proof goes
  4. 3:27Where it stands

The claim, in plain words

The classical Bernstein theorem says that an entire minimal graph over the plane is flat. Its affine cousin replaces area by affine area, which is unchanged by volume-preserving affine maps. A convex graph is affine maximal when it is critical for affine area; then it satisfies a fourth-order equation. Every paraboloid is a solution: our computer checks that quadratic functions give exactly zero, while a slightly perturbed paraboloid does not. The question is whether paraboloids are the only complete solutions.

For surfaces, Chern asked this in the late 1970s, and Calabi asked a version with completeness measured by the affine metric. Trudinger and Wang settled both, in 2000 and 2002; Li and Jia also proved the second by another route. In a 2008 survey they conjectured the answer: only paraboloids up to dimension nine, but a smooth nonquadratic example from dimension ten. They had already found a singular example in dimension ten. Shortly before this release, others wrote that even dimension three was open.

Result 353 is two OpenAI papers, made public October 6, 2026. The first, 23 pages, dated September 24, claims rigidity in dimensions three through nine: a smooth, locally uniformly convex affine maximal graph that is complete for the metric it inherits from Euclidean space is an elliptic paraboloid. It also gives the affine-complete version, using Trudinger and Wang’s earlier work. The second, 7 pages, dated October 5, constructs a smooth entire nonquadratic affine maximal graph in dimension ten.

What it doesn’t claim

Not claimed: anything in dimension eleven or higher, or the first counterexample in dimension ten. Hours after the release, Trudinger and Wang posted a paper with the same ansatz, noting it had been submitted on February 2, and Wang had announced it in a talk in April. Neither OpenAI paper cites their 2008 prediction.

Where it stands

Posted as preprints
OpenAI, 2 papers, dated September 24 and October 5, 2026
Peer reviewed
Not yet
Formalized in Lean
The rigidity theorem in dimensions 3–9 only (docs)

Last checked October 19, 2026. Both papers are unrefereed and unchanged since release. The rigidity theorem in dimensions three to nine is formalized in Lean, about 40,000 lines, not run by us; three outside projects re-ran it successfully, and the Lean proves the interior-estimate step its own way instead of assuming it. The affine-complete version and the dimension-ten example have no Lean. An AI audit found no gap. Beyond Trudinger and Wang’s priority note, we found no specialist comment and no reported error. OSVerify has not reviewed it.

How the proof goes

  1. Where the dimension enters. The rigidity proof takes affine limits of the graph and asks how many flat directions they can have. The equation, rewritten as stationarity of affine area, gives a logarithmic integral inequality, and this is where the dimension enters: at its natural parameter, one quadratic form has determinant (n − 2)(10 − n)/16, which our computer checks is positive exactly for dimensions three through nine. That inequality forces a measure to grow exponentially, while cell bounds allow only polynomial growth, so no limit has two or more flat directions. An interior estimate of Trudinger and Wang then makes the third derivatives vanish, and the graph is quadratic.
  2. Dimension ten: a profile in a box. The dimension-ten example uses the ansatz u = √(F² + t²), which reduces the equation to a radial system. A contraction argument starts it smoothly at the origin, and a box for its logarithmic derivatives is shown to be invariant, with Trudinger and Wang’s singular profile at its corner. Our computer integrates the profile and sees it stay in the box, creeping toward that corner, and checks at sample points that the resulting function solves the ten-variable equation to rounding error.

The numbers in the video

  • Ours: quadratic functions give exactly 0 in the affine maximal equation; a perturbed paraboloid gives about 0.33 at (1, 0).
  • Ours: the quadratic form's determinant (n − 2)(10 − n)/16 (at its natural parameter) is positive exactly for n = 3, …, 9.
  • Ours: the dimension-ten profile, integrated numerically, stays inside the invariant box and creeps toward its corner (9/2, 7/2, 33/7).
  • Ours: at sample points the dimension-ten function solves the ten-variable equation to rounding error; adding a square does not give a solution in dimension 11.
  • Lean: 322 files and 40,454 lines in the import closure of the rigidity comparator (counted by us; not run by us).

Read the source

The 2 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00The question

The classical Bernstein theorem says that an entire minimal graph over the plane is flat. Its affine cousin replaces area by affine area, which is unchanged by volume-preserving affine maps. A convex graph is affine maximal when it is critical for affine area; then it satisfies a fourth-order equation. Every paraboloid is a solution: our computer checks that quadratic functions give exactly zero, while a slightly perturbed paraboloid does not. The question is whether paraboloids are the only complete solutions. For surfaces, Chern asked this in the late 1970s, and Calabi asked a version with completeness measured by the affine metric. Trudinger and Wang settled both, in 2000 and 2002; Li and Jia also proved the second by another route. In a 2008 survey they conjectured the answer: only paraboloids up to dimension nine, but a smooth nonquadratic example from dimension ten. They had already found a singular example in dimension ten. Shortly before this release, others wrote that even dimension three was open.

1:09The claim

Result 353 is two OpenAI papers, made public October 6, 2026. The first, 23 pages, dated September 24, claims rigidity in dimensions three through nine: a smooth, locally uniformly convex affine maximal graph that is complete for the metric it inherits from Euclidean space is an elliptic paraboloid. It also gives the affine-complete version, using Trudinger and Wang’s earlier work. The second, 7 pages, dated October 5, constructs a smooth entire nonquadratic affine maximal graph in dimension ten. Not claimed: anything in dimension eleven or higher, or the first counterexample in dimension ten. Hours after the release, Trudinger and Wang posted a paper with the same ansatz, noting it had been submitted on February 2, and Wang had announced it in a talk in April. Neither OpenAI paper cites their 2008 prediction.

2:09How the proof goes

The rigidity proof takes affine limits of the graph and asks how many flat directions they can have. The equation, rewritten as stationarity of affine area, gives a logarithmic integral inequality, and this is where the dimension enters: at its natural parameter, one quadratic form has determinant (n − 2)(10 − n)/16, which our computer checks is positive exactly for dimensions three through nine. That inequality forces a measure to grow exponentially, while cell bounds allow only polynomial growth, so no limit has two or more flat directions. An interior estimate of Trudinger and Wang then makes the third derivatives vanish, and the graph is quadratic. The dimension-ten example uses the ansatz u = √(F² + t²), which reduces the equation to a radial system. A contraction argument starts it smoothly at the origin, and a box for its logarithmic derivatives is shown to be invariant, with Trudinger and Wang’s singular profile at its corner. Our computer integrates the profile and sees it stay in the box, creeping toward that corner, and checks at sample points that the resulting function solves the ten-variable equation to rounding error.

3:27Where it stands

Both papers are unrefereed and unchanged since release. The rigidity theorem in dimensions three to nine is formalized in Lean, about 40,000 lines, not run by us; three outside projects re-ran it successfully, and the Lean proves the interior-estimate step its own way instead of assuming it. The affine-complete version and the dimension-ten example have no Lean. An AI audit found no gap. Beyond Trudinger and Wang’s priority note, we found no specialist comment and no reported error. If they hold, Euclidean-complete affine maximal graphs are paraboloids exactly up to dimension nine, and dimension ten is the first with a smooth exception.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.