Regularity of infinity-harmonic functions
Regularity of infinity-harmonic functions concerns the viscosity solutions of the infinity Laplace equation ⟨D2u ∇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 (github.com/openai/math) claims uniform interior C1,α 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 C1,α 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 C1 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 C1,1/3loc regularity and leaves open a universal endpoint norm estimate.
- Aronsson's example |x1|4/3 − |x2|4/3 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 αd in (0, 1/3] and Cd such that every bounded infinity-harmonic function on the unit ball of Rd is C1,αd on the half ball, with the sup norm of the gradient plus its αd-Hölder seminorm bounded by Cd times the oscillation on the unit ball. Corollary 1.2 states interior C1 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 Uniform interior C1,α estimates for infinity-harmonic functions. The collection contains no Lean formalization or scope note for this result.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 18 October 2026) |
|---|---|---|---|---|
| 2026-10-09 | A. Sobral, E. V. Teixeira and J. M. Urbano, arXiv 2610.13137v1, Qualitative-to-quantitative regularity for degenerate equations | Related work (planar case) | A principle turning qualitative C1,γ regularity of all solutions into uniform estimates for every smaller exponent. Applied to Xu's planar theorem, it gives uniform interior C1,β estimates for planar infinity-harmonic functions for every β < 1/3. It does not cite the OpenAI manuscript. | arXiv preprint, version 1. |
| 2026-10-12 to 2026-10-18 | K. Kitamura, KitaKen1/infinity-laplacian-bounded-forcing (GitHub), with a proof note | Verification (Lean) and extension | Δ∞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 90d031a of the three Comparator targets, axiom audits and a fresh kernel replay, with only the standard axioms, and the repository keeps an 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 issue 7198 and pull request 7446 (KitaKen1) | Formal statement | The issue proposed the bounded-forcing statement on 12 October. The pull request, opened 18 October, adds FormalConjectures/Paper/InfinityLaplacian.lean 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, referee review in JJardine919/openai-math-audit (archived at 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.