AI Proved What?

Episode 360, October 2026

Curvature keeps transport tame?

Two AI preprints claim Villani’s MTW conjecture and Hölder optimal transport

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

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

Chapters

  1. 0:00The question
  2. 1:21The claim
  3. 2:25How the proof goes
  4. 3:29Where it stands

The claim, in plain words

Optimal transport asks for the cheapest way to move one distribution of mass onto another, here with cost the squared distance. On a line the answer is simply sorting: our computer checks all 5,040 matchings of seven points, and the sorted one is always cheapest. On a curved manifold the optimal map can jump, and whether it must be continuous depends on a fourth-order curvature condition of Ma, Trudinger and Wang, called MTW. Our computer finds that the MTW quantity is zero for the flat cost and positive on the round sphere for perpendicular directions.

A second ingredient is the injectivity domain: at each point, the set of initial velocities whose geodesics are still shortest a little past time one. On the round sphere it is a disc of radius pi; on flat tori, a square or a hexagon; all convex. A conjecture named after Villani, from a 2011 survey, says the weak form of MTW forces every injectivity domain to be convex. Figalli, Gallouët and Rifford proved it in 2014 when geodesics stop being shortest before reaching a conjugate point, and Figalli, Rifford and Villani showed that on surfaces, continuous transport is equivalent to weak MTW plus convex domains.

Result 360 is two OpenAI papers, dated September 25 and made public October 6, 2026. The first, 24 pages, claims the conjecture on every closed connected manifold of dimension two or more: weak MTW makes every injectivity domain convex, with no assumption about conjugate points. The second, 41 pages, builds on the first: for densities between two fixed bounds, the optimal map and its inverse are Hölder continuous, with one exponent and one constant for the whole class.

What it doesn’t claim

Not claimed: smoothness, or an explicit exponent, which comes from a contradiction argument. Weak MTW is itself restrictive, forcing nonnegative sectional curvature, so this is not continuity on every manifold. A one-line remark in the second paper combines it with Figalli, Rifford and Villani to get the equivalence of transport continuity and weak MTW; that remark is not formalized. We found no competing claim.

Where it stands

Posted as a preprint
OpenAI, 24 + 41 pages, dated September 25, 2026
Peer reviewed
Not yet
Formalized in Lean
Both main theorems (scope notes)

Last checked October 19, 2026. Both papers are unrefereed and unchanged since release. Both main theorems are formalized in Lean, about 19,000 and 74,000 lines, not run by us; the transport Lean re-proves what it needs rather than importing the convexity Lean. We found no specialist comment and no reported error. OSVerify has not reviewed it.

How the proof goes

  1. No hidden conjugate points. Weak MTW makes the cost’s Hessian concave along a line of velocities, tested in perpendicular directions. The new step rules out a hidden conjugate velocity on a segment of velocities whose geodesics are all shortest: it would have to degenerate along the segment, and then a blow-down estimate contradicts an exact radial identity. With that, the map from potential gradients to points is continued from small times to every time before one, a covering argument shows it cannot fold, and convexity follows from a potential built from just two targets.
  2. Hölder by contradiction. For the transport paper, convex sections turn a power bound on oscillation into a Hölder bound, with exponent half the power, capped at one half. The power itself is found by contradiction: a determinant gain proportional to a free parameter is capped by a comparison of Jacobians that uses weak MTW, so the parameter cannot be large. Our computer checks the paper’s projection and Schur-complement algebra exactly in 200 random cases.

The numbers in the video

  • Ours: on a line, optimal transport is sorting — checked against all 5,040 matchings of 7 points, three times, exactly.
  • Ours: the MTW quantity is 0 for the flat cost and, on the unit sphere for a perpendicular pair, starts at 1 and grows with the velocity.
  • Ours: the transport paper's projection and Schur-complement algebra holds exactly in 200 random cases each.
  • Lean: 210 files / 19,463 lines and 645 files / 74,032 lines in the two comparators' import closures, which share no files (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

Optimal transport asks for the cheapest way to move one distribution of mass onto another, here with cost the squared distance. On a line the answer is simply sorting: our computer checks all 5,040 matchings of seven points, and the sorted one is always cheapest. On a curved manifold the optimal map can jump, and whether it must be continuous depends on a fourth-order curvature condition of Ma, Trudinger and Wang, called MTW. Our computer finds that the MTW quantity is zero for the flat cost and positive on the round sphere for perpendicular directions. A second ingredient is the injectivity domain: at each point, the set of initial velocities whose geodesics are still shortest a little past time one. On the round sphere it is a disc of radius pi; on flat tori, a square or a hexagon; all convex. A conjecture named after Villani, from a 2011 survey, says the weak form of MTW forces every injectivity domain to be convex. Figalli, Gallouët and Rifford proved it in 2014 when geodesics stop being shortest before reaching a conjugate point, and Figalli, Rifford and Villani showed that on surfaces, continuous transport is equivalent to weak MTW plus convex domains.

1:21The claim

Result 360 is two OpenAI papers, dated September 25 and made public October 6, 2026. The first, 24 pages, claims the conjecture on every closed connected manifold of dimension two or more: weak MTW makes every injectivity domain convex, with no assumption about conjugate points. The second, 41 pages, builds on the first: for densities between two fixed bounds, the optimal map and its inverse are Hölder continuous, with one exponent and one constant for the whole class. Not claimed: smoothness, or an explicit exponent, which comes from a contradiction argument. Weak MTW is itself restrictive, forcing nonnegative sectional curvature, so this is not continuity on every manifold. A one-line remark in the second paper combines it with Figalli, Rifford and Villani to get the equivalence of transport continuity and weak MTW; that remark is not formalized. We found no competing claim.

2:25How the proof goes

Weak MTW makes the cost’s Hessian concave along a line of velocities, tested in perpendicular directions. The new step rules out a hidden conjugate velocity on a segment of velocities whose geodesics are all shortest: it would have to degenerate along the segment, and then a blow-down estimate contradicts an exact radial identity. With that, the map from potential gradients to points is continued from small times to every time before one, a covering argument shows it cannot fold, and convexity follows from a potential built from just two targets. For the transport paper, convex sections turn a power bound on oscillation into a Hölder bound, with exponent half the power, capped at one half. The power itself is found by contradiction: a determinant gain proportional to a free parameter is capped by a comparison of Jacobians that uses weak MTW, so the parameter cannot be large. Our computer checks the paper’s projection and Schur-complement algebra exactly in 200 random cases.

3:29Where it stands

Both papers are unrefereed and unchanged since release. Both main theorems are formalized in Lean, about 19,000 and 74,000 lines, not run by us; the transport Lean re-proves what it needs rather than importing the convexity Lean. We found no specialist comment and no reported error. If they hold, on closed manifolds of dimension two or more, weak MTW alone makes injectivity domains convex and optimal transport between densities bounded above and below Hölder continuous.

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.