Lean formalization of interior gradient Hölder estimates for infinity-harmonic functions

Juan J. Manfredi machine-checked in Lean one of the result families in OpenAI's October 2026 mathematics release, a uniform interior estimate giving every bounded viscosity solution of the infinity-Laplace equation on the unit ball of $\mathbb{R}^d$, $d \ge 3$, a gradient that is Hölder continuous on the half ball, and with it the corollary that every infinity-harmonic function on a connected open set in those dimensions is $C^1$; the Lean proofs and the blueprint were written by Claude under an AI-assisted formalization pipeline.

What was found

The infinity-Laplace equation $\Delta_\infty u = \sum u_i u_j u_{ij} = 0$ arises as the limit of the $p$-Laplace equation and governs absolutely minimizing Lipschitz extensions. How smooth its solutions are has been open away from the plane: Savin proved planar solutions are $C^1$ in 2005, and Evans and Smart proved in 2011 that solutions are differentiable everywhere in every dimension, but neither a uniform gradient bound nor $C^1$ regularity was known for $d \ge 3$. The OpenAI manuscript of 4 October 2026 claims both: for every $d \ge 3$ there are $\alpha \in (0, 1/3]$ and a finite $C$ with $\sup |\nabla u| + [\nabla u]_{C^{0,\alpha}} \le C\,\mathrm{osc}\,u$ on the half ball for every bounded viscosity solution on the unit ball, and as a consequence that every infinity-harmonic function on a connected open subset of $\mathbb{R}^d$ is $C^1$. The formalization carries all three of the manuscript's results, the estimate, the corollary and the Liouville theorem for the degenerate limiting equation on space-time that the proof rests on, as InfHarmonic.main_estimate, InfHarmonic.interior_C1 and InfHarmonic.liouville, proved from Mathlib and including the Crandall-Ishii-Lions theorem of sums and Alexandrov's theorem used along the way. It is pinned to Lean v4.35.0-rc2 and the matching Mathlib release, and the README reports no sorry outside the statement file and no axioms beyond the three standard ones.

Novelty check

arXiv, 2026-11-02: abs:"infinity-harmonic" returns 27 records and none states a uniform interior Hölder-gradient estimate in dimension three or above. The literature the search turns up is consistent with the problem having been open: Savin's planar $C^1$ result and a 2019 reworking of it, Evans and Smart's everywhere differentiability and its 2014 extension to a class of Aronsson equations, and, most usefully, arXiv:2610.13137 of 2026-10-09, which converts qualitative into quantitative regularity for degenerate equations and obtains uniform interior estimates for infinity-harmonic functions in the plane only, by way of Xu's planar qualitative $C^{1, 1/3}$ result. That paper appeared five days after the OpenAI manuscript's date and still treats the planar case as the frontier, which is evidence that the claim for $d \ge 3$ was not already in the literature. OpenAI's own formalization catalogue at lean/formalization.yaml lists no source matching this family, so the release attached no Lean proof to it, though that catalogue was only partly read. Within this registry the family is one of the 372 carried by 2026-10-06-openai-math-collection with no entry of its own, and no entry covers the infinity-Laplacian or infinity-harmonic functions.

Machine-checked elsewhere

Graded formally verified for verification and ai-led for autonomy. What these mean.

Cite this entry

whataifound.org. (2026). Lean formalization of interior gradient Hölder estimates for infinity-harmonic functions. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-29-infinity-harmonic-c1alpha-lean

@misc{whataifound-independent-2026-lean,
  title        = {Lean formalization of interior gradient Hölder estimates for infinity-harmonic functions},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Independent. Verification: Formally verified. Autonomy: AI-led.},
  url          = {https://whataifound.org/finding/2026-10-29-infinity-harmonic-c1alpha-lean}
}

Related findings

← All mathematics findings in the registry