AI Proved What?

Episode 358, October 2026

No conjugate points, yet never nonpositive?

An AI preprint claims a three-manifold without conjugate points that admits no nonpositively curved metric

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

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

Chapters

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

The claim, in plain words

A conjugate point is where nearby geodesics leaving a point come back together, at least to first order. On a round sphere of radius one, geodesics from the north pole meet again at the south pole: our computer finds the first refocusing at distance pi, 3.1416. In the flat plane and the hyperbolic plane they never refocus; they spread apart linearly or exponentially. Nonpositive curvature everywhere rules out conjugate points. The question is the converse, for closed manifolds: if some metric has no conjugate points, must the manifold also carry a metric of nonpositive curvature?

For surfaces the answer is yes. Gulliver showed that a metric without conjugate points can still have some positive curvature, so the question is about the manifold, not the metric. Ivanov and Kapovitch asked it in 2012, guessing no in general but saying it might be true in dimension three, and named graph manifolds as the main test case. A survey by Burns and Matveev first said dimension three was settled, and a year later corrected itself: still open even in dimension three.

Result 358 is one OpenAI paper, 22 pages, dated September 24 and made public October 6, 2026. It claims a closed, connected, orientable three-manifold that carries a smooth metric without conjugate points but admits no smooth metric of nonpositive curvature. The manifold is two copies of a one-holed torus times a circle, glued along their boundary tori by the matrix (1 1; 1 0).

What it doesn’t claim

The manifold is not new: Leeb showed in 1995 that gluings like this admit no nonpositively curved metric, and the paper says so. The new part is the metric. Not claimed: higher dimensions, or a classification of graph manifolds, and it is not the trace-above-two gluing in Ivanov and Kapovitch’s test question. We found no competing claim.

Where it stands

Posted as a preprint
OpenAI, 22 pages, dated September 24, 2026
Peer reviewed
Not yet
Formalized in Lean
The main theorem (scope notes)

Last checked October 19, 2026. The paper is unrefereed and unchanged since release. Its main theorem is formalized in Lean, about 25,000 lines, not run by us. The Lean statement matches the theorem, and the formal proof takes a different route for the curvature obstruction. The stronger group-theoretic result is not formalized. We found no specialist comment and no reported error. OSVerify has not reviewed it.

How the proof goes

  1. Why curvature ≤ 0 is impossible. Why no nonpositive curvature? In such a metric, loops of the shared torus would act, on the universal cover, as translations of a flat plane. Each piece forces two of these translation vectors to be perpendicular, giving u perpendicular to v and u plus v perpendicular to u, so u has length zero, which is impossible. Our computer checks this arithmetic, and that among 232 small integer gluings exactly eight, the signed permutations, pass Leeb’s test.
  2. Building the metric. The metric is built from nonpositively curved pieces made from a hyperbolic punctured torus, joined through a neck. Across the neck, a tiny shear realizes the integer twist, because the torus periods are chosen in a matching ratio. The neck must therefore contain some positive curvature, since this manifold has no nonpositively curved metric. So the hard part is showing that no geodesic picks up a conjugate point: an index-form identity, a classification of how geodesics visit the neck, and a uniform estimate for those that enter and come back, summed over all visits.

The numbers in the video

  • Ours: on the unit sphere, nearby geodesics from a point first refocus at distance π ≈ 3.1416; in the flat and hyperbolic planes they never do.
  • Ours: the gluing matrix (1 1; 1 0) has determinant −1 and trace 1; of 232 small integer gluings, exactly 8 (the signed permutations) pass Leeb's test.
  • Ours: with our own cutoff, the paper's neck is concave once its shear parameter δ is about 10⁻⁴; the paper only says δ is sufficiently small.
  • Lean: 19 files and 24,974 lines in the import closure of the comparator (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

A conjugate point is where nearby geodesics leaving a point come back together, at least to first order. On a round sphere of radius one, geodesics from the north pole meet again at the south pole: our computer finds the first refocusing at distance pi, 3.1416. In the flat plane and the hyperbolic plane they never refocus; they spread apart linearly or exponentially. Nonpositive curvature everywhere rules out conjugate points. The question is the converse, for closed manifolds: if some metric has no conjugate points, must the manifold also carry a metric of nonpositive curvature? For surfaces the answer is yes. Gulliver showed that a metric without conjugate points can still have some positive curvature, so the question is about the manifold, not the metric. Ivanov and Kapovitch asked it in 2012, guessing no in general but saying it might be true in dimension three, and named graph manifolds as the main test case. A survey by Burns and Matveev first said dimension three was settled, and a year later corrected itself: still open even in dimension three.

1:12The claim

Result 358 is one OpenAI paper, 22 pages, dated September 24 and made public October 6, 2026. It claims a closed, connected, orientable three-manifold that carries a smooth metric without conjugate points but admits no smooth metric of nonpositive curvature. The manifold is two copies of a one-holed torus times a circle, glued along their boundary tori by the matrix (1 1; 1 0). The manifold is not new: Leeb showed in 1995 that gluings like this admit no nonpositively curved metric, and the paper says so. The new part is the metric. Not claimed: higher dimensions, or a classification of graph manifolds, and it is not the trace-above-two gluing in Ivanov and Kapovitch’s test question. We found no competing claim.

2:04How the proof goes

Why no nonpositive curvature? In such a metric, loops of the shared torus would act, on the universal cover, as translations of a flat plane. Each piece forces two of these translation vectors to be perpendicular, giving u perpendicular to v and u plus v perpendicular to u, so u has length zero, which is impossible. Our computer checks this arithmetic, and that among 232 small integer gluings exactly eight, the signed permutations, pass Leeb’s test. The metric is built from nonpositively curved pieces made from a hyperbolic punctured torus, joined through a neck. Across the neck, a tiny shear realizes the integer twist, because the torus periods are chosen in a matching ratio. The neck must therefore contain some positive curvature, since this manifold has no nonpositively curved metric. So the hard part is showing that no geodesic picks up a conjugate point: an index-form identity, a classification of how geodesics visit the neck, and a uniform estimate for those that enter and come back, summed over all visits.

3:14Where it stands

The paper is unrefereed and unchanged since release. Its main theorem is formalized in Lean, about 25,000 lines, not run by us. The Lean statement matches the theorem, and the formal proof takes a different route for the curvature obstruction. The stronger group-theoretic result is not formalized. We found no specialist comment and no reported error. If it holds, in dimension three a metric without conjugate points does not force a closed manifold to admit nonpositive curvature.

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.