Honest coordinates?
An AI preprint claims bi-Lipschitz charts at every regular point of a noncollapsed RCD space
Covers result 357 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
4:10. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
Spaces with a lower bound on Ricci curvature, taken broadly to include limits of smooth ones, can have edges and cone points. Noncollapsed RCD spaces are a synthetic version of them: n-dimensional, and measured by n-dimensional volume. At a regular point, every zoom-in looks like flat n-space. The question is whether a neighbourhood of such a point has a bi-Lipschitz chart: coordinates that stretch or shrink distances by at most a fixed factor. Looking almost flat at each scale is not enough on its own. Our computer shows that a fixed 5% distortion at each of 40 halvings of the scale multiplies to about seven, and keeps growing, while errors with a finite sum keep the total bounded.
For the related limits of smooth manifolds, Cheeger and Colding found charts that are only bi-Hölder, which can distort small distances by an unbounded factor, and asked about a bi-Lipschitz upgrade in 1997. Kapovitch and Mondino extended bi-Hölder charts to RCD spaces, and Mondino and Naber covered almost every point by bi-Lipschitz pieces, but not open neighbourhoods of each point. In August 2026, Honda and Zhang recalled the conjecture that every regular point has a bi-Lipschitz chart.
Result 357 is one OpenAI paper, 43 pages, dated September 25 and made public October 6, 2026. It claims that for every dimension n of at least two there is one constant, depending only on n, such that every regular point of every noncollapsed RCD space of that dimension, whatever its curvature bound, has an open neighbourhood with a bi-Lipschitz chart onto an open set in n-space, distorting distances by at most that constant. The size of the neighbourhood may depend on the point.
What it doesn’t claim
Not claimed: a constant near one, smooth or harmonic coordinates, that the set of regular points is open, or anything for collapsed spaces. The neighbourhood may contain singular points. The catalog’s summary describes a point-dependent constant, weaker than the paper’s claim. We found no competing claim.
Where it stands
- Posted as a preprint
- OpenAI, 43 pages, dated September 25, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- None in OpenAI’s catalog; an uncatalogued development in the repository (Main.lean) proves a weaker form, with a constant per point; not checked by anyone
Last checked October 19, 2026. The paper is unrefereed and unchanged since release. The catalog lists no Lean, but OpenAI’s repository contains an uncatalogued Lean development of about 265,000 lines, with no gaps marked, whose main theorem gives a chart at every regular point with some constant, not the uniform one. No comparator certifies it, and we did not run it. An AI audit found no gap, without checking the imported analysis. We found no specialist comment and no reported error. OSVerify has not reviewed it.
How the proof goes
- Zoom in, then re-stretch. The proof zooms in at the point. In a noncollapsed space the volume density is at most one everywhere, and volume ratios, measured against a model space, never increase as the radius grows, so every nearby ball at every small scale is trapped close to Euclidean. Harmonic functions then give coordinates that are open and bi-Hölder, but their stretch may degenerate slowly across scales. The fix is to re-stretch the coordinate values by the right amount at each scale.
- A budget from volume. The budget for that comes from volume. At each scale the error is bounded by the drop in a volume ratio between two radii, plus a tiny curvature term, and those drops telescope: on the unit sphere, our computer finds they add up to one minus the ratio at radius one, about 8%. A two-point directional estimate turns this into control of stretching along the direction joining any two nearby points, and an iteration in coordinate space uses only the sum of the errors, never the sum of their square roots. The limit is the chart, with a constant of four times the square root of a number that depends on the dimension, so at least eight.
The numbers in the video
- Ours: a fixed 5% distortion at each of 40 halvings of the scale multiplies to 7.04, and keeps growing; errors 1/i² (a finite sum) keep the total below 3.7.
- Ours: √x is bi-Hölder but stretches by 4, 16 and 64 at scales 2⁻⁴, 2⁻⁸ and 2⁻¹².
- Ours: on the unit sphere, the volume-ratio drops at each halving of the radius add up to 1 − θ(1) ≈ 0.0806.
- Lean: 2,944 files and 265,431 lines in the import closure of the uncatalogued OAI.Geometry.RCD.Main (counted by us; not run by us).
Read the source
- Bi-Lipschitz Coordinates at Regular Points of Noncollapsed RCD Spaces (PDF), 43 pages.
- The collection’s catalog, where this is result 357.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
Spaces with a lower bound on Ricci curvature, taken broadly to include limits of smooth ones, can have edges and cone points. Noncollapsed RCD spaces are a synthetic version of them: n-dimensional, and measured by n-dimensional volume. At a regular point, every zoom-in looks like flat n-space. The question is whether a neighbourhood of such a point has a bi-Lipschitz chart: coordinates that stretch or shrink distances by at most a fixed factor. Looking almost flat at each scale is not enough on its own. Our computer shows that a fixed 5% distortion at each of 40 halvings of the scale multiplies to about seven, and keeps growing, while errors with a finite sum keep the total bounded. For the related limits of smooth manifolds, Cheeger and Colding found charts that are only bi-Hölder, which can distort small distances by an unbounded factor, and asked about a bi-Lipschitz upgrade in 1997. Kapovitch and Mondino extended bi-Hölder charts to RCD spaces, and Mondino and Naber covered almost every point by bi-Lipschitz pieces, but not open neighbourhoods of each point. In August 2026, Honda and Zhang recalled the conjecture that every regular point has a bi-Lipschitz chart.
1:18The claim
Result 357 is one OpenAI paper, 43 pages, dated September 25 and made public October 6, 2026. It claims that for every dimension n of at least two there is one constant, depending only on n, such that every regular point of every noncollapsed RCD space of that dimension, whatever its curvature bound, has an open neighbourhood with a bi-Lipschitz chart onto an open set in n-space, distorting distances by at most that constant. The size of the neighbourhood may depend on the point. Not claimed: a constant near one, smooth or harmonic coordinates, that the set of regular points is open, or anything for collapsed spaces. The neighbourhood may contain singular points. The catalog’s summary describes a point-dependent constant, weaker than the paper’s claim. We found no competing claim.
2:13How the proof goes
The proof zooms in at the point. In a noncollapsed space the volume density is at most one everywhere, and volume ratios, measured against a model space, never increase as the radius grows, so every nearby ball at every small scale is trapped close to Euclidean. Harmonic functions then give coordinates that are open and bi-Hölder, but their stretch may degenerate slowly across scales. The fix is to re-stretch the coordinate values by the right amount at each scale. The budget for that comes from volume. At each scale the error is bounded by the drop in a volume ratio between two radii, plus a tiny curvature term, and those drops telescope: on the unit sphere, our computer finds they add up to one minus the ratio at radius one, about 8%. A two-point directional estimate turns this into control of stretching along the direction joining any two nearby points, and an iteration in coordinate space uses only the sum of the errors, never the sum of their square roots. The limit is the chart, with a constant of four times the square root of a number that depends on the dimension, so at least eight.
3:24Where it stands
The paper is unrefereed and unchanged since release. The catalog lists no Lean, but OpenAI’s repository contains an uncatalogued Lean development of about 265,000 lines, with no gaps marked, whose main theorem gives a chart at every regular point with some constant, not the uniform one. No comparator certifies it, and we did not run it. An AI audit found no gap, without checking the imported analysis. We found no specialist comment and no reported error. If it holds, every regular point of a noncollapsed RCD space has bi-Lipschitz coordinates, with distortion controlled by the dimension alone.
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.