Lean formalization in OpenAI math repository (Result 081)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Riesz transforms and uniform rectifiability in higher codimension'. We prove that an n-Ahlfors–David regular Radon measure on ℝd is uniformly n-rectifiable if its n-dimensional Riesz transform is uniformly bounded from scalar L^2(\mu) to vector-valued L^2(\mu) over all positive hard truncations, for integers d ≥ 4 and 2\le n\le d-2. This gives a positive answer to the David–Semmes Riesz-transform question in its remaining higher-codimension range. The conclusion gives uniform big pieces of Lipschitz images of Euclidean balls.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 081). The Lean development was not rebuilt locally.