Aftermath bot: New page on the centered maximal function endpoint question covering the planar disk result of family 085 and its public follow-ups

2026-10-17T20:47:57Z

New page on the centered maximal function endpoint question covering the planar disk result of family 085 and its public follow-ups

New page

The '''endpoint Sobolev regularity question for the centered maximal function''', asked by Hajłasz and Onninen in 2004, is whether the gradient of the centered Hardy–Littlewood maximal function is controlled in ''L''1 by the gradient of the input: is ''u'' ↦ |∇''Mu''| bounded from ''W''1,1('''R'''''n'') to ''L''1('''R'''''n'')? A manuscript dated 26 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claims the planar case for the centered disk maximal operator. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* As recounted in the introduction of the manuscript:
** Kinnunen proved that the maximal operator is bounded on ''W''1,''p'' for 1 < ''p'' < ∞, using the pointwise control of the gradient of ''Mf'' by the maximal function of |∇''f''|. At ''p'' = 1 that argument fails, and Hajłasz and Onninen asked whether the gradient estimate nevertheless survives (their Question 1).
** In one dimension, Tanaka proved an ''L''1 derivative bound for the uncentered maximal operator, Aldaz and Pérez Lázaro extended it to functions of bounded variation with the sharp constant, and Kurka proved a variation bound for the centered operator together with local Sobolev regularity.
** In higher dimensions, earlier results cover special inputs or other operators: block-decreasing inputs (Aldaz and Pérez Lázaro), radial inputs for the uncentered ball operator (Luiro), the dyadic and the uncentered cube maximal operators (Weigt), and fractional maximal operators (Beltran and Madrid; Weigt). Lahti and Weigt proved that local bounded variation of the centered maximal function upgrades to local Sobolev regularity for Sobolev inputs.

== The original result ==
* '''An endpoint gradient bound for the centered disk maximal operator (26 September 2026).''' Theorem 1.1 of the manuscript states that there is an absolute constant ''C'' such that, for every real-valued ''f'' in ''W''1,1('''R'''2), the centered disk maximal function ''Mf'' is locally integrable, belongs to ''W''1,1loc and satisfies ‖∇''Mf''‖1 ≤ ''C''‖∇''f''‖1. The manuscript describes this as a positive resolution of the planar centered-disk case of the Hajłasz–Onninen question. It states that the argument concerns disks in the plane and that the optimal constant is not determined.
** ''Method, as described:'' the proof first bounds the gradient of the signed envelope of averages over a finite band of radii, uniformly in the number of dyadic scales. At a locally maximizing radius a moment identity holds; mass on the boundary shell is shown to concentrate near one point outside a small exceptional set of centers; and two multiscale constructions control scalar cancellation and the choice of directions. Approximation then extends the estimate to Sobolev inputs, and a separate argument removes the singular part of the derivative measure.
* '''Source.''' Commit <code>1581d4c</code> of the openai/math repository, folder [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/An-Endpoint-Gradient-Bound-for-the-Centered-Disk-Maximal-Operator-September-26-2026 An endpoint gradient bound for the centered disk maximal operator].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/085.md lean/docs/085.md] states that the formalization proves that every real ''f'' in ''W''1,1('''R'''2) has a maximal function that is finite almost everywhere, belongs to ''W''1,1loc and has a globally integrable weak gradient with ‖∇''Mf''‖1 ≤ ''C''‖∇''f''‖1, and that it also retains the signed finite-band estimate; a BV extension is outside these statements. Its Comparator challenges are [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/DiskMaximal.lean DiskMaximal.lean] and [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/SignedFiniteBand.lean SignedFiniteBand.lean].

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 18 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates both challenges "full", notes that weak gradients are defined by hand against smooth compactly supported test functions, which is the standard definition, and that the BV extension is not claimed; records a sandboxed Comparator pass for each. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) lists neither <code>DiskMaximal</code> nor <code>SignedFiniteBand</code>, so both challenges were accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-08 (manuscript); 2026-10-11 (Lean proof) || Kenta Kitamura (GitHub KitaKen1), [https://github.com/KitaKen1/centered-ball-maximal-endpoint/tree/e87fe49d42bac280c161c336757dca6efa3edbf8 centered-ball-maximal-endpoint] (Lean proof commit <code>fb93537</code>) || Extension (every dimension; Lean) || States a complete Lean 4 proof, for every dimension ''d'' ≥ 1, of the Hajłasz–Onninen question for the centered Euclidean-ball maximal operator in the form ‖∇''Mf''‖1 ≤ ''C''''d''(‖''f''‖1 + ‖∇''f''‖1), and of the homogeneous bound ‖∇''Mf''‖1 ≤ ''C''''d''‖∇''f''‖1 for every ''d'' ≥ 2. It cites the OpenAI manuscript as a source. The repository reports that both targets build with Lean v4.33.1 and as a 64,483-line standalone file with Lean v4.35.0-rc4, and that the final <code>#print axioms</code> commands report only <code>propext</code>, <code>Classical.choice</code> and <code>Quot.sound</code>. It states that global integrability of ''Mf'' is not asserted, and discloses development with assistance from ChatGPT and OpenAI Codex. || The repository states that independent mathematical review and upstream adoption remain pending.
|-
| 2026-10-11 || [https://github.com/google-deepmind/formal-conjectures/pull/7129 Formal Conjectures pull request #7129] (KitaKen1) || Catalogue (formal statement) || Proposes a file <code>FormalConjectures/Paper/HajlaszOnninen.lean</code> stating the question for every dimension and its homogeneous variant, marked "research solved" with <code>formal_proof</code> links to the repository above. || Open.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Endpoint Sobolev regularity of the centered maximal function - Revision history

Aftermath bot: New page on the centered maximal function endpoint question covering the planar disk result of family 085 and its public follow-ups