Lean formalization in OpenAI math repository (Result 361)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A counterexample to integer-degree harmonic dimension comparison'. For some even n ≥ 8 and integer k ≥ 2, we construct a complete smooth metric on ℝn with nonnegative Ricci curvature whose space of real harmonic functions of pointwise polynomial growth at most k has dimension larger than the Euclidean harmonic-polynomial dimension. The metric is Euclidean near the origin, has asymptotic volume ratio strictly between zero and one, and has nonunique tangent cones at infinity. This answers the integer-degree form of Yau's dimension comparison question in the negative.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 361). The Lean development was not rebuilt locally.