Lean formalization in OpenAI math repository (Result 085)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'An Endpoint Gradient Bound for the Centered Disk Maximal Operator'. We prove the endpoint gradient bound \|\nabla Mf\|_1\le C\|\nabla f\|_1 for every real-valued f\in W^{1,1}(\mathbb R^2), where Mf(x) is the supremum of the averages of |f| over disks centered at x, and C is an absolute constant. The maximal function belongs to W^{1,1}_{\mathrm{loc}}(\mathbb R^2) and has a globally integrable weak gradient. This gives a positive resolution of the planar centered-disk case of the endpoint question of Hajłasz and Onninen.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 085). The Lean development was not rebuilt locally.