Scaling with proof size and baseline cost: method

Question

Do larger proofs, or more expensive original checks, get larger speedups from the LOT optimizations, and what explains the differences between problems? The analysis relates the measured speedup of each problem to (i) the cost of its original check and (ii) static properties of its proof, and then explains the pattern with the measured phase times.

Data

• Timing: the re-measurement campaign of the appendix (section B.1), read when the page is generated. For each problem and scope: the original-pipeline time, the LOT time and the speedup = original ÷ LOT, computed from the unrounded seconds. Only runs marked final are used; a whole tree is used only when both of its sides are final, and an empty cell means “not final yet”. A value that contains an estimated part (measured up to the 12 h cap plus an estimate of the rest, or an estimate only) is marked *, and so is its speedup; a lower bound is marked ≥ and its speedup is a lower bound too.
• Proof properties (groups A and B): static counts of the same proof version as the timing, the tree’s final root commit; the analysis stops if a root commit differs from the one the timing runs checked.
• Phase times and ledger counts (group C, explanation only): each timed run’s log split into phases (process samples and the comparator’s timing lines; a run stopped at the cap is split at its sampled stage boundaries), and the LOT comparator’s counts of constants checked and skipped.

Scopes: root = the check of the final root commit; chain = the problem’s dependency chain of B.1 (original: one check per non-root level; LOT: one chain check); whole tree = the replay of every trusted check of the tree in its own order (original: each check from scratch; LOT: with the ledger and build cache learned along the replay).

Metric rules

Groups A and B are independent properties of the proof (static, the same proof version); S describes the timed chain scope rather than the whole proof; group C describes the workload and the mechanism (from the measured runs or the tree’s history) and is used for explanation only, not as a predictor. No Lean, Lake or checker was run to count them: sources and existing build artifacts were parsed.

• A1 proof modules — Modules in the import closure of the final root obligation’s module that this proof generated (obligation modules and the tree’s own library modules). Excluded: Lean core (Init, Std, Lean, Lake), Mathlib and its dependencies, shared libraries (lean-pool; for Kakeya 4D also the WangZahlLot package), the problem harness, the unchanged scaffold and the seed modules; the excluded modules of each problem are listed below.
• A1 seed modules — Earlier work on the same problem that was added before the run and never changed; not counted in A1–A4 (listed with the excluded modules).
• A2 declarations — User-written declaration commands in the A1 modules, counted from the source: theorem/lemma, def/abbrev/opaque/irreducible_def, instance, structure/class/inductive, axiom, and each name of an alias; not counted: example, attribute, notation/macro/syntax commands and compiler-generated constants.
• A3 lines of Lean — Physical lines of the A1 modules, comments and blank lines included.
• A4 closure constants — The kernel-check closure of the final root: the constants the root check exports and checks, all libraries included, of the kinds the LOT ledger tracks (definitions, theorems, opaques).
• A4 proof constants and proof share — The closure constants declared in the A1 modules; proof share = proof constants ÷ closure constants.
• B5 final sub-theorems — Obligations (root excluded) whose own module is in the import closure of the final root, i.e. whose statement the final proof uses. An accepted obligation of which the final proof imports only helper modules, not the statement, is not counted.
• B5 whole-tree obligations — All obligations the tree ever created (root excluded), superseded and refuted ones included.
• B6 leaves — Leaves of the final proof tree, in which each final sub-theorem hangs under its nearest recorded ancestor that is itself final: final sub-theorems with no final child.
• B7 decomposition depth — Depth of the final proof tree: the largest number of non-root levels from the root to a leaf.
• B7 dependency depth — Depth of the final sub-theorems’ dependency graph: the longest chain root → o₁ → … → oₖ in which each obligation’s own module imports (directly or through helper or library modules) the next one’s own module; edges include sibling and cross dependencies.
• B7 import depth (aux.) — Auxiliary: the longest path in the obligation-level import graph, in which any module an obligation owns (helper modules included) importing any module of another obligation is an edge.
• B7 chain levels — The non-root levels of the dependency chain timed in B.1 (the final root is not counted); † in Table B.3.2 marks a chain whose levels lie on a superseded branch, outside the final proof.
• B8 mean and max branching — Final children per internal node of the final proof tree (root included): mean and maximum.
• S chain-scope modules (aux.) — Chain only: proof modules in the import closure of each chain level, at the commit checked for that level, summed over the levels; a property of the timed chain, not of the whole proof.
• C9 planned checks — Trusted checks in the whole-tree replay plan (original pipeline); LOT runs fewer of them because it merges each closing cascade into one chain check; checks per final obligation = planned checks ÷ final obligations (root included; checks on obligations that were later superseded count too).
• C9 failed checks — Share of the planned checks whose verdict in the tree’s own run was a rejection (the tree’s check time limit included).
• C10 phase shares — The original pipeline’s time by phase: setup/other, build, export & prep and kernel, in % of the scope’s timed runs (root, chain, whole tree); for a run stopped at the 12 h cap, of its measured part.
• C11 ledger skip share — Constants skipped ÷ (checked + skipped) in the LOT runs; root and chain from the run’s ledger counts, whole tree summed over all LOT checks.
• C12 mean time per check — The scope’s original time ÷ its checks (root: one check; chain: its levels; whole tree: the checks of the replay plan); seconds in summary.csv, minutes in Table B.3.3.

