openai/math, paper family 377. OpenAI, `Uniform Interior C^{1,alpha} Estimates for Infinity-Harmonic Functions`, OpenAI math release (paper family 377). Statement formalised from Theorem 1.1 of the paper.openai/math 第 377 族。OpenAI, `Uniform Interior C^{1,alpha} Estimates for Infinity-Harmonic Functions`, OpenAI math release (paper family 377). Statement formalised from Theorem 1.1 of the paper. github.com/openai/math
When LOT proved this problem, a 2-level chain of intermediate theorems closed at once: each level is proved from the one below. We checked that chain twice, each run alone in its own sandbox with 8 whole CPU cores (16 CPUs) and 64 GiB locked for it: once with Lean’s original pipeline and once with LOT’s infrastructure, all six optimizations on. Both runs accepted every level.LOT 证这道题时，有一条 2 层的中间定理链同时收口：每一层都由下一层推出。我们把这条链检查了两遍，每一遍单独运行，独占锁定 8 个完整 CPU 核（16 个逻辑 CPU）和 64 GiB 内存：一遍用 Lean 原始流程，一遍用 LOT 基础设施（6 项优化全开）。两遍都接受了每一层。
Premise. Both runs start from the same situation: every theorem of the chain is already proved. LOT’s run also assumes what LOT has already done by then: everything below the chain was pre-checked, so the build of the library just below the chain is ready to reuse. That earlier work happens while the agents are still proving and is not inside the LOT time below; measured on its own, that build takes 231 s from scratch on the same 8 cores, 217 modules. The ledger is not assumed: the LOT run starts with an empty one.前提。两遍检查从相同的情况开始：链上每个定理都已经证明完毕。LOT 那一遍还默认 LOT 此前已经做完的工作：链下面的一切都做过预检查，紧挨着链的那一层库已经编译好、可以直接复用。这部分工作发生在 agent 还在证明的时候，不计入下面 LOT 的用时；单独测量，这次从头编译在同样的 8 个核上用时 231 秒，217 个模块。账本不算在前提里：LOT 那一遍从空账本开始。
What the two times are. Lean original is the wall-clock time to check the 2 levels one after another on one worker, each from scratch with the unmodified official checker. LOT’s infrastructure (all six optimizations on) is the wall-clock time of the latest pipeline on the same chain: a probe build that reuses the artefacts of the level below, then one check of the whole chain with parallel kernel replay. In this single replay the ledger is on but starts empty, and the queueing and speculative-checking optimizations, which act across a whole tree, have nothing to overlap with. Neither time includes the root check, queue waits or the scheduler’s pauses. The chain is not necessarily the tree’s longest: it is one closing cascade, the levels that became checkable one after another when the bottom theorem was proved, chosen for size and variety.两个时间分别是什么。Lean 原始流程：在一台 worker 上把这 2 层依次检查完的总用时，每层都用未改动的官方检查器从头检查。LOT 基础设施（6 项优化全开）：最新流程检查同一条链的总用时，先做一次复用下一层编译产物的探测编译，再用并行内核重放把整条链一次查完。在这次单独回放里，账本虽然开着但从空开始；排队和推测并行检查这两项是在整棵树的层面起作用的，这里没有可以重叠的东西。两个时间都不含根检查、排队等待和调度器的停顿。这条链不一定是这棵树里最长的：它是一次“收口”，即最底层定理证完后，上面各层依次变得可检查；挑选时兼顾规模和多样性。
Each bar spans its own run from start to finish, drawn from the measured stage times, so both end at the same length; the minutes on the right and the shared clock show how long each run really took. White ticks separate the levels.每条色条从头到尾对应各自那次运行，按实测各阶段用时画出，所以两条最终一样长；右侧分钟数和共用的时钟显示各自的真实用时。白色刻线分隔各层。
A level lights up when a run has checked it: red for the original pipeline, teal for the optimized one.某次运行检查完一层，该层就会亮起：红色是原始流程，青色是优化后的流程。
iharm_contact_propagationSections 6–7 / Proposition 7.1: propagate the extremal contact to a sequence of shrinking scales localized in fitted frames around one terminal point with finite slope. Assumes the uniform centered growth bound, which is supplied by the fit-compactness child.
∀ (E : Type) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (C0 : ℝ) (A : (E × ℝ → ℝ) → Prop) (d : ((E × ℝ) →L[ℝ] ℝ) → E × ℝ) (P M C : ℝ → (E × ℝ → ℝ) → E × ℝ → ℝ), (∀ L : (E × ℝ) →L[ℝ] ℝ, d L = ((InnerProductSpace.toDual ℝ E).symm (L.comp (ContinuousLinearMap.inl ℝ E ℝ)), (1 : ℝ))) → (∀ v : E × ℝ → ℝ, A v ↔ Continuous v ∧ (∀ (z : E × ℝ) (φ : E × ℝ → ℝ), ContDiffAt ℝ 2 φ z → φ z = v z → ((∀ᶠ w in nhds z, v w ≤ φ w) → 0 ≤ fderiv ℝ (fderiv ℝ φ) z (d (fderiv ℝ φ z)) (d (fderiv ℝ φ z))) ∧ ((∀ᶠ w in nhds z, φ w ≤ v w) → fderiv ℝ (fderiv ℝ φ) z (d (fderiv ℝ φ z)) (d (fderiv ℝ φ z)) ≤ 0)) ∧ ∀ (x : E) (t r : ℝ), 0 < r → ∃ (p : E) (a : ℝ), (∀ (h : E) (ℓ : ℝ), |ℓ| ≤ r → ‖h - ℓ • p‖ ≤ r → |v (x + h, t + ℓ) - v (x, t) - inner ℝ p h - (a - ‖p‖ ^ 2 / 2) * ℓ| ≤ C0 * r)) → (∀ (r : ℝ) (f : E × ℝ → ℝ) (z : E × ℝ), P r f z = sSup (Set.range fun y : E => f (y, z.2 + r) - ‖y - z.1‖ ^ 2 / (2 * r))) → (∀ (r : ℝ) (f : E × ℝ → ℝ) (z : E × ℝ), M r f z = sInf (Set.range fun y : E => f (y, z.2 - r) + ‖y - z.1‖ ^ 2 / (2 * r))) → (∀ (r : ℝ) (f : E × ℝ → ℝ) (z : E × ℝ), C r f z = sSup {s : ℝ | ∃ (n : ℕ) (θ : Fin n → ℝ) (y : Fin n → E), (∀ i, 0 < θ i) ∧ Finset.univ.sum θ = 1 ∧ Finset.univ.sum (fun i => θ i • y i) = z.1 ∧ s = Finset.univ.sum (fun i => θ i * f (y i, z.2)) - Finset.univ.sum (fun i => θ i * ‖y i - z.1‖ ^ 2) / (2 * r)}) → (∃ G : ℝ, 0 < G ∧ ∀ v : E × ℝ → ℝ, A v → (v (0, 1) = 0 ∧ ∀ (h : E) (ℓ : ℝ), |ℓ| ≤ 1 → ‖h‖ ≤ 1 → |v (h, 1 + ℓ)| ≤ C0) → ∀ K : ℝ, 2 ≤ K → ∀ (x : E) (t : ℝ), ‖x‖ ≤ K → |t| ≤ K → |v (x, t)| ≤ G * K * (1 + Real.log K) ^ 2) → ∀ (κ : ℝ) (v W : E × ℝ → ℝ), (0 < κ ∧ A v ∧ (v (0, 1) = 0 ∧ ∀ (h : E) (ℓ : ℝ), |ℓ| ≤ 1 → ‖h‖ ≤ 1 → |v (h, 1 + ℓ)| ≤ C0) ∧ (∀ z : E × ℝ, 0 < z.2 → W z = C z.2 v z - κ ^ 2 * z.2 / 2) ∧ ContinuousOn W {z : E × ℝ | 0 < z.2} ∧ (∀ z : E × ℝ, 0 < z.2 → v z - κ ^ 2 * z.2 / 2 ≤ W z ∧ W z ≤ v z) ∧ (∀ z : E × ℝ, 0 < z.2 → ∀ φ : E × ℝ → ℝ, ContDiffAt ℝ 2 φ z → φ z = W z → (∀ᶠ w in nhds z, W w ≤ φ w) → 0 ≤ fderiv ℝ (fderiv ℝ φ) z (d (fderiv ℝ φ z)) (d (fderiv ℝ φ z))) ∧ W (0, 1) = v (0, 1) ∧ ∃ H : ℝ, Filter.Tendsto (fun r : ℝ => (P r v (0, 1) - v (0, 1)) / r) (nhdsWithin 0 (Set.Ioi 0)) (nhds H) ∧ Filter.Tendsto (fun r : ℝ => (v (0, 1) - M r v (0, 1)) / r) (nhdsWithin 0 (Set.Ioi 0)) (nhds H) ∧ Filter.Tendsto (fun r : ℝ => (P r W (0, 1) - W (0, 1)) / r) (nhdsWithin 0 (Set.Ioi 0)) (nhds H)) → (∃ (b : E) (K : ℝ) (r : ℕ → ℝ) (x p : ℕ → E) (a : ℕ → ℝ), 0 ≤ K ∧ (∀ n, 0 < r n) ∧ Filter.Tendsto r Filter.atTop (nhds 0) ∧ (∃ H : ℝ, Filter.Tendsto (fun ℓ : ℝ => (P ℓ v (b, 0) - v (b, 0)) / ℓ) (nhdsWithin 0 (Set.Ioi 0)) (nhds H) ∧ Filter.Tendsto (fun ℓ : ℝ => (v (b, 0) - M ℓ v (b, 0)) / ℓ) (nhdsWithin 0 (Set.Ioi 0)) (nhds H)) ∧ ∀ n, (∀ (h : E) (ℓ : ℝ), |ℓ| ≤ (r n) → ‖h - ℓ • (p n)‖ ≤ (r n) → |v ((x n) + h, (r n) + ℓ) - v ((x n), (r n)) - inner ℝ (p n) h - ((a n) - ‖(p n)‖ ^ 2 / 2) * ℓ| ≤ C0 * (r n)) ∧ C (r n) v (x n, r n) - v (x n, r n) = κ ^ 2 * r n / 2 ∧ ‖b - x n + r n • p n‖ ≤ K * r n)iharm_liouvilleTheorem 3.1 (Liouville), proved in Sections 4-8, assuming SR and ST: for m >= 1 and a constant C0, a continuous viscosity solution v of D^2 v[(grad_x v, 1)] = 0 on R^m x R (tests in all variables) that has, at every center (x, t) and every radius R > 0, a fit (3.2) (p, a) with |v(x+h, t+l) - v(x,t) - p.h - (a - |p|^2/2) l| <= C0 R on the sheared box |l| <= R, |h - l p| <= R, is affine: v(x, t) = p.x + q t + c.
(∀ (V : Type) [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (N : ℕ) (U : Fin N → Set V) (g : Fin N → V → ℝ) (ξ : Fin N → (V →L[ℝ] ℝ) → V) (Ψ : (Fin N → V) → ℝ) (zh : Fin N → V) (c : Fin N → ℝ), (∀ j, IsOpen (U j)) → (∀ j, ContinuousOn (g j) (U j)) → (∀ j, Continuous (ξ j)) → (∀ j, ∀ z ∈ U j, ∀ φ : V → ℝ, ContDiffAt ℝ 2 φ z → φ z = g j z → (∀ᶠ y in nhds z, g j y ≤ φ y) → 0 ≤ fderiv ℝ (fderiv ℝ φ) z (ξ j (fderiv ℝ φ z)) (ξ j (fderiv ℝ φ z))) → (∀ j, zh j ∈ U j) → ContDiffAt ℝ 2 Ψ zh → (∀ᶠ z in nhds zh, Finset.univ.sum (fun j => g j (z j)) - Ψ z ≤ Finset.univ.sum (fun j => g j (zh j)) - Ψ zh) → 0 ≤ fderiv ℝ (fderiv ℝ Ψ) zh (fun j => c j • ξ j (fderiv ℝ (fun y => Ψ (Function.update zh j y)) (zh j))) (fun j => c j • ξ j (fderiv ℝ (fun y => Ψ (Function.update zh j y)) (zh j)))) → (∀ (V : Type) [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (U : Set V) (g : ℕ → V → ℝ) (g₀ : V → ℝ) (ξ : ℕ → (V →L[ℝ] ℝ) → V) (ξ₀ : (V →L[ℝ] ℝ) → V), IsOpen U → (∀ k, ContinuousOn (g k) U) → TendstoLocallyUniformlyOn g g₀ Filter.atTop U → Continuous ξ₀ → TendstoLocallyUniformly ξ ξ₀ Filter.atTop → (∀ᶠ k in Filter.atTop, ∀ z ∈ U, ∀ φ : V → ℝ, ContDiffAt ℝ 2 φ z → φ z = g k z → (∀ᶠ y in nhds z, g k y ≤ φ y) → 0 ≤ fderiv ℝ (fderiv ℝ φ) z (ξ k (fderiv ℝ φ z)) (ξ k (fderiv ℝ φ z))) → ∀ z ∈ U, ∀ φ : V → ℝ, ContDiffAt ℝ 2 φ z → φ z = g₀ z → (∀ᶠ y in nhds z, g₀ y ≤ φ y) → 0 ≤ fderiv ℝ (fderiv ℝ φ) z (ξ₀ (fderiv ℝ φ z)) (ξ₀ (fderiv ℝ φ z))) → ∀ (m : ℕ) (C0 : ℝ) (v : EuclideanSpace ℝ (Fin m) × ℝ → ℝ), 1 ≤ m → Continuous v → (∀ (z : EuclideanSpace ℝ (Fin m) × ℝ) (φ : EuclideanSpace ℝ (Fin m) × ℝ → ℝ), ContDiffAt ℝ 2 φ z → φ z = v z → ((∀ᶠ w in nhds z, v w ≤ φ w) → 0 ≤ fderiv ℝ (fderiv ℝ φ) z ((InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin m))).symm ((fderiv ℝ φ z).comp (ContinuousLinearMap.inl ℝ (EuclideanSpace ℝ (Fin m)) ℝ)), (1 : ℝ)) ((InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin m))).symm ((fderiv ℝ φ z).comp (ContinuousLinearMap.inl ℝ (EuclideanSpace ℝ (Fin m)) ℝ)), (1 : ℝ))) ∧ ((∀ᶠ w in nhds z, φ w ≤ v w) → fderiv ℝ (fderiv ℝ φ) z ((InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin m))).symm ((fderiv ℝ φ z).comp (ContinuousLinearMap.inl ℝ (EuclideanSpace ℝ (Fin m)) ℝ)), (1 : ℝ)) ((InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin m))).symm ((fderiv ℝ φ z).comp (ContinuousLinearMap.inl ℝ (EuclideanSpace ℝ (Fin m)) ℝ)), (1 : ℝ)) ≤ 0)) → (∀ (x : EuclideanSpace ℝ (Fin m)) (t R : ℝ), 0 < R → ∃ (p : EuclideanSpace ℝ (Fin m)) (a : ℝ), ∀ (h : EuclideanSpace ℝ (Fin m)) (ℓ : ℝ), |ℓ| ≤ R → ‖h - ℓ • p‖ ≤ R → |v (x + h, t + ℓ) - v (x, t) - inner ℝ p h - (a - ‖p‖ ^ 2 / 2) * ℓ| ≤ C0 * R) → ∃ (p : EuclideanSpace ℝ (Fin m)) (q c : ℝ), ∀ (x : EuclideanSpace ℝ (Fin m)) (t : ℝ), v (x, t) = inner ℝ p x + q * t + cimport ChallengeDeps
/-- Theorem 1.1 (uniform interior estimate): for every `d ≥ 3` there are `α_d ∈ (0, 1/3]` and
`C_d < ∞` such that every bounded infinity-harmonic `u ∈ C(B₁)` is `C^{1,α_d}` on `B_{1/2}` with
`‖∇u‖_{L∞(B_{1/2})} + [∇u]_{C^{0,α_d}(B_{1/2})} ≤ C_d osc_{B₁} u`. -/
theorem infinity_harmonic_c1alpha (d : ℕ) (hd : 3 ≤ d) :
∃ α : ℝ, 0 < α ∧ α ≤ 1 / 3 ∧ ∃ C : ℝ,
∀ u : EuclideanSpace ℝ (Fin d) → ℝ,
IsInfinityHarmonic (Metric.ball 0 1) u →
BddAbove (u '' Metric.ball 0 1) → BddBelow (u '' Metric.ball 0 1) →
let osc := sSup (u '' Metric.ball 0 1) - sInf (u '' Metric.ball 0 1)
(∀ x ∈ Metric.ball (0 : EuclideanSpace ℝ (Fin d)) (1 / 2), DifferentiableAt ℝ u x) ∧
(∀ x ∈ Metric.ball (0 : EuclideanSpace ℝ (Fin d)) (1 / 2), ‖gradient u x‖ ≤ C * osc) ∧
(∀ x ∈ Metric.ball (0 : EuclideanSpace ℝ (Fin d)) (1 / 2),
∀ y ∈ Metric.ball (0 : EuclideanSpace ℝ (Fin d)) (1 / 2),
‖gradient u x - gradient u y‖ ≤ C * osc * ‖x - y‖ ^ α) := by
sorry
LOT always checks the root, the problem’s own theorem, with the unmodified official pipeline from scratch, as Lean-Eval does. As a what-if we also checked the root once as an ordinary node with all of LOT’s optimizations, under the same premise as above: everything below it already proved and pre-checked.LOT 对根（题目本身的定理）总是用未改动的官方流程从头检查，与 Lean-Eval 一致。作为假设对比，我们还把根当作普通节点、打开 LOT 全部优化检查了一次，前提与上文相同：它下面的一切都已证明并做过预检查。
5.53× faster. Each bar spans its own run (colours as in the legend above). Not inside the LOT time, and listed here: the root’s probe build (92 s), done ahead of time while the last levels were checked, and the ledger of 51,167 constants learned from the chain’s own checks.快 5.53 倍。每条色条对应各自那次运行（颜色同上方图例）。不计入 LOT 用时、在此单独列出的有：根的探测编译（92 秒），在检查最后几层时就已提前完成；以及从这条链自己的检查里学到的 51,167 个常量的账本。
infinity_harmonic_c1alpha : (d : ℕ) (hd : 3 ≤ d) : ∃ α : ℝ, 0 < α ∧ α ≤ 1 / 3 ∧ ∃ C : ℝ, ∀ u : EuclideanSpace ℝ (Fin d) → ℝ, IsInfinityHarmonic (Metric.ball 0 1) u → BddAbove (u '' Metric.ball 0 1) → BddBelow (u '' Metric.ball 0 1) → (∀ x ∈ Metric.ball (0 : EuclideanSpace ℝ (Fin d)) (1 / 2), DifferentiableAt ℝ u x) ∧ (∀ x ∈ Metric.ball (0 : EuclideanSpace ℝ (Fin d)) (1 / 2), ‖gradient u x‖ ≤ C * (sSup (u '' Metric.ball 0 1) - sInf (u '' Metric.ball 0 1))) ∧ (∀ x ∈ Metric.ball (0 : EuclideanSpace ℝ (Fin d)) (1 / 2), ∀ y ∈ Metric.ball (0 : EuclideanSpace ℝ (Fin d)) (1 / 2), ‖gradient u x - gradient u y‖ ≤ C * (sSup (u '' Metric.ball 0 1) - sInf (u '' Metric.ball 0 1)) * ‖x - y‖ ^ α)| Configuration配置 | Wall clock (min)用时（分钟） | CPU-hours used实际 CPU 小时 |
|---|---|---|
| Lean's original pipelineLean 原始流程 | 12.0 | 1.103 |
| LOT’s infrastructure (all six optimizations)LOT 基础设施（6 项优化全开） | 4.1 | 0.168 |
| Optimizations of the previous release, levels side by side (2 workers)上一版优化，各层并排检查（2 个 worker） | 3.0 | 0.213 |
| As it ran in the proved tree (that day’s pipeline, queueing included)证明树当时实际用时（当时的流程，含排队） | 6.1 | – |
Conditions: each run alone on 8 whole physical cores (16 CPUs, both hyperthreads) and 64 GiB of one NUMA node of one host (AMD EPYC 7B13), locked exclusively for that run so that no other process could use those CPUs; network off, every tool and library mounted read-only; Lean leanprover/lean4:v4.35.0-rc3. The original pipeline is the unmodified official checker[3,4] run once per level; queue waits and the scheduler’s pauses between levels are not counted for either lane. Measured on 2026-10-24.条件：每次运行单独占用同一台主机（AMD EPYC 7B13）一个 NUMA 节点上的 8 个完整物理核（16 个逻辑 CPU，含超线程）和 64 GiB 内存，运行期间独占锁定，其他进程用不了这些 CPU；断网，所有工具和库只读挂载；Lean leanprover/lean4:v4.35.0-rc3。原始流程是未经改动的官方检查器[3,4]，每层运行一次；两条泳道都不计排队等待和层与层之间调度器的停顿。测于 2026-10-24。