AI Proved What?

Episode 366, October 2026

Only three shapes for every edge?

An AI preprint claims the interior Mumford–Shah conjecture in the plane, two days after a similar arXiv claim

Covers result 366 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

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

Chapters

  1. 0:00The question
  2. 1:13The claim
  3. 2:15How the proof goes
  4. 3:22Where it stands

The claim, in plain words

How should a computer draw the edges in a picture? In 1989, Mumford and Shah proposed an energy: approximate the picture by a function that is smooth except across a set of edges, and charge for wiggles inside the regions, for the total length of the edges, and for distance from the picture. In a one-dimensional toy, our computer finds the trade-off: smoothing a step of height h costs about 0.23 h², a cut costs one, so a cut wins once the step is taller than about 2.08.

Their conjecture says the best edges are simple: finitely many curves that run through, stop at a crack tip, or meet three at a time at 120°. Our computer shows why the angle: crossing the diagonals of a unit square costs 2.83, while two junctions at 120° cost 2.73. Near a crack tip the gradient blows up; for the model tip, the area where it exceeds t is exactly 1/(4π t⁴), a borderline rate that De Lellis and Focardi tied to the conjecture. Their 2025 monograph calls it a long-standing open problem, to date still open.

Result 366 is one OpenAI paper, 20 pages, dated September 24 and made public October 6, 2026. It claims the interior part of the planar conjecture for reduced absolute minimizers with bounded data: near every edge point inside the domain, the edges form one regular arc, a crack tip, or three arcs at 120°, and only finitely many pieces meet any compact interior region. A weak L⁴ bound on the gradient then follows, via known work.

What it doesn’t claim

Not claimed: anything at the boundary of the domain, or finitely many pieces overall. And it was not the first public claim. On September 22, Francesco Deangelis posted on the arXiv a claimed proof of the conjecture, including the same interior structure; his note says he obtained it using OpenAI’s ChatGPT Astra. The OpenAI paper cites it; both slide the floating piece, but they finish differently.

Where it stands

Posted as a preprint
OpenAI, 20 pages, dated September 24, 2026; an earlier claim by Deangelis (arXiv, September 22) is cited
Peer reviewed
Not yet; no specialist verdict on either paper
Formalized in Lean
None in OpenAI’s catalog; an uncatalogued development in the repository (CompactExclusion.lean) proves the paper’s new step, Proposition 5.1; the full theorem is stated in Lean but not proved

Last checked October 19, 2026. The paper is unrefereed and unchanged since release, and it leans on the cited theory. The release catalogue lists no Lean, but the repository holds an uncatalogued Lean proof of the new step, about 8,200 lines, not run by us; the full theorem is stated in Lean but not proved. We found no specialist verdict on either paper. OSVerify has not reviewed it.

How the proof goes

  1. Zooming in, and the floating piece. Zoom in at an edge point. Decades of work, collected in the De Lellis and Focardi monograph, show the zoomed picture is a line, a half-line or a 120-degree junction, unless a bounded piece of edge floats in a connected background. The paper rules out that last case. It splits the gradient into a field carrying the piece’s jumps and a harmonic part that extends across it, then slides the piece by a small vector t. Lengths and the piece’s own energy do not change; a cross term does, and it is harmonic in t with its minimum at zero, so it must be constant. Our computer shows the reason: a harmonic function’s average on a circle equals its centre value, so if the centre is a minimum, the function is flat on the circle.
  2. Deleting the piece. Varying the jumps along an arc of the piece then forces the whole gradient to vanish. The function is constant everywhere off the edges, so deleting it costs nothing and saves its length, contradicting minimality. Results from earlier work then turn each zoomed picture back into one of the three shapes at small scale.

The numbers in the video

  • Ours: in a 1-D toy, smoothing a step of height h costs 0.23 h² and a cut costs 1, so cutting wins above h = 2.08.
  • Ours: crossing the diagonals of a unit square costs 2.83; two 120° junctions cost 2.73.
  • Ours: for the model crack tip, the area where the gradient exceeds t is exactly 1/(4π t⁴).
  • Lean: 24 files and 8,228 lines in the import closure of the uncatalogued proof of the paper’s new step (counted by us; not run by us).

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00The question

How should a computer draw the edges in a picture? In 1989, Mumford and Shah proposed an energy: approximate the picture by a function that is smooth except across a set of edges, and charge for wiggles inside the regions, for the total length of the edges, and for distance from the picture. In a one-dimensional toy, our computer finds the trade-off: smoothing a step of height h costs about 0.23 h², a cut costs one, so a cut wins once the step is taller than about 2.08. Their conjecture says the best edges are simple: finitely many curves that run through, stop at a crack tip, or meet three at a time at 120°. Our computer shows why the angle: crossing the diagonals of a unit square costs 2.83, while two junctions at 120° cost 2.73. Near a crack tip the gradient blows up; for the model tip, the area where it exceeds t is exactly 1/(4π t⁴), a borderline rate that De Lellis and Focardi tied to the conjecture. Their 2025 monograph calls it a long-standing open problem, to date still open.

1:13The claim

Result 366 is one OpenAI paper, 20 pages, dated September 24 and made public October 6, 2026. It claims the interior part of the planar conjecture for reduced absolute minimizers with bounded data: near every edge point inside the domain, the edges form one regular arc, a crack tip, or three arcs at 120°, and only finitely many pieces meet any compact interior region. A weak L⁴ bound on the gradient then follows, via known work. Not claimed: anything at the boundary of the domain, or finitely many pieces overall. And it was not the first public claim. On September 22, Francesco Deangelis posted on the arXiv a claimed proof of the conjecture, including the same interior structure; his note says he obtained it using OpenAI’s ChatGPT Astra. The OpenAI paper cites it; both slide the floating piece, but they finish differently.

2:15How the proof goes

Zoom in at an edge point. Decades of work, collected in the De Lellis and Focardi monograph, show the zoomed picture is a line, a half-line or a 120-degree junction, unless a bounded piece of edge floats in a connected background. The paper rules out that last case. It splits the gradient into a field carrying the piece’s jumps and a harmonic part that extends across it, then slides the piece by a small vector t. Lengths and the piece’s own energy do not change; a cross term does, and it is harmonic in t with its minimum at zero, so it must be constant. Our computer shows the reason: a harmonic function’s average on a circle equals its centre value, so if the centre is a minimum, the function is flat on the circle. Varying the jumps along an arc of the piece then forces the whole gradient to vanish. The function is constant everywhere off the edges, so deleting it costs nothing and saves its length, contradicting minimality. Results from earlier work then turn each zoomed picture back into one of the three shapes at small scale.

3:22Where it stands

The paper is unrefereed and unchanged since release, and it leans on the cited theory. The release catalogue lists no Lean, but the repository holds an uncatalogued Lean proof of the new step, about 8,200 lines, not run by us; the full theorem is stated in Lean but not proved. We found no specialist verdict on either paper. If it holds, the edges inside an optimal planar picture come in just three shapes, as Mumford and Shah conjectured, now with two AI-generated proofs, dated two days apart.

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.