A three-manifold without conjugate points or nonpositive curvature

Proves that a closed three-manifold can carry a metric without conjugate points yet no metric of nonpositive curvature.

1 paper September 24, 2026 Explained by AI

On a curved space, geodesics are the straightest paths. Two geodesics leaving one point can meet again, as lines of longitude meet at the poles; the meeting point is called a conjugate point. Nonpositive curvature rules out conjugate points, and experts asked if the reverse holds for whole spaces. This paper builds a closed three-dimensional space with a metric that has no conjugate points but that allows no metric of nonpositive curvature. Lean, a computer proof checker, has a formal statement of this result.

First step

2014

Sergei Ivanov and Vitali Kapovitch, Questions 1.1 and 8.1 on manifolds without conjugate points

Significance

Solid

It answers a question of Ivanov and Kapovitch, and of Burns and Matveev, in dimension three, with a Lean statement.

Trust

Formal proof listed

Field

Differential geometry

1 paper

The explanation

Start on a round sphere of radius 1. Two great circles leave the north pole at a small angle. Their gap grows like sin t, where t is the distance travelled. At t = π, about 3.1416, sin t is 0 again, so they meet at the south pole. On a flat plane the gap grows like t and never returns to 0. On a saddle-shaped surface of curvature −1 it grows like sinh t, faster still. At t = 2, sin t is about 0.909, t is 2, and sinh t is about 3.627. A Jacobi field measures this gap between nearby geodesics. A metric has no conjugate points if no nonzero Jacobi field vanishes at two different timesSource 1.

Nonpositive curvature, meaning curvature at most zero in every direction, rules out conjugate pointsSource 2. Gulliver showed the reverse fails for a single metric. He added positive curvature in small regions and kept the absence of conjugate pointsSource 3. But his spaces still carry some other metric of negative curvature. So the real question is about the space itself. If a closed space carries a metric without conjugate points, must it carry some metric of nonpositive curvature? Ivanov and Kapovitch asked this, and so did a survey by Burns and MatveevSource 4. For closed surfaces the answer is yes, so the problem starts in dimension threeSource 5.

The paper proves the answer is no in dimension threeSource 6. The space is built from two copies of a punctured torus times a circle. Their boundary tori are glued by the rule h₂ = h₁ + f₁ and f₂ = h₁Source 7. Here h is a loop around the surface boundary and f is a loop around the circle. As a whole-number matrix this rule is (1, 1; 1, 0), with determinant −1. A known argument of Leeb shows this gluing allows no metric of nonpositive curvature. Under such a metric, two pairs of loops would need perpendicular directions, and the gluing makes that impossibleSource 8.

The hard part is the metric. Each piece is nonpositively curved. Between them sits a neck, a torus times an intervalSource 9. Its metric comes from a carefully bent path of matrices. The obstacle is a geodesic that enters the neck, turns and comes back out. The paper bounds every such excursion uniformly in its angle and duration. This lets one metric handle every complete geodesicSource 10.

How sure is this? Lean, a computer proof checker, has a formal statement of the main result. It covers all geodesics, including constant ones and unbounded time. So the paper proves this result, as far as the Lean statement matches the paper. The extra focal-point and CAT(0) consequences are not in the Lean scope. No specialist review is published.

What it doesn't show. This does not show that every metric without conjugate points fails to be nonpositively curved. It gives one example, not a classification, and the Lean scope leaves out the focal-point and CAT(0) consequences.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

Solid, with a Lean statement of the main theorem. It gives one example in dimension three, not a general theory. No specialist review is published.

Words used

Geodesic: A straightest possible path on a curved space.
Jacobi field: A measure of the gap between a geodesic and nearby geodesics as they travel.
Conjugate points: Two points on a geodesic where a nonzero Jacobi field is zero, so nearby geodesics meet again.
Sectional curvature: The curvature of a space measured along one two-dimensional slice through a point.
Three-manifold: A space that looks like ordinary three-dimensional space near every point.
Punctured torus: The surface of a doughnut with one small disc removed.
Graph manifold: A three-manifold glued from pieces that are surfaces times a circle.

The original paper

A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric (PDF, opens in a new tab)
September 24, 2026 Formal proof listed

Lean notes

All quoted lines (10)

A Riemannian metric has no conjugate points if no nonzero Jacobi field along a geodesic vanishes at two distinct times.
A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric Back to text
Nonpositive sectional curvature implies this condition.
A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric Back to text
Gulliver showed that the converse fails for an individual metric: local modifications of negatively curved metrics can produce regions of positive curvature while preserving the absence of conjugate points.
A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric Back to text
This question appears in Ivanov and Kapovitch and in the survey of Burns and Matveev, which explicitly includes dimension three.
A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric Back to text
Uniformization then supplies a flat or negatively curved metric, so the existence problem begins in dimension three.
A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric Back to text
There exists a closed connected orientable smooth three-manifold $M$ with a $C^\infty$ Riemannian metric without conjugate points, such that $M$ admits no $C^\infty$ Riemannian metric whose sectional curvature is everywhere at most zero.
A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric Back to text
The gluing is $h_2=h_1+f_1,\qquad f_2=h_1.$
A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric Back to text
These two orthogonality conditions are incompatible with the gluing.
A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric Back to text
Each product piece has nonpositive sectional curvature. Between them we insert a neck $[0,1]\times T^2$ with metric $g=dt^2+dx^{\mathsf T}P(t)^{-1}\,dx,$ where $P(t)$ is a smooth path of positive definite matrices.
A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric Back to text
This is what permits one metric to handle every complete geodesic.
A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric Back to text

Other sources

openai/math, Lean scope note for family 358 It constructs a closed connected orientable smooth three-manifold with a smooth Riemannian metric having no conjugate points, while the same manifold admits no smooth metric of everywhere nonpositive sectional curvature.
openai/math release notes (2026): model provenance and review status manuscripts and supporting proof artifacts produced by an internal OpenAI model

356Gigli’s characterization of Alexandrov curvatureDifferential geometry
359Negative Kähler curvature without bounded holomorphic coordinatesDifferential geometry
360Weak MTW curvature gives convexity and regular optimal transportDifferential geometry
361Failure of integer-degree harmonic dimension comparisonDifferential geometry
352A finite-time singularity of Calabi flowDifferential geometry

Browse Differential geometry Curvature and geometric flows Open since the 2010s Lean-checked results Solid results