View source for Regularity of infinity-harmonic functions

'''Regularity of infinity-harmonic functions''' concerns the viscosity solutions of the infinity Laplace equation ⟨''D''<sup>2</sup>''u'' ∇''u'', ∇''u''⟩ = 0, the equation of absolutely minimizing Lipschitz extensions. Whether these solutions are continuously differentiable in dimensions ''d'' ≥ 3 had been open. A manuscript dated 4 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claims uniform interior ''C''<sup>1,α</sup> estimates in every dimension ''d'' ≥ 3. 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:
** Aronsson connected the equation with absolute minimizers, Lipschitz functions whose Lipschitz constant cannot be lowered on any subdomain with the same boundary values. Jensen established the viscosity characterization and uniqueness for the Dirichlet problem, and Crandall, Evans and Gariepy developed comparison with cones and the associated slope estimates.
** Crandall and Evans proved that blow-ups at a fixed point are affine. Savin proved continuity of the gradient in the plane, and Evans and Savin obtained planar interior ''C''<sup>1,α</sup> estimates for some positive exponent. Evans and Smart proved differentiability at every point in every dimension; continuity of the derivative is a further assertion. Peng, Zhang and Zhou proved interior ''C''<sup>1</sup> regularity for infinity-harmonic potentials in convex rings.
** For the planar endpoint exponent 1/3, the manuscript cites Brustad's June 2026 preprint, under additional assumptions on the gradient, and Xu's July 2026 preprint, which states unrestricted planar ''C''<sup>1,1/3</sup><sub>loc</sub> regularity and leaves open a universal endpoint norm estimate.
** Aronsson's example |''x''<sub>1</sub>|<sup>4/3</sup> − |''x''<sub>2</sub>|<sup>4/3</sup> shows that no exponent above 1/3 is possible in any dimension ''d'' ≥ 2.

== The original result ==
* '''Claim.''' Theorem 1.1 of the manuscript states that for every integer ''d'' ≥ 3 there are α<sub>''d''</sub> in (0, 1/3] and ''C''<sub>''d''</sub> such that every bounded infinity-harmonic function on the unit ball of '''R'''<sup>''d''</sup> is ''C''<sup>1,α<sub>''d''</sub></sup> on the half ball, with the sup norm of the gradient plus its α<sub>''d''</sub>-Hölder seminorm bounded by ''C''<sub>''d''</sub> times the oscillation on the unit ball. Corollary 1.2 states interior ''C''<sup>1</sup> regularity of every infinity-harmonic function on any open set in dimension ''d'' ≥ 3. The manuscript states that the exponent comes from a compactness argument and is not explicit.
* ''Method, as described:'' after adjoining a linear coordinate, a three-point estimate gives uniform affine approximation at small scales. Failure of a uniform power rate for affine fits in anisotropic cylinders, the scaling of Evans and Savin, produces an entire nonaffine solution of a limiting equation with affine fits at every center and scale. A Liouville theorem shows that such solutions are affine. Its proof combines an extremal horizontal Jensen defect, a variance-penalized barycentric envelope that remains a subsolution, and a fair choice between forward and backward optimizers that localizes contacts at small times.
* '''Source.''' The manuscript [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Uniform-Interior-C1alpha-Estimates-for-Infinity-Harmonic-Functions-October-4-2026 Uniform interior C<sup>1,α</sup> estimates for infinity-harmonic functions]. The collection contains no Lean formalization or scope note for this result.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 18 October 2026)
|-
| 2026-10-09 || A. Sobral, E. V. Teixeira and J. M. Urbano, [https://arxiv.org/abs/2610.13137v1 arXiv 2610.13137v1], ''Qualitative-to-quantitative regularity for degenerate equations'' || Related work (planar case) || A principle turning qualitative ''C''<sup>1,γ</sup> regularity of all solutions into uniform estimates for every smaller exponent. Applied to Xu's planar theorem, it gives uniform interior ''C''<sup>1,β</sup> estimates for planar infinity-harmonic functions for every β &lt; 1/3. It does not cite the OpenAI manuscript. || arXiv preprint, version 1.
|-
| 2026-10-12 to 2026-10-18 || K. Kitamura, [https://github.com/KitaKen1/infinity-laplacian-bounded-forcing/tree/de6c5cb152885a1c15aa90832bd1c8561e3bc90d KitaKen1/infinity-laplacian-bounded-forcing] (GitHub), with [https://github.com/KitaKen1/infinity-laplacian-bounded-forcing/blob/90d031a29226758eb5b16aeeba9078e8edb64552/PDF/infinity-laplacian-bounded-forcing.pdf a proof note] || Verification (Lean) and extension || Lean 4 proofs of three statements: Theorem 1.1 of the manuscript, its scaling to arbitrary balls, and a bounded-forcing variant for every ''n'' ≥ 2 in which the estimate gains a term (''RM'')<sup>1/3</sup> for |Δ<sub>∞</sub>''u''| ≤ ''M''. The repository states that the variant does not assert the endpoint exponent 1/3. The pull request below reports a successful public run at commit <code>90d031a</code> of the three Comparator targets, axiom audits and a fresh kernel replay, with only the standard axioms, and the repository keeps an [https://github.com/KitaKen1/infinity-laplacian-bounded-forcing/tree/1655481ffd47c05c45ebb9a3a366bd951e932495/ComparatorLog20261018 archive of the run]. || Repository; the pull request states that ChatGPT and OpenAI Codex assisted with the formalization, proofs and documentation.
|-
| 2026-10-12 to 2026-10-18 || Formal Conjectures [https://github.com/google-deepmind/formal-conjectures/issues/7198 issue 7198] and [https://github.com/google-deepmind/formal-conjectures/pull/7446 pull request 7446] (KitaKen1) || Formal statement || The issue proposed the bounded-forcing statement on 12 October. The pull request, opened 18 October, adds <code>FormalConjectures/Paper/InfinityLaplacian.lean</code> with the three statements marked research solved and with formal-proof links to the repository above. || Pull request open, not merged, as of 18 October 2026.
|-
| 2026-10-16 || J. Jardine, Lattice24, [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_370.json referee review] in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 Zenodo 10.5281/zenodo.23422995]) || Review (AI-assisted audit) || The review reports no gap. Its one minor remark states that the restriction ''d'' ≥ 3 is never used: the Liouville theorem is proved for every dimension and the reduction works for any ''d'', so the argument as written would also give the planar case. || Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.
|}

== 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]]