Modules excluded from A1–A4, per problem (number of modules in the final root’s import closure):

Predictors

17 predictors: the scope’s original time (the baseline cost), groups A and B, and one auxiliary scope descriptor (S, chain only).

The original time and the speedup share the numerator (speedup = original ÷ LOT), so part of their correlation is built in. The analysis therefore also reports how much the LOT time itself varies (ranges, the log–log slope of the speedup on the original time).

Variants

1. Measured only (primary): problems whose pair contains no estimated part.
2. Including estimates: every final pair; lower bounds enter at their bound.
3. and 4. The same two without Hilbert–Smith (304), the largest baseline in every scope.

Statistics

• Spearman ρ with average ranks for ties, per scope × variant × predictor, from the unrounded speedups; computed only for n ≥ 4. Two speedups that differ only after the first decimal are still ordered by their unrounded values; the analysis text names such near ties.
• Two-sided p from the exact permutation distribution: all n! orderings of the speedups (n ≤ 9). The smallest attainable p is 2/n! (0.083 at n = 4, 0.017 at n = 5).
• 95% bootstrap percentile interval for n ≥ 5, resampling the problems with replacement, from the exact bootstrap distribution for n ≤ 10: all n^n equally likely resamples, enumerated as the distinct multisets of problems weighted by their multiplicity (387,420,489 resamples as 24,310 multisets at n = 9), so the interval has no Monte Carlo error; for larger n (not reached here) 20,000 Monte Carlo resamples with a seed derived from the data. Resamples in which either variable is constant are dropped. When every resample gives the same ρ (ranks that agree exactly), the interval is degenerate and is not reported.
• Benjamini–Hochberg q within each scope × variant over the predictors that apply to the scope (16 at the root, 17 along the chain, 16 over the whole tree); the p-values themselves are unadjusted.
• Reading rule (the verdict column of correlations.csv, filled for the primary variant): supported when the primary ρ > 0 with p < 0.05 and ρ stays positive without Hilbert–Smith (when that variant has a ρ); otherwise negative when ρ < 0 with p < 0.05; otherwise suggestive when ρ ≥ 0.5; otherwise not supported; not testable when the primary variant has fewer than four pairs (no ρ). The analysis text uses the same rule and states results of the other variants with their variant named.
• A value that contains an estimated part is marked * in the text, and so is a ρ whose test includes such a value.
• Descriptive: ranges and fold changes of the original and LOT times, the log–log least-squares slope b of the speedup on the original time (speedup ∝ original^b, LOT ∝ original^(1−b)), and Spearman ρ of the proof-size counts among themselves (collinearity).

