AI Proved What?

Episode 340, October 2026

Arnold’s guess fails?

An AI preprint claims a counterexample to the nearby Lagrangian conjecture

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

3:59. English captions available. The video loads from YouTube when you press play.

Chapters

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

The claim, in plain words

Phase space records a position and a momentum. Over a circle, the zero section, where momentum is zero, is the simplest exact Lagrangian: a closed curve that encloses no net action. The graph of the slope of any function on the circle is another, and our computer checks that its action is zero, while a curve shifted up by a constant is not exact. Any Hamiltonian motion of the zero section keeps it exact, as our computer’s animation shows.

The nearby Lagrangian conjecture, usually attributed to Arnold in 1986, asks the converse: is every closed exact embedded Lagrangian in a cotangent bundle just the zero section moved by a Hamiltonian motion? It was proved only over a few bases, all of dimension at most 2, such as the circle, the sphere, building on Hind’s work, and the torus. In every dimension, Abouzaid and Kragh showed that such a Lagrangian has the simple homotopy type of the base, and later work constrained it further. In 2025, Courte and Porcelli wrote that no counterexamples are known, even to a stronger version.

Result 340 is one OpenAI paper, 28 pages, dated September 23 and made public October 6, 2026. It claims a counterexample. For some large even number N, in the cotangent bundle of the product of a 9-sphere and an (N − 1)-sphere, there is a closed exact embedded Lagrangian, diffeomorphic to the base, that no compactly supported Hamiltonian motion carries the zero section onto. The value of N is not computed; the construction needs it to be at least 40.

What it doesn’t claim

Not claimed: an exotic Lagrangian, since this one is diffeomorphic to the base; any counterexample in low dimensions; or a specific value of N.

Where it stands

Posted as a preprint
OpenAI, 28 pages, dated September 23, 2026
Reviewed by OSVerify
0 major, 1 minor issue (a citation number); not a certification
Peer reviewed
Not yet
Formalized in Lean
Partly: about 22,000 uncatalogued lines, with two key topological steps assumed

Last checked October 19, 2026. The paper is unrefereed and unchanged since release. OSVerify reviewed it and reported no major issue and one minor one, a wrong theorem number in a citation; that is not a certification. About 22,000 lines of uncatalogued Lean, not run by us, derive the counterexample from Lean versions of its two topological steps, the hidden class and the one-critical-point argument, which are assumed rather than formalized. The argument also leans on very recent preprints for its model identifications. We found no specialist comment and no reported mathematical error. OSVerify has not reviewed it.

How the proof goes

  1. A hidden class, then a Lagrangian that carries it. The obstruction lives in Waldhausen’s space of tubes, built from functions that look quadratic at infinity. A count of group sizes, 8 against 32, using Rognes’s computation for the smooth Whitehead spectrum of a point, gives a nonzero tube class whose spherical image vanishes; our computer redoes this count over all 512 possible maps. The paper then builds a generating family whose data at infinity is that class. A momentum-separation trick makes the resulting Lagrangian embedded rather than merely immersed; our toys show how such families can produce double points, and how separation pulls the branches apart.
  2. If it could be moved, the class would vanish. Now suppose a Hamiltonian motion carried the zero section onto this Lagrangian. The paper follows the generating family step by step back along the motion, to the zero section. At the end, each fiber has exactly one nondegenerate critical point, and Morse theory, families of h-cobordisms and Igusa’s stability theorem then force the tube class to vanish, because its spherical image is still trivial. That contradicts the nonzero class.

The numbers in the video

  • Ours: in the phase space of a circle, the graph of a slope has action 0 (exact), while a curve shifted by 0.1 has action 2π·0.1 ≈ 0.628 (not exact).
  • Ours: the group count behind the hidden class, 8 against 32, checked over all 512 possible maps.
  • Ours: a generating family can produce an exact figure eight with one double point; momentum separation pulls branches apart (ratio 0.005, 0.877, 0.995 as the parameter grows).
  • Lean (uncatalogued): main_reduction’s import closure is 86 files and 22,119 lines; it assumes the two topological steps (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

Phase space records a position and a momentum. Over a circle, the zero section, where momentum is zero, is the simplest exact Lagrangian: a closed curve that encloses no net action. The graph of the slope of any function on the circle is another, and our computer checks that its action is zero, while a curve shifted up by a constant is not exact. Any Hamiltonian motion of the zero section keeps it exact, as our computer’s animation shows. The nearby Lagrangian conjecture, usually attributed to Arnold in 1986, asks the converse: is every closed exact embedded Lagrangian in a cotangent bundle just the zero section moved by a Hamiltonian motion? It was proved only over a few bases, all of dimension at most 2, such as the circle, the sphere, building on Hind’s work, and the torus. In every dimension, Abouzaid and Kragh showed that such a Lagrangian has the simple homotopy type of the base, and later work constrained it further. In 2025, Courte and Porcelli wrote that no counterexamples are known, even to a stronger version.

1:09The claim

Result 340 is one OpenAI paper, 28 pages, dated September 23 and made public October 6, 2026. It claims a counterexample. For some large even number N, in the cotangent bundle of the product of a 9-sphere and an (N − 1)-sphere, there is a closed exact embedded Lagrangian, diffeomorphic to the base, that no compactly supported Hamiltonian motion carries the zero section onto. The value of N is not computed; the construction needs it to be at least 40. Not claimed: an exotic Lagrangian, since this one is diffeomorphic to the base; any counterexample in low dimensions; or a specific value of N.

1:54How the proof goes

The obstruction lives in Waldhausen’s space of tubes, built from functions that look quadratic at infinity. A count of group sizes, 8 against 32, using Rognes’s computation for the smooth Whitehead spectrum of a point, gives a nonzero tube class whose spherical image vanishes; our computer redoes this count over all 512 possible maps. The paper then builds a generating family whose data at infinity is that class. A momentum-separation trick makes the resulting Lagrangian embedded rather than merely immersed; our toys show how such families can produce double points, and how separation pulls the branches apart. Now suppose a Hamiltonian motion carried the zero section onto this Lagrangian. The paper follows the generating family step by step back along the motion, to the zero section. At the end, each fiber has exactly one nondegenerate critical point, and Morse theory, families of h-cobordisms and Igusa’s stability theorem then force the tube class to vanish, because its spherical image is still trivial. That contradicts the nonzero class.

3:04Where it stands

The paper is unrefereed and unchanged since release. OSVerify reviewed it and reported no major issue and one minor one, a wrong theorem number in a citation; that is not a certification. About 22,000 lines of uncatalogued Lean, not run by us, derive the counterexample from Lean versions of its two topological steps, the hidden class and the one-critical-point argument, which are assumed rather than formalized. The argument also leans on very recent preprints for its model identifications. We found no specialist comment and no reported mathematical error. If it holds, Arnold’s expectation fails in general: in very high dimension, a cotangent bundle can contain an exact Lagrangian that is shaped exactly like the base but cannot be moved onto it.

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.