AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Weak Hessian bounds along every geodesic in RCD spaces

Can the mathematical statement in Weak Hessian bounds along every geodesic in RCD spaces be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 356)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Weak Hessian bounds along every geodesic in RCD spaces'. On a full-support \mathrm{RCD}(K,N) space with 1\lt N\lt \infty, we prove that a bounded globally Lipschitz function whose distributional Hessian is bounded above by a bounded continuous function satisfies the corresponding second-derivative inequality along every minimizing geodesic.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 356). The Lean development was not rebuilt locally.