{"id":"palomar/PALOMAR-2026-10-29-000040","url":"https://github.com/na0b/infharmonic-lean/tree/e8710101271a529a8bd84fe0e610c3ab10de85b3","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-29-000040-v1.json","repo":"https://github.com/na0b/infharmonic-lean","tags":["math.AP","msc:35J94","msc:35B65","msc:35D40","msc:35B53","msc:68V20"],"score":0,"title":"Uniform interior C^{1,α} estimates for infinity-harmonic functions in dimensions d ≥ 3","trust":"high","domain":"math.AP","source":"palomar","authors":["Juan J. Manfredi"],"reviews":0,"subject":"math.AP","summary":"A complete Lean 4 / Mathlib formalization of the main results of the preprint \"Uniform Interior C^{1,α} Estimates for Infinity-Harmonic Functions\" (OpenAI, 2026). For every dimension d ≥ 3 there are α ∈ (0, 1/3] and C < ∞ such that every bounded viscosity solution u of the infinity-Laplace equation Δ_∞u = Σ u_i u_j u_ij = 0 on the unit ball of ℝ^d is differentiable on the half ball, with sup |∇u| + [∇u]_{C^{0,α}} ≤ C · osc u (Theorem 1.1). Consequently every infinity-harmonic function on a connected open subset of ℝ^d, d ≥ 3, is C¹ (Corollary 1.2). The proof rests on a Liouville theorem for…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"Uniform Interior C^{1,α} Estimates for Infinity-Harmonic Functions","identifier":"OpenAI Math Release preprint, October 4, 2026","relationship":"formalizes"}]}