Gigli's characterization of Alexandrov curvature
From OpenAI Aftermath
Gigli's characterization of Alexandrov curvature is a conjecture of N. Gigli (2019) relating two notions of a lower curvature bound on singular spaces: the Alexandrov lower bound, defined by comparing geodesic triangles with triangles in a model surface of constant curvature κ, and a lower bound for the distributional sectional curvature tensor that Gigli defined on RCD spaces, metric measure spaces with synthetic lower Ricci curvature bounds. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), dated 24 September 2026 and listed as its result 356, claim the conjecture in every dimension n ≥ 2 and a companion transfer theorem for weak Hessian bounds; the companion theorem has a Lean formalization, the characterization does not. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the main manuscript:
- Lott–Villani and Sturm developed synthetic lower Ricci curvature bounds through convexity of entropy along Wasserstein geodesics; Ambrosio–Gigli–Savaré introduced the RCD(K, ∞) framework with quadratic Cheeger energy, extended by Ambrosio–Gigli–Mondino–Rajala.
- Petrunin and Zhang–Zhu connected Alexandrov lower curvature bounds with the curvature-dimension condition, and Kuwae–Machigashira–Shioya supplied the Sobolev theory of Alexandrov spaces. Gigli defined the distributional curvature functional on RCD spaces and conjectured the characterization in dimensions at least two.
- Ketterer and Mondino characterized smooth sectional and intermediate Ricci bounds by optimal transport; Lebedeva and Petrunin constructed a weak curvature tensor for smoothable Alexandrov spaces; Brena and Gigli explained the regularity obstruction in passing from a distributional Hessian bound to convexity; and Erös, Kunzinger, Ohanyan and Vardabasso proved a local distributional-to-Alexandrov comparison for C1 metrics.
The original results
- Claim (characterization). The main theorem of Gigli's distributional curvature characterization of Alexandrov spaces states that, for an integer n ≥ 2, a real κ and a complete separable metric space, being an n-dimensional Alexandrov space with curvature bounded below by κ is equivalent to the following: with the n-dimensional Hausdorff measure as reference measure, the space has full support, is RCD((n − 1)κ, n) in the unreduced sense, and Gigli's curvature functional satisfies the lower bound κ on all test fields and nonnegative test functions of his original classes.
- Claim (companion). Weak Hessian bounds along every geodesic in RCD spaces states that, in a full-support RCD(K, N) space with 1 < N < ∞, a bounded globally Lipschitz function whose weak Hessian is bounded above by a bounded continuous function times the metric satisfies the corresponding one-dimensional distributional bound along every constant-speed minimizing geodesic, not only almost every one; the main manuscript uses it for the converse direction.
- Method, as described: the forward direction extracts the curvature functional from small Alexandrov configurations integrated against transported densities. The converse combines a heat-regularized index inequality, frames of test gradients along almost every relevant path, built from harmonic splitting maps with capacity estimates and Deng's continuity of tangent cones, a Hessian comparison for modified distance functions, the companion theorem along every geodesic, and the local-to-global theorem for Alexandrov spaces.
- Formalization, as described by the repository. The scope note lean/docs/356.md states that the Lean formalization transfers a weak Hessian upper bound to every prescribed minimizing geodesic in an RCD(K, N) space with finite N > 1, the theorem of the companion manuscript; the characterization itself is not formalized.
- Sources (openai/math repository, commit
7ef5c0c): Gigli's distributional curvature characterization of Alexandrov spaces and Weak Hessian bounds along every geodesic in RCD spaces, both dated 24 September 2026.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 30 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | Alexandrov curvature: from distributional tensors to every geodesic, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains the two expressions of a lower sectional-curvature bound, the analytic setting of RCD spaces with quadratic Sobolev energy, and how the companion paper isolates the passage from an integrated Hessian inequality to a statement along every geodesic. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) |
Review (fidelity of the formal statements) | Rates this family "supporting-only": only the companion statement along every constant-speed geodesic is stated in Lean, while Gigli's conjecture is not; it notes that the RCD and Sobolev calculus is built within the formalization and records a sandboxed Comparator pass for the challenge WeakHessian on 8 October 2026. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38051470892 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the solution of WeakHessian, in 1677 s. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list WeakHessian, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_197 of the characterization in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap and no minor notes. The reviewer states that it read every section and lists hand checks of the forward expansion and its averaging coefficients, the polarization identity for the curvature functional, and the Riccati evolution and cancellations of the heat-regularized index inequality. | Part of an audit that its README describes as complete for the collection's manuscripts without a Lean formalization. It is published under CC BY 4.0. |
| 2026-10-19 | AI Proved What?, episode 356 Fat triangles from a tensor?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of both claims and their history. The episode states that dimension one, other reference measures and upper curvature bounds are not claimed, and that for surfaces the direction from the RCD condition to the Alexandrov bound was already proved by Lytchak and Stadler in 2018, a result the paper does not cite. It also notes that the Lean formalization of the companion follows a different route from the companion's own proof. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as preprints: OpenAI, 53 + 11 pages, dated September 24, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the companion lemma only, not the characterization. The page states that it found no specialist comment and no reported error. |
Notes
- The background summarizes the main manuscript's own account of earlier work.
- See also Bi-Lipschitz charts at regular points of RCD spaces for another result of the collection on RCD spaces.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
