Lean-Eval problem sphere_theorem_differentiable (submitted by Kim Morrison). S. Brendle & R. Schoen, Manifolds with 1/4-pinched curvature are space forms, J. AMS 22 (2009). Knill, Some fundamental theorems in mathematics, §121.Lean-Eval 题目 sphere_theorem_differentiable（提交者 Kim Morrison）。S. Brendle & R. Schoen, Manifolds with 1/4-pinched curvature are space forms, J. AMS 22 (2009). Knill, Some fundamental theorems in mathematics, §121. github.com/leanprover/lean-eval
When LOT proved this problem, a 3-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 证这道题时，有一条 3 层的中间定理链同时收口：每一层都由下一层推出。我们把这条链检查了两遍，每一遍单独运行，独占锁定 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 1536 s from scratch on the same 8 cores, 1198 modules. The ledger is not assumed: the LOT run starts with an empty one.前提。两遍检查从相同的情况开始：链上每个定理都已经证明完毕。LOT 那一遍还默认 LOT 此前已经做完的工作：链下面的一切都做过预检查，紧挨着链的那一层库已经编译好、可以直接复用。这部分工作发生在 agent 还在证明的时候，不计入下面 LOT 的用时；单独测量，这次从头编译在同样的 8 个核上用时 1536 秒，1198 个模块。账本不算在前提里：LOT 那一遍从空账本开始。
What the two times are. Lean original is the wall-clock time to check the 3 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 上把这 3 层依次检查完的总用时，每层都用未改动的官方检查器从头检查。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.某次运行检查完一层，该层就会亮起：红色是原始流程，青色是优化后的流程。
SphereFlow.ThreeD.maximal_ricci_flow_round_limitFor an already supplied finite-time classical Ricci flow on a closed connected three-manifold, positive initial Ricci and the curvature continuation obstruction imply that g(t)/(4*(T-t)) converges to a smooth metric of sectional curvature one, with a torsion-free compatible connection.
∀ {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [CompleteSpace E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (⊤ : ℕ∞) M] [ModelWithCorners.Boundaryless I] [T2Space M] [CompactSpace M] [ConnectedSpace M] (T : ℝ) (g : ℝ → Bundle.RiemannianMetric (TangentSpace I : M → Type _)) (c : ℝ → CovariantDerivative I E (TangentSpace I : M → Type _)) (R : ℝ → M → E →ₗ[ℝ] E →ₗ[ℝ] E →ₗ[ℝ] E), Module.finrank ℝ E = 3 → 0 < T → (∀ x (v : TangentSpace I x), v ≠ 0 → 0 < LinearMap.trace ℝ E (((R 0 x).flip v).flip v)) → ContMDiffOn (ModelWithCorners.prod (modelWithCornersSelf ℝ ℝ) I) (ModelWithCorners.prod I (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) (⊤ : ℕ∞) (fun p : ℝ × M => @Bundle.TotalSpace.mk' M (fun x => TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ) (E →L[ℝ] E →L[ℝ] ℝ) p.2 ((g p.1).inner p.2)) (Set.prod (Set.Ico 0 T) Set.univ) → (∀ t ∈ Set.Ico 0 T, CovariantDerivative.ContMDiffCovariantDerivative (c t) (⊤ : ℕ∞) ∧ (c t).torsion = 0 ∧ @LeanEval.Geometry.SphereTheorem.IsMetricCompatible E _ _ H _ I M _ _ _ (Bundle.RiemannianBundle.mk (g t)) (c t) ∧ (∀ X Y Z : (x : M) → TangentSpace I x, ContMDiff I (ModelWithCorners.tangent I) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' E x (X x)) → ContMDiff I (ModelWithCorners.tangent I) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' E x (Y x)) → ContMDiff I (ModelWithCorners.tangent I) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' E x (Z x)) → ∀ x, R t x (X x) (Y x) (Z x) = LeanEval.Geometry.SphereTheorem.curv (c t) X Y Z x) ∧ (∀ x (v : TangentSpace I x), HasDerivWithinAt (fun s => (g s).inner x v v) (-2 * LinearMap.trace ℝ E (((R t x).flip v).flip v)) (Set.Ico 0 T) t)) → (¬ ∃ B : ℝ, ∀ t ∈ Set.Ico 0 T, ∀ x (v : TangentSpace I x), |LinearMap.trace ℝ E (((R t x).flip v).flip v)| ≤ B * (g t).inner x v v) → ∃ (gLimit : Bundle.RiemannianMetric (TangentSpace I : M → Type _)) (cLimit : CovariantDerivative I E (TangentSpace I : M → Type _)), ContMDiff I (ModelWithCorners.prod I (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' (E →L[ℝ] E →L[ℝ] ℝ) x (gLimit.inner x)) ∧ cLimit.torsion = 0 ∧ @LeanEval.Geometry.SphereTheorem.IsMetricCompatible E _ _ H _ I M _ _ _ (Bundle.RiemannianBundle.mk gLimit) cLimit ∧ (∀ X Y : (x : M) → TangentSpace I x, ContMDiff I (ModelWithCorners.tangent I) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' E x (X x)) → ContMDiff I (ModelWithCorners.tangent I) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' E x (Y x)) → ∀ x, gLimit.inner x (X x) (X x) = 1 → gLimit.inner x (Y x) (Y x) = 1 → gLimit.inner x (X x) (Y x) = 0 → gLimit.inner x (LeanEval.Geometry.SphereTheorem.curv cLimit X Y Y x) (X x) = 1) ∧ (∀ x (u v : TangentSpace I x), Filter.Tendsto (fun t => (4 * (T - t))⁻¹ * (g t).inner x u v) (nhdsWithin T (Set.Iio T)) (nhds (gLimit.inner x u v)))SphereFlow.connected_three_dimensional_roundingOn a connected compact smooth boundaryless three-manifold, a smooth metric with smooth torsion-free compatible connection and positive sectional curvature admits a smooth metric and smooth torsion-free compatible connection with a positive constant sectional curvature on orthonormal pairs. The analytic proof uses positive sectional curvature implies positive Ricci curvature and Hamilton convergence.
∀ {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [CompleteSpace E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (⊤ : ℕ∞) M] [ModelWithCorners.Boundaryless I] [T2Space M] [CompactSpace M] [ConnectedSpace M] (g₀ : Bundle.RiemannianMetric (TangentSpace I : M → Type _)), Module.finrank ℝ E = 3 → ContMDiff I (ModelWithCorners.prod I (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' (E →L[ℝ] E →L[ℝ] ℝ) x (g₀.inner x)) → ∀ (cov : CovariantDerivative I E (TangentSpace I : M → Type _)), CovariantDerivative.ContMDiffCovariantDerivative cov (⊤ : ℕ∞) → cov.torsion = 0 → @LeanEval.Geometry.SphereTheorem.IsMetricCompatible E _ _ H _ I M _ _ _ (Bundle.RiemannianBundle.mk g₀) cov → (∀ (X Y : (x : M) → TangentSpace I x), ContMDiff I (ModelWithCorners.tangent I) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' E x (X x)) → ContMDiff I (ModelWithCorners.tangent I) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' E x (Y x)) → ∀ x, g₀.inner x (X x) (X x) = 1 → g₀.inner x (Y x) (Y x) = 1 → g₀.inner x (X x) (Y x) = 0 → 0 < g₀.inner x (LeanEval.Geometry.SphereTheorem.curv cov X Y Y x) (X x)) → ∃ (g : Bundle.RiemannianMetric (TangentSpace I : M → Type _)) (cov' : CovariantDerivative I E (TangentSpace I : M → Type _)) (k : ℝ), ContMDiff I (ModelWithCorners.prod I (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' (E →L[ℝ] E →L[ℝ] ℝ) x (g.inner x)) ∧ CovariantDerivative.ContMDiffCovariantDerivative cov' (⊤ : ℕ∞) ∧ cov'.torsion = 0 ∧ @LeanEval.Geometry.SphereTheorem.IsMetricCompatible E _ _ H _ I M _ _ _ (Bundle.RiemannianBundle.mk g) cov' ∧ 0 < k ∧ (∀ (X Y : (x : M) → TangentSpace I x), ContMDiff I (ModelWithCorners.tangent I) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' E x (X x)) → ContMDiff I (ModelWithCorners.tangent I) (⊤ : ℕ∞) (fun x => Bundle.TotalSpace.mk' E x (Y x)) → ∀ x, g.inner x (X x) (X x) = 1 → g.inner x (Y x) (Y x) = 1 → g.inner x (X x) (Y x) = 0 → g.inner x (LeanEval.Geometry.SphereTheorem.curv cov' X Y Y x) (X x) = k)SphereFlow.three_dimensional_roundingA compact smooth boundaryless Riemannian manifold of exact dimension 3 with positive sectional curvature admits a weakly smooth metric, a torsion-free compatible connection, and a positive locally constant curvature function satisfying the full sectional numerator identity. Includes empty, disconnected and nonorientable manifolds. The analytic construction for three-manifolds uses positive sectional curvature implies positive Ricci curvature, followed by Hamilton convergence.
∀ {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [CompleteSpace E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ((⊤ : ℕ∞) : WithTop ℕ∞) M] [ModelWithCorners.Boundaryless I] [T2Space M] [CompactSpace M] (g₀ : Bundle.RiemannianMetric (TangentSpace I : M → Type _)), Module.finrank ℝ E = 3 → ContMDiff I (ModelWithCorners.prod I (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : M => Bundle.TotalSpace.mk' (E →L[ℝ] E →L[ℝ] ℝ) x (g₀.inner x)) → ∀ (cov : CovariantDerivative I E (TangentSpace I : M → Type _)), CovariantDerivative.ContMDiffCovariantDerivative cov ((⊤ : ℕ∞) : WithTop ℕ∞) → cov.torsion = 0 → @LeanEval.Geometry.SphereTheorem.IsMetricCompatible E _ _ H _ I M _ _ _ (Bundle.RiemannianBundle.mk g₀) cov → (∀ (X Y : (x : M) → TangentSpace I x), ContMDiff I (ModelWithCorners.tangent I) ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : M => Bundle.TotalSpace.mk' E x (X x)) → ContMDiff I (ModelWithCorners.tangent I) ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : M => Bundle.TotalSpace.mk' E x (Y x)) → ∀ (x : M), g₀.inner x (X x) (X x) = (1 : ℝ) → g₀.inner x (Y x) (Y x) = (1 : ℝ) → g₀.inner x (X x) (Y x) = (0 : ℝ) → 0 < g₀.inner x (LeanEval.Geometry.SphereTheorem.curv cov X Y Y x) (X x)) → ∃ (g : Bundle.RiemannianMetric (TangentSpace I : M → Type _)) (cov' : CovariantDerivative I E (TangentSpace I : M → Type _)) (κ : M → ℝ), (∀ (X Y : (x : M) → TangentSpace I x), ContMDiff I (ModelWithCorners.tangent I) ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : M => Bundle.TotalSpace.mk' E x (X x)) → ContMDiff I (ModelWithCorners.tangent I) ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : M => Bundle.TotalSpace.mk' E x (Y x)) → ContMDiff I (modelWithCornersSelf ℝ ℝ) ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : M => g.inner x (X x) (Y x))) ∧ cov'.torsion = 0 ∧ @LeanEval.Geometry.SphereTheorem.IsMetricCompatible E _ _ H _ I M _ _ _ (Bundle.RiemannianBundle.mk g) cov' ∧ IsLocallyConstant κ ∧ (∀ x : M, 0 < κ x) ∧ (∀ (X Y : (x : M) → TangentSpace I x), ContMDiff I (ModelWithCorners.tangent I) ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : M => Bundle.TotalSpace.mk' E x (X x)) → ContMDiff I (ModelWithCorners.tangent I) ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : M => Bundle.TotalSpace.mk' E x (Y x)) → ∀ (x : M), g.inner x (LeanEval.Geometry.SphereTheorem.curv cov' X Y Y x) (X x) = κ x * (g.inner x (X x) (X x) * g.inner x (Y x) (Y x) - (g.inner x (X x) (Y x)) ^ 2))import ChallengeDeps
open LeanEval.Geometry.SphereTheorem
open scoped Manifold ContDiff Bundle Topology
open Bundle ContDiff Set VectorField CovariantDerivative Metric
variable
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] [CompleteSpace E]
{H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
{M : Type*} [TopologicalSpace M] [ChartedSpace H M]
[IsManifold I ∞ M]
[RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
[IsContMDiffRiemannianBundle I ∞ E (fun (x : M) ↦ TangentSpace I x)]
theorem differentiable_sphere_theorem [I.Boundaryless] [T2Space M] [CompactSpace M] [SimplyConnectedSpace M]
(hdim : 2 ≤ Module.finrank ℝ E)
(cov : CovariantDerivative I E (TangentSpace I (M := M)))
[ContMDiffCovariantDerivative cov ∞]
(_htor : cov.torsion = 0) (_hmet : IsMetricCompatible cov)
(_hpinch : QuarterPinched cov) :
Nonempty
(M ≃ₘ⟮I, 𝓡 (Module.finrank ℝ E)⟯
(sphere (0 : EuclideanSpace ℝ (Fin (Module.finrank ℝ E + 1))) 1)) := by
sorry
LOT checks the root with the unmodified official pipeline from scratch, as Lean-Eval does; this is that check, alone on the same isolated cores. No what-if with LOT’s optimizations was run for this problem: Its root statement is written inside a block of shared variables and uses scoped manifold notation, so it cannot be restated as one self-contained line..LOT 对根总是用未改动的官方流程从头检查，与 Lean-Eval 一致；这里就是这次检查，同样在独占锁定的核上单独运行。这道题没有做打开 LOT 优化的假设对比：它的根命题写在一组共享变量声明之中，并使用了局部作用域的流形记号，无法改写成一行自包含的命题。。
| Configuration配置 | Wall clock (min)用时（分钟） | CPU-hours used实际 CPU 小时 |
|---|---|---|
| Lean's original pipelineLean 原始流程 | 75.5 | 10.014 |
| LOT’s infrastructure (all six optimizations)LOT 基础设施（6 项优化全开） | 6.5 | 0.338 |
| Optimizations of the previous release, levels side by side (2 workers)上一版优化，各层并排检查（2 个 worker） | 13.1 | 0.775 |
| As it ran in the proved tree (that day’s pipeline, queueing included)证明树当时实际用时（当时的流程，含排队） | 101.9 | – |
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。