Mechanism view

Every timed run of a scope is split into four phases that tile its wall time: setup/other (container setup, teardown, unattributed), build (Lake builds inside the check, plus LOT’s timed gate builds and cache builds), export & prep (exporting the challenge and the solution, the comparator’s parse before the kernels and, in LOT, the ledger digests), kernel (nanoda and the Lean kernel replay; concurrent in LOT, so the phase is their wall-clock span). Per problem the figure shows the original time by phase (shares) with its total, the LOT time by phase (seconds for root and chain, hours for the whole tree; the original and LOT totals are those of Table B.3.1, so their ratio is the speedup), the speedup and the LOT ledger skip share (constants skipped ÷ closure constants; for the whole tree summed over all LOT checks). Rows are sorted by original time. For a run stopped at the 12 h cap the phases are split from its measured part (marked †) and the total includes the estimated rest. A LOT bar longer than its axis is cut at the edge and its label ends with →. Per-phase ratios (original ÷ LOT) in the text use fully measured pairs only. The mean time per check in the text is each side’s total ÷ its own number of checks (LOT runs fewer checks than the plan because it merges each closing cascade into one chain check), so its ratio is not the speedup.

Figures

• ρ matrix: rows = predictors, columns = scopes, one panel per variant; diverging blue (positive) / red (negative) with a neutral midpoint; • = exact p < 0.05 (unadjusted); blank = n < 4 or not applicable.
• Scatter: speedup against original time, kernel-check closure size (A4) and lines of Lean (A3), per scope; log axes; filled = measured, hollow = contains an estimate, arrow = lower bound; dashed line = the speedup if the LOT time were fixed at the scope’s median (root and chain).
• Mechanism: the view above.

Each figure is available as SVG (light and dark renders in one file; the visible one follows the reader’s color scheme), a light PDF and a dark PDF; the text in these files is English. The phase colors follow the main page (build blue, export purple, kernel green; one green for the kernel phase of both pipelines), with the blue darker and the purple lighter so that the two stay apart under color-vision deficiency. They were checked with a palette validator (all pairs, Machado 2009 color-vision deficiency simulation): build, export & prep and kernel pass every check in both modes (worst CVD ΔE 12.5 light / 12.9 dark, target ≥ 8; worst normal-vision ΔE 18.7 / 18.4, floor 15); the neutral setup/other gray sits next to build only (CVD ΔE 26.9 / 15.8). The light green of the kernel is below 3:1 contrast on white, so every bar segment is also identified by the legend and the CSV tables.

Files

summary.csv (one row per problem: groups A, B and C9, the timing pairs with their flags, the original-pipeline phase shares, the LOT ledger skip shares and the mean original time per check), correlations.csv (every test: scope, variant, predictor, n, the problems used, ρ, p, q, the bootstrap interval and how it was computed, and for the primary variant the verdict of the reading rule above), the figures, and this file. The two CSV files are UTF-8 with a byte order mark, so that spreadsheet programs read ≥, –, ∞ and α correctly.

Limits

Small n (9 roots, fewer measured chains and whole trees), coarse exact p-values, wide bootstrap intervals; strongly collinear size metrics; the built-in coupling of original time and speedup; estimated values only in the variants that include them. Statements about mechanisms rest on the phase split and the spread of the LOT times, not on the correlations alone.

加速与证明规模、基线代价的关系：方法

问题

更大的证明、或更贵的原始检查，是否从 LOT 优化中得到更大的加速？各题之间的差异由什么解释？本分析把每题实测的加速比与 （i）原始检查的代价、（ii）证明的静态属性联系起来，再用实测的阶段时间解释其规律。

数据

• 计时：附录的统一重测（B.1 节），在生成页面时读取。每题每个范围给出原始流程时间、LOT 时间和加速比 = 原始 ÷ LOT， 用未取整的秒数计算。只用已定稿的运行；全树只在两侧都定稿时使用，空格表示“尚未定稿”。含估算部分的值（实测到 12 h 上限 加其余部分的估算，或纯估算）标 *，其加速比也标 *；下界标 ≥，其加速比也是下界。
• 证明属性（A、B 组）：与计时同一证明版本（树的最终根提交）的静态计数；若某题根提交与计时运行检查的不一致，分析停止。
• 阶段时间与账本计数（C 组，仅用于解释）：每次计时运行的日志切分成阶段（进程采样和比较器的计时行；在上限处停止的运行按 采样到的阶段边界切分），以及 LOT 比较器给出的检查/跳过常量数。

范围：根 = 最终根提交的检查；链 = B.1 中该题的依赖链（原始：每个非根层一次检查；LOT：一次链检查）；全树 = 按树自己的顺序重放全部可信检查（原始：每次从头检查；LOT：账本与构建缓存在重放中逐步积累）。

指标规则

A、B 组是证明的独立属性（静态，同一证明版本）；S 描述计时的链范围，而不是整个证明；C 组描述工作量与机制（来自实测运行或 树的历史），只用于解释，不作为预测量。计数时没有运行 Lean、Lake 或检查器：解析的是源码和已有的构建产物。

• A1 证明模块数 —— 最终根义务模块的传递 import 闭包中由本证明生成的模块（义务模块与树内自有的库模块）。排除 Lean 核心（Init、Std、Lean、Lake）、Mathlib 及其依赖、共享库（lean-pool；Kakeya 4D 另有 WangZahlLot 包）、题目框架、未改动的模板和种子模块；各题排除的模块见下表。
• A1 种子模块 —— 开跑前加入、之后未改动的同题旧工作；不计入 A1–A4（列在排除的模块中）。
• A2 声明数 —— A1 模块中用户书写的声明命令，按源码计数：theorem/lemma、def/abbrev/opaque/irreducible_def、instance、structure/class/inductive、axiom，以及 alias 的每个名字；不计 example、attribute、notation/macro/syntax 命令和编译器自动生成的常量。
• A3 Lean 行数 —— A1 模块的物理行数，含注释和空行。
• A4 闭包常量数 —— 最终根的内核检查闭包：根检查导出并检查的常量（含全部库），按 LOT 账本统计的种类（定义、定理、opaque）计。
• A4 本证明常量数与本证明占比 —— 闭包中由 A1 模块声明的常量；本证明占比 = 本证明常量数 ÷ 闭包常量数。
• B5 最终子定理数 —— 自身模块在最终根 import 闭包中的义务（不含根），即最终证明用到其命题的义务。最终证明只导入了其辅助模块、没有用到其命题的已接受义务不计入。
• B5 全树义务数 —— 树中创建过的全部义务（不含根），含已被取代和被否定的。
• B6 叶数 —— 最终证明树的叶（每个最终子定理挂在记录中离它最近、且本身也属于最终证明的祖先下）：没有最终子节点的最终子定理。
• B7 分解深度 —— 最终证明树的深度：从根到叶的最大非根层数。
• B7 依赖深度 —— 最终子定理依赖图的深度：最长的依赖链 根 → o₁ → … → oₖ，其中每个义务的自身模块（直接或经辅助/库模块）导入下一个义务的自身模块；边包括兄弟依赖和交叉依赖。
• B7 导入深度（辅助） —— 辅助口径：义务级 import 图的最长路径，义务拥有的任一模块（含辅助模块）导入另一义务的任一模块即算一条边。
• B7 链层数 —— B.1 中计时的依赖链的非根层数（最终根不计入）；表 B.3.2 中的 † 表示该链的各层位于已被取代的分支上，不属于最终证明。
• B8 平均与最大分支数 —— 最终证明树中每个内部节点（含根）的最终子节点数：均值与最大值。
• S 链范围模块数（辅助） —— 仅用于链：链的每一层在其被检查的提交处 import 闭包中的证明模块数，对各层求和；描述的是计时的链，而不是整个证明。
• C9 计划检查数 —— 全树重放计划中的可信检查数（原始流程）；LOT 把每个收尾级联合并为一次链检查，所以运行的检查更少；每个最终义务的检查数 = 计划检查数 ÷ 最终义务数（含根；花在后来被取代的义务上的检查也计入）。
• C9 失败检查 —— 在树自身的运行中判定为拒绝（含该树的检查时限）的计划检查所占比例。
• C10 阶段占比 —— 原始流程的时间按阶段的占比：启动/其他、构建、导出与准备、内核，占该范围计时运行的百分比（根、链、全树）；在 12 h 上限处停止的运行取其实测部分。
• C11 账本跳过比例 —— LOT 运行中跳过的常量 ÷（检查的 + 跳过的）；根和链取该次运行的账本计数，全树为全部 LOT 检查之和。
• C12 每次检查的平均时间 —— 该范围的原始时间 ÷ 其检查数（根：一次；链：层数；全树：重放计划中的检查数）；summary.csv 中单位为秒，表 B.3.3 中为分钟。

各题从 A1–A4 中排除的模块（最终根 import 闭包中的模块数）：

预测量

共 17 个：该范围的原始时间（基线代价）、A 组与 B 组，以及一个辅助的范围描述量（S，仅用于链）。

原始时间与加速比共用分子（加速比 = 原始 ÷ LOT），二者的相关有一部分是结构性的。因此分析同时报告 LOT 时间本身的变化幅度 （范围、加速比对原始时间的双对数斜率）。

变体

1. 仅实测（主口径）：成对值不含估算部分的题目。
2. 含估算：全部已定稿的成对值；下界按其界值计入。
3. 和 4. 上述两种去掉 Hilbert–Smith (304)（每个范围中基线最大的一题）。

统计方法

• Spearman ρ，并列值取平均秩，按范围 × 变体 × 预测量计算，使用未取整的加速比；仅在 n ≥ 4 时计算。两个只在一位小数之后 才不同的加速比仍按未取整值排序；分析文字会点出这样的近似并列。
• 双侧 p 取精确置换分布：加速比的全部 n! 种排列（n ≤ 9）。可达到的最小 p 为 2/n!（n = 4 时 0.083，n = 5 时 0.017）。
• n ≥ 5 时给 95% bootstrap 百分位区间，对题目有放回抽样。n ≤ 10 时用精确 bootstrap 分布：全部 n^n 种等可能的抽样， 按不同的题目多重集枚举并以其重数加权（n = 9 时 387,420,489 种抽样合为 24,310 个多重集），区间没有蒙特卡洛误差；n 更大时 （本分析未出现）用 20,000 次蒙特卡洛抽样，种子由数据决定。任一变量为常数的抽样丢弃。若每次抽样的 ρ 都相同（秩完全一致）， 区间是退化的，不予报告。
• 在每个范围 × 变体内，对适用于该范围的预测量做 Benjamini–Hochberg 校正，给出 q 值（根 16 个、链 17 个、全树 16 个）；p 值本身未校正。
• 判读规则（correlations.csv 的 verdict 列，只对主口径填写）：主口径 ρ > 0 且 p < 0.05、去掉 Hilbert–Smith 后 ρ 仍为正 （该变体有 ρ 时），记为 supported（支持）；否则若 ρ < 0 且 p < 0.05，记为 negative（负相关）；否则若 ρ ≥ 0.5，记为 suggestive（有迹象）；其余记为 not supported（不支持）；主口径不足四对（没有 ρ）记为 not testable（无法检验）。 分析文字使用同一规则，其他变体的结果注明变体后给出。
• 含估算部分的值在文字中标 *；检验中含这样的值的 ρ 也标 *。
• 描述量：原始与 LOT 时间的范围与倍数、加速比对原始时间的双对数最小二乘斜率 b（加速比 ∝ 原始^b，LOT ∝ 原始^(1−b)），以及 证明规模计数之间的 Spearman ρ（共线性）。

机制视图

每个范围的每次计时运行切成四个阶段，正好铺满其墙钟时间：启动/其他（容器启动、收尾、未归属部分）、构建（检查内的 Lake 构建，以及 LOT 计时的门构建与缓存构建）、导出与准备（导出题面与解答、比较器在内核之前的解析，LOT 中还有账本摘要）、 内核（nanoda 与 Lean 内核重放；LOT 中二者并发，取其墙钟跨度）。图中每题给出：原始时间的各阶段占比及总时间、LOT 时间的 各阶段时长（根和链以秒计，全树以小时计；原始与 LOT 的总时间即表 B.3.1 中的值，二者之比就是加速比）、加速比、LOT 账本跳过比例 （跳过的常量 ÷ 闭包常量；全树为全部 LOT 检查之和）。各行按原始时间排序。在 12 h 上限处停止的运行，阶段由实测部分切分（标 †）， 总时间含其余部分的估算。超出坐标轴的 LOT 条形在边缘截断，标签以 → 结尾。文字中的分阶段比值（原始 ÷ LOT）只用两侧都完整实测的 成对值。文字中每次检查的平均时间是各自的总时间 ÷ 各自的检查数（LOT 把每个收尾级联合并为一次链检查，运行的检查比计划少）， 所以二者之比不是加速比。

图

• ρ 矩阵：行 = 预测量，列 = 范围，每个变体一个面板；发散色，蓝为正、红为负、中点中性；• = 精确 p < 0.05（未校正）；空白 = n < 4 或不适用。
• 散点图：各范围中加速比对原始时间、内核检查闭包规模（A4）和 Lean 行数（A3）；对数坐标；实心 = 实测，空心 = 含估算，箭头 = 下界；虚线 = 若 LOT 时间固定为该范围中位数时的加速比（根与链）。
• 机制图：上述机制视图。

每张图提供 SVG（浅色与深色两份渲染在同一文件中，按读者的配色方案显示其一）、浅色 PDF 和深色 PDF；这些文件中的图内文字为英文。 阶段配色沿用主页面（构建蓝、导出紫、内核绿；两条流程的内核阶段用同一种绿），蓝色加深、紫色调浅，使二者在色觉缺陷下仍可区分。 配色用调色板校验器检查过（全部配对，Machado 2009 色觉缺陷模拟）：构建、导出与准备、内核三色在两种模式下通过全部检查（色觉缺陷模拟下最小 ΔE 浅色 12.5 / 深色 12.9，目标 ≥ 8；正常视觉最小 ΔE 18.7 / 18.4，下限 15）；中性灰的启动/其他只与构建相邻（色觉缺陷 ΔE 26.9 / 15.8）。内核的浅绿色在白底上对比度低于 3:1，所以每个条形段也可由图例和 CSV 表识别。

文件

summary.csv（每题一行：A、B 组与 C9、带标记的计时对、原始流程各阶段占比、LOT 账本跳过比例、每次检查的原始平均时间）、 correlations.csv（每个检验：范围、变体、预测量、n、所用题目、ρ、p、q、bootstrap 区间及其算法，主口径另有按上述判读规则得出的 verdict）、各图，以及本文件。两个 CSV 文件为带字节顺序标记（BOM）的 UTF-8，电子表格程序可以正确显示 ≥、–、∞ 和 α。

局限

样本小（9 个根，实测的链和全树更少），精确 p 值粒度粗，bootstrap 区间宽；规模指标之间高度共线；原始时间与加速比之间有结构性 耦合；估算值只进入含估算的变体。关于机制的结论依据阶段切分与 LOT 时间的离散程度，而不仅是相关系数。