LOT · Lean Check Pipeline · Appendix附录

Appendix: measurements and model inputs附录：实测数据与模型输入

Nine proved problems, checked with Lean's original pipeline (baseline) and with LOT's (full: all five optimizations), at three levels: one node, one dependency chain, the whole tree. Every number says whether it was measured (M) or estimated (E); uniform assumptions are marked U. The raw data is downloadable at the end.九道已证题目，分别用 Lean 原始流程（baseline）和 LOT 流程（完整版：五项优化全开）检查，分单节点、依赖链、全树三个层次。每个数字都标明是实测（M）还是估算（E）；统一假设标为 U。原始数据在页末下载。

ASetup and what is counted环境与计时口径

Host主机	AMD EPYC 7B13, 224 CPUs (112 physical cores, 2 threads each个物理核，每核 2 线程), 882 GiB RAM, Linux 6.8
One check单次检查	alone on 8 whole physical cores (16 CPUs) and 64 GiB of one NUMA node (304 and 074: 128 GiB), in an exclusive cgroup-v2 partition locked for the run, so no other process could use those CPUs; container network none, image python:3.12-bookworm, LEAN_NUM_THREADS 16; the parallel replay uses 12 threads独占 8 个完整物理核（16 个 CPU）和一个 NUMA 节点上的 64 GiB（304、074 为 128 GiB），运行期间锁定为专用 cgroup-v2 分区，其他进程无法使用这些 CPU；容器无网络，镜像 python:3.12-bookworm，LEAN_NUM_THREADS 16；并行重放用 12 线程
Whole tree全树	two such lanes (16 cores in all); a check starts when a lane is free and the check whose landing made its library commit has finished (list scheduling in the tree's own order)两条这样的通道（共 16 核）；某个检查在有空闲通道、且产生其库提交的那次落地检查已完成时开始（按树自己的顺序做列表调度）
Software软件	Lean 4 v4.35.0-rc3 · Mathlib 5e0c4e5 · lean-pool e9d53e9 · 074 also the WangZahlLot package074 另加 WangZahlLot 包 · lean4export 71043e7c · baseline: the official comparator with the toolchain's nanoda 0.4.17, trusted checker check.sh v12 with LOT_LEAN_REPLAY=offbaseline：官方 comparator 与工具链自带 nanoda 0.4.17，可信检查脚本 check.sh v12，LOT_LEAN_REPLAY=off · full: comparator fork (parallel replay, ledger) 82325f10 with nanoda-t 1b6e35f5 (nanoda 0.4.6-beta + ledger patches), check.sh v12 per node, check-v13 for one check per chain (LOT archive 80fddd7), check-v15 for the fast root (LOT 4.5)完整版：comparator 分支（并行重放、账本）82325f10 与 nanoda-t 1b6e35f5（nanoda 0.4.6-beta + 账本补丁），单节点用 check.sh v12，整链一检用 check-v13（LOT archive 80fddd7），快速根用 check-v15（LOT 4.5）
Queue and scheduler排队与调度	not in the measured numbers: durations are measured inside the container (queue waits, scheduler ticks, docker start and teardown left out). The model adds them (section D).不计入实测数字：时长在容器内测量（排队、调度间隔、docker 启停都不含）。模型里另外加上（D 节）。
Cache preparation缓存准备	single node and chain: not counted (the library's first full build is a premise of build reuse; its time is listed per problem). Whole tree: counted (the first bar of the full replay is that build). LOT's per-check gate builds are counted everywhere.单节点与链：不计入（库的第一次完整编译是编译复用的前提，每题单列其时间）。全树：计入（完整版回放的第一段就是这次编译）。LOT 每次检查的 gate build 在各层次都计入。
Root check根检查	not in single node or chain. In the whole tree: baseline = the official root check; full = LOT 4.5's fast root with its gate build.单节点和链都不含。全树里：baseline 是官方根检查；完整版是 LOT 4.5 的快速根加它的 gate build。
Final official check最终官方终检	not counted anywhere. Since LOT 4.5 it runs once after the proof, outside the tree's time; the whole-tree replays measured it (listed per tree).都不计入。从 LOT 4.5 起它在证完后单独跑一次，不算树的时间；全树回放测了它（各树单列）。
Runs cut at 12 h12 h 截断	measured up to the cut, the rest estimated; each method is stated with the problem (M+E).截断前实测，其余估算；方法写在各题下（M+E）。

BBaseline vs full at three levels三个层次的 baseline 与完整版

B1 · Single nodeB1 · 单节点

Problem题目	nodes (the chain’s levels)节点数（链上各层）	baseline, meanbaseline 平均	full without coalescing, mean完整版（不合并）平均	×
Direct summand	4	19.3 min M	4.3 min M	4.5×
Bochner–Riesz 3D (078)	10	26.4 min M	4.9 min M	5.4×
Hilbert–Smith (304)	12	11.68 h M (1 of 12 levels)	1.30 h E	9.0×
∞-harmonic C^1,α (377)	2	6.0 min M	3.0 min M	2.0×
Shafarevich	5	18.8 min M	4.6 min M	4.1×
Quadrisecant	4	3.2 min M	2.2 min M	1.4×
Sphere theorem	3	25.2 min M	6.2 min M	4.1×
Kakeya 3D (Wang–Zahl)	3	4.1 min M	2.3 min M	1.8×
Kakeya 4D (074)	5	3.40 h M (3 of 5 levels)	21.7 min E	9.4×

B2 · Dependency chain (root excluded)B2 · 依赖链（不含根）

Problem题目	length链长	baseline: level by levelbaseline：逐层	full: one check完整版：一次检查	×	root, official (for reference)根，官方（参考）	root, LOT 4.5 fast (for reference)根，LOT 4.5 快速（参考）
Direct summand	4	1.29 h M	6.0 min M	13.0×	37.3 min M	8.8 min M
Bochner–Riesz 3D (078)	10	4.40 h M	7.8 min M	33.7×	1.45 h M	25.1 min M
Hilbert–Smith (304)	12	133.56 h M+E	1.30 h M	102.9×	14.64 h M+E	13.1 min M
∞-harmonic C^1,α (377)	2	12.0 min M	4.1 min M	2.9×	12.3 min M	5.5 min M
Shafarevich	5	1.57 h M	6.5 min M	14.4×	41.5 min M	23.9 min M
Quadrisecant	4	12.7 min M	3.3 min M	3.8×	5.6 min M	2.3 min M
Sphere theorem	3	1.26 h M	6.5 min M	11.6×	46.7 min M	13.0 min M
Kakeya 3D (Wang–Zahl)	3	12.3 min M	2.8 min M	4.4×	1.42 h M	1.16 h M
Kakeya 4D (074)	5	15.88 h M+E	21.7 min E	44.0×	4.46 h M	– –

B3 · Whole tree (root included; 2 lanes × 8 cores)B3 · 全树（含根；2 条通道 × 8 核）

Problem题目	nodes (accepted / all)节点（已接受 / 全部）	depth深度	checks: baseline → full检查次数：baseline → 完整版	baselinebaseline	full完整版	×	final official check (not counted)最终官方终检（不计入）
Direct summand	307 / 514	10	386 → 352	23.51 h E	13.60 h E	1.7×	–
Bochner–Riesz 3D (078)	126 / 214	11	191 → 172	15.34 h M+E	7.07 h M	2.2×	1.23 h M
Hilbert–Smith (304)	164 / 209	13	257 → 226	165.63 h E	67.05 h E low confidence置信度低	2.5×	–
∞-harmonic C^1,α (377)	39 / 48	4	63 → 61	2.63 h M	1.71 h M	1.5×	10.3 min M
Shafarevich	106 / 148	9	180 → 168	51.32 h E	7.40 h E	6.9×	–
Quadrisecant	36 / 47	6	44 → 40	1.25 h M	1.03 h M	1.2×	4.8 min M
Sphere theorem	111 / 167	8	143 → 133	30.36 h E	7.69 h E	4.0×	–
Kakeya 3D (Wang–Zahl)	134 / 234	10	193 → 174	45.14 h E	5.76 h E	7.8×	–
Kakeya 4D (074)	241 / 296	12	358 → 319	150.85 h E	27.82 h E low confidence置信度低	5.4×	–

Single node: the chain's own levels, each checked on its own (same nodes for both columns). Full = LOT's gate build + check.sh with build reuse, parallel replay and the ledger learned from the levels below; no coalescing. Chain: every non-root level of the chain accepted; full = one check of the whole chain. Whole tree: every check that reached check.sh in the tree's history, the root included. 304 and 074: the single-node full value is the chain's one check (see each problem below); 074's full side is estimated until the nanoda-t fix is measured.单节点：链自己的各层，逐层单独检查（两列是同一批节点）。完整版 = LOT 的 gate build + check.sh（编译复用、并行重放、账本学自下层），不合并。链：链上所有非根层通过；完整版是整链一次检查。全树：树历史上到达 check.sh 的全部检查，含根。304 和 074 的单节点完整版取整链一次检查的值（见下面各题）；074 的完整版在 nanoda-t 修复实测前为估算。

CHow the six unmeasured trees are estimated六棵未实测的树如何估算

Only three trees were replayed whole. For the other six, the estimator takes the tree's own check plan (which checks reached check.sh, which check each one waited for, which re-checks close together) and places it on the same two lanes. Baseline: each check takes its historical seconds in the tree times the chain example's measured baseline/historical ratio, and the root its measured official check. Full: the library's cache build first, then each check takes the measured single-node full mean, each closing chain the measured one check, and the root the measured fast root. 304 and 074 have no single-node full measurement, so each check takes its historical seconds (low confidence).只有三棵树做了完整回放。其余六棵，估算器取树自己的检查计划（哪些检查到达了 check.sh、各自等哪个检查、哪些复查一起收口），放在同样的两条通道上排。Baseline：每个检查取它在树里的历史秒数，乘以该题链示例实测的 baseline/历史比值；根取实测的官方根检查。完整版：先做库的缓存编译，然后每个检查取实测的单节点完整版平均值，每条收口链取实测的整链一次检查，根取实测的快速根。304 和 074 没有单节点完整版实测，每个检查取历史秒数（置信度低）。

On the three measured trees, the estimator is off by 10–48% (baseline) and 1–24% (full):在三棵实测树上，估算器的误差为 10–48%（baseline）和 1–24%（完整版）：

Tree树	baseline measuredbaseline 实测	estimator估算器	error误差	full measured完整版实测	estimator估算器	error误差
Bochner–Riesz 3D (078)	15.34 h	22.76 h	+48%	7.07 h	8.74 h	+24%
∞-harmonic C^1,α (377)	2.63 h	2.37 h	-10%	1.71 h	1.74 h	+1%
Quadrisecant	1.25 h	1.06 h	-15%	1.03 h	51.2 min	-17%

DInputs of the six-step model, per problem六档模型的逐题输入

Steps, each keeping the ones before: baseline → + scheduling and infrastructure → + chain / subtree coalescing → + build reuse → + verified-constant ledger → + parallel kernel replay. Seconds; means over the chain's levels. Hover a cell for its source.各档依次叠加：baseline → + 调度与基础设施 → + 链／子树合并 → + 编译复用 → + 已验证常量账本 → + 并行内核重放。单位为秒，取链上各层的平均值。鼠标停在单元格上可看来源。

Queue before / after the scheduling work调度优化前 / 后的排队 U	1,080 s / 8 s: median wait before a check started, 16–20 min before and about 8 s after (Gorenstein–Walter tree, Oct 15, 2026)1,080 s / 8 s：检查开跑前等待的中位数，优化前 16–20 min，优化后约 8 s（Gorenstein–Walter 树，2026-10-15）
Gap between levels层与层之间的调度间隔 U	360 s: closing a chain level by level adds 0.05–0.2 h per level in the production trees (model 0.1 h); gone once the chain is one check360 s：生产树里逐层收链每层多 0.05–0.2 h（模型取 0.1 h）；整链一检后不再有
Checks after coalescing合并后的检查次数	chain: 1. Whole tree: the tree table above (checks baseline → full)链：1。全树：见上表（检查次数 baseline → 完整版）
Ledger: kernel time left账本：剩余内核时间 U	0.15 for every problem: with serial kernels the kernel phase was 85% shorter with the ledger (93.1% of constants skipped, 7/7 spot checks identical). The per-problem measurements below are with the parallel replay already on, where the kernel phase is short, so they do not isolate the ledger.各题统一取 0.15：串行内核时账本让内核阶段缩短 85%（跳过 93.1% 的常量，抽查 7/7 一致）。下面的逐题实测是在并行重放已开时测的，那时内核阶段本来就短，不能单独说明账本的作用。

Input (s)输入（秒）	Direct summand	Bochner–Riesz 3D (078)	Hilbert–Smith (304)	∞-harmonic C^1,α (377)	Shafarevich	Quadrisecant	Sphere theorem	Kakeya 3D (Wang–Zahl)	Kakeya 4D (074)
LL	4 M	10 M	12 M	2 M	5 M	4 M	3 M	3 M	5 M
setup准备	11 M	22 M	34 M	7 M	9 M	6 M	14 M	6 M	68 M
build from scratch从头编译	616 M	1,241 M	9,339 M	204 M	616 M	91 M	968 M	111 M	9,571 M
build with reuse复用编译	78 M	85 M	217 E	86 M	90 M	67 M	125 M	58 M	275 E
export导出	74 M	72 M	117 M	44 M	120 M	35 M	104 M	41 M	507 M
parse解析	38 M	36 M	63 M	20 M	67 M	14 M	61 M	19 M	298 M
nanoda (serial pipeline)nanoda（串行流程）	43 M	52 M	2,663 M	18 M	60 M	9 M	62 M	14 M	224 M
serial Lean replayLean 串行重放	377 M	161 M	29,819 M	68 M	256 M	35 M	300 M	54 M	1,568 M
parallel kernels (nanoda ‖ Lean)并行双内核（nanoda ‖ Lean）	100 M	90 M	4,289 M	41 M	106 M	19 M	140 M	35 M	420 E
constants left after the ledger账本后剩余常量	0.242 M	0.051 M	–	–	0.056 M	0.115 M	0.004 M	0.045 M	–
kernel wall warm / cold (parallel)内核墙钟热/冷（并行）	0.909 M	1.095 M	–	–	0.841 M	1.467 M	0.688 M	0.790 M	–
one check of the chain整链一次检查	357 M	470 M	4,674 M	248 M	389 M	205 M	389 M	169 M	1,300 E
cache build (not counted)缓存构建（不计入）	967 M	4,219 M	17,043 M	231 M	974 M	110 M	1,536 M	115 M	9,016 M

Two things to know before using these inputs使用这些输入前要注意两点

The ledger also helps the coalesced chain, through the checks done earlier in the tree. In a tree, a chain's one check starts after the tree's other checks (the obligations below it, side children, every earlier proof), so the ledger already holds Mathlib's constants and everything checked before; only the chain's own new proofs are left to the kernels. The reference model below therefore applies the ledger factor to the one check as well. Our measured full numbers are more conservative: each was measured alone, starting from an empty ledger (0 constants skipped), so they leave this gain out.账本对合并后的链同样有收益，来自树里之前做过的检查。在树里，一条链的那次检查是在树的其他检查（它下面的义务、旁支子义务、之前的所有证明）之后才开始的，这时账本里已经有 Mathlib 的常量和之前查过的全部内容，内核只需要查链上新写的证明。所以下面的参考模型对这次检查也乘上账本系数。我们实测的完整版数字更保守：每次都是单独测的，账本从空开始（跳过 0 个常量），没有包含这部分收益。
The per-problem ledger measurements cannot be used as the ledger factor. They were taken with the parallel replay already on, when the kernel phase is short: the warm/cold kernel-wall ratio ranges over 0.69–1.47 (above 1 on some problems, because the warm and cold levels differ in size). The model therefore uses the uniform 0.15 measured with serial kernels.按题实测的账本数据不能直接当账本系数用。这些数据是在并行重放已经打开时测的，那时内核阶段本来就短：热/冷内核墙钟之比在 0.69–1.47 之间（有几题大于 1，因为热层和冷层的规模不同）。所以模型统一使用串行内核下实测的 0.15。

Reference: the main page's model with these inputs (chain level)参考：主页面的模型代入这些输入（链层次）

The model of the main page's section 3 with each problem's means. Queue and gaps included; the measured columns exclude them.主页面第 3 节的模型，代入各题的平均值。含排队和层间间隔；实测列不含。

Step (chain level)档位（链层次）	Direct summand	Bochner–Riesz 3D (078)	Hilbert–Smith (304)	∞-harmonic C^1,α (377)	Shafarevich	Quadrisecant	Sphere theorem	Kakeya 3D (Wang–Zahl)	Kakeya 4D (074)
BaselineBaseline	2.79 h	8.30 h	144.82 h	54.0 min	3.47 h	1.71 h	2.36 h	1.30 h	18.89 h
+ Scheduling and infrastructure+ 调度与基础设施	1.60 h	5.32 h	141.24 h	18.3 min	1.98 h	31.2 min	1.46 h	24.7 min	17.40 h
+ Chain / subtree coalescing+ 链／子树合并	19.5 min	26.5 min	11.68 h	6.1 min	18.9 min	3.3 min	25.3 min	4.2 min	3.40 h
+ Build reuse+ 编译复用	10.5 min	7.3 min	9.14 h	4.2 min	10.2 min	2.9 min	11.2 min	3.3 min	49.1 min
+ Verified-constant ledger+ 已验证常量账本	4.5 min	4.2 min	1.48 h	3.0 min	5.7 min	2.3 min	6.1 min	2.4 min	23.7 min
+ Parallel kernel replay+ 并行内核重放	3.7 min	3.9 min	18.0 min	2.8 min	5.2 min	2.2 min	5.6 min	2.3 min	20.3 min
Model speedup模型加速比	44.7×	126.4×	481.6×	19.0×	40.3×	46.3×	25.5×	34.3×	55.8×
Measured chain: baseline / full实测链：baseline / 完整版	1.29 h / 6.0 min	4.40 h / 7.8 min	133.56 h / 1.30 h	12.0 min / 4.1 min	1.57 h / 6.5 min	12.7 min / 3.3 min	1.26 h / 6.5 min	12.3 min / 2.8 min	15.88 h / –

EPer problem: every measured run逐题：每次实测运行

Direct summand theorem and derived variant (direct_summand)

Tree树: 514 obligations个义务, 307 accepted (live)个已接受（有效）, depth深度 10; checks that reached check.sh到达 check.sh 的检查 386 (294 proof checks次证明检查, 91 re-checks of glue proofs次胶水复查, 1 root次根检查); closing chains收口链 20 (lengths长度 2, 3, 2, 2, 2, 2, 2, 2, 2, 2, 4, 3, 5, 2, 2, 2, 6, 2, 3, 4), 352 checks after coalescing次检查（合并后）; historical check time in the tree树中历史检查时间合计 26.05 h; production生产配置: max_gate_builds 48, check_timeout 10,800 s. DAG + check plan检查计划 (JSON)

Baseline, each level from scratch (official pipeline: check.sh v12, LOT_LEAN_REPLAY=off)Baseline：每层从头检查（官方流程：check.sh v12，LOT_LEAN_REPLAY=off）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
ds-iso-orig-L1	ACCEPT	863.5	10.0	452.3	42.0	22.0	35.0	302.1	359.1	1	–	–
ds-iso-orig-L2	ACCEPT	891.0	10.0	477.3	45.0	25.0	33.0	300.7	358.7	1	–	–
ds-iso-orig-L3	ACCEPT	1,614.6	12.0	937.6	128.0	62.0	45.0	429.9	536.9	1	–	–
ds-iso-orig-L4	ACCEPT	1,270.7	11.0	597.5	82.0	45.0	60.0	475.3	580.3	1	–	–

Full without coalescing, each level (gate build + check.sh v12 seeded, parallel replay, ledger learned from the levels below)完整版不合并，每层（gate build + 播种的 check.sh v12、并行重放、账本学自下层）

run运行	verdict结论	total s总计 s	gate buildgate build	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
ds-iso-side-L1	ACCEPT	193.5	25.3	12.0	39.0	44.0	22.4	48.7	76.1	98.5	12	53,507	0
ds-iso-side-L2	ACCEPT	193.8	25.0	12.0	35.0	46.0	23.7	52.3	77.0	100.7	12	55,536	0
ds-iso-side-L3	ACCEPT	294.8	32.2	14.0	76.0	115.0	56.7	20.7	33.1	89.8	12	12,798	55,513
ds-iso-side-L4	ACCEPT	238.2	29.5	12.0	51.0	84.0	46.8	44.4	36.8	91.2	12	23,472	55,513

Full: one check of the whole chain (check-v13), gate build 1.1 min完整版：整链一次检查（check-v13），gate build 1.1 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
ds-iso-one-1	ACCEPT	289.5	12.0	62.0	80.0	46.5	79.6	89.0	135.5	12	78,988	0

Root, official check (not in the chain or node numbers)根，官方检查（不计入链和节点数字）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
ds-iso-root-orig	ACCEPT	2,238.9	10.0	1,090.9	101.0	60.0	107.0	870.0	1,037.0	1	–	–

Root, LOT 4.5 fast root (check-v15), gate build 3.2 min根，LOT 4.5 快速根（check-v15），gate build 3.2 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
ds-iso-root-fast-1	ACCEPT	335.3	17.0	43.0	112.0	63.2	100.0	74.3	163.2	12	20,041	78,948

Cache build (the library's first build from scratch, a premise of build reuse, not counted)缓存构建（库第一次从头编译，编译复用的前提，不计入）: 16.1 min

Bochner–Riesz Multipliers in Three Dimensions (078)

Whole-tree baseline estimate: 全树 baseline 估算方法：181 checks measured in this tree (79509 s on one lane; their historical 43854 s). The other 10: the closing cascade the chain example measured (6 levels) and the root take the chain example's isolated ORIGINAL times (measured in the chain example (same isolation)); other closing-cascade REGATEs take their historical seconds x 3.15 (the chain example's measured ORIGINAL/historical ratio: the tree's REGATEs were seeded and prewarmed); the rest their historical seconds x 1.81 (this tree's measured ratio); all placed on the same two lanes. The naive estimate (every unmeasured check x 1.81) is in estimate_s_naive

Tree树: 214 obligations个义务, 126 accepted (live)个已接受（有效）, depth深度 11; checks that reached check.sh到达 check.sh 的检查 191 (154 proof checks次证明检查, 36 re-checks of glue proofs次胶水复查, 1 root次根检查); closing chains收口链 4 (lengths长度 2, 4, 7, 10), 172 checks after coalescing次检查（合并后）; historical check time in the tree树中历史检查时间合计 14.87 h; production生产配置: max_gate_builds 32, check_timeout 10,800 s. DAG + check plan检查计划 (JSON)

Baseline, each level from scratch (official pipeline: check.sh v12, LOT_LEAN_REPLAY=off)Baseline：每层从头检查（官方流程：check.sh v12，LOT_LEAN_REPLAY=off）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
br-iso-orig-L1	ACCEPT	1,198.5	23.0	922.2	60.0	31.0	39.0	123.3	193.3	1	–	–
br-iso-orig-L2	ACCEPT	1,260.1	22.0	972.2	62.0	33.0	40.0	130.9	203.9	1	–	–
br-iso-orig-L3	ACCEPT	1,328.6	22.0	1,021.3	70.0	35.0	43.0	137.2	215.3	1	–	–
br-iso-orig-L4	ACCEPT	1,272.5	22.0	978.3	64.0	31.0	41.0	136.2	208.2	1	–	–
br-iso-orig-L5	ACCEPT	1,282.9	22.0	987.3	61.0	31.0	49.0	132.6	212.6	1	–	–
br-iso-orig-L6	ACCEPT	1,361.9	22.0	1,048.3	66.0	31.0	50.0	144.5	225.6	1	–	–
br-iso-orig-L7	ACCEPT	1,450.2	22.0	1,112.4	74.0	33.0	51.0	157.8	241.8	1	–	–
br-iso-orig-L8	ACCEPT	1,551.6	23.0	1,201.4	73.0	33.0	53.0	168.2	254.2	1	–	–
br-iso-orig-L9	ACCEPT	2,396.8	25.0	1,930.8	93.0	49.0	77.0	222.0	348.0	1	–	–
br-iso-orig-L10	ACCEPT	2,746.1	22.0	2,240.1	100.0	49.0	82.0	252.9	384.0	1	–	–

run运行	verdict结论	total s总计 s	gate buildgate build	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
br-iso-side-L1	ACCEPT	238.5	39.3	27.0	53.0	75.0	32.6	50.8	16.6	83.4	12	63,532	0
br-iso-side-L2	ACCEPT	292.9	71.7	30.0	76.0	90.0	45.2	51.6	17.8	96.8	12	66,507	0
br-iso-side-L3	ACCEPT	218.9	22.6	26.0	45.0	69.0	36.6	42.2	8.7	78.9	12	1,830	66,484
br-iso-side-L4	ACCEPT	202.3	22.7	26.0	36.0	64.0	32.8	43.4	8.4	76.2	12	1,842	66,484
br-iso-side-L5	ACCEPT	202.1	22.8	26.0	35.0	65.0	33.6	42.4	8.3	76.1	12	119	68,303
br-iso-side-L6	ACCEPT	317.2	45.7	28.0	59.0	113.0	72.5	44.7	9.2	117.2	12	551	68,303
br-iso-side-L7	ACCEPT	211.1	34.8	26.0	36.0	72.0	33.2	43.9	8.4	77.1	12	34	68,831
br-iso-side-L8	ACCEPT	205.1	77.5	26.0	31.0	67.0	37.5	43.6	9.3	81.1	12	50	68,831
br-iso-side-L9	ACCEPT	285.3	23.3	26.0	39.0	96.0	50.5	73.8	16.8	124.2	12	14,395	68,858
br-iso-side-L10	ACCEPT	370.4	24.3	27.0	51.0	134.0	84.9	73.5	17.8	158.4	12	14,503	68,858

Full: one check of the whole chain (check-v13), gate build 2.0 min完整版：整链一次检查（check-v13），gate build 2.0 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
br-iso-one-1	ACCEPT	351.5	27.0	87.0	102.0	51.8	83.7	28.5	135.5	12	83,370	0

Root, official check (not in the chain or node numbers)根，官方检查（不计入链和节点数字）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
br-iso-root-orig	ACCEPT	5,236.4	28.0	4,561.1	154.0	94.0	87.0	312.2	493.3	1	–	–

Root, LOT 4.5 fast root (check-v15), gate build 17.2 min根，LOT 4.5 快速根（check-v15），gate build 17.2 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
br-iso-root-fast-1	ACCEPT	473.9	42.0	60.0	197.0	113.0	61.9	20.9	174.9	12	9,908	83,338

Cache build (the library's first build from scratch, a premise of build reuse, not counted)缓存构建（库第一次从头编译，编译复用的前提，不计入）: 1.17 h

The Hilbert–Smith conjecture in every finite dimension (304)

Chain baseline estimate: 链 baseline 估算方法：level 1 ran to the end (42035 s, measured); level 2 was stopped at the 12 h cut after 1193 s, in its solution_build stage (1106 s in it, Lake at 9964/10072); its remainder, 10410 s, is the rest of that stage (1451 s, at least 0) plus the later stages (8960 s): level 1's measured run (42035 s)'s stages times 0.274 (the build had compiled 860 of the 1988 Submission modules in the import closure in 1106 s (whole build ~2556 s, linear)); levels 3-12 not started (the 12 h of timeline were used up): each estimated as level 1's time (42035 s, measured) times the square root of the import-closure ratio (L3 1999, L4 2001, L5 2002, L6 2003, L7 2006, L8 2007, L9 2011, L10 2015, L11 2027, L12 2473 vs 1987 Submission modules; time ~ sqrt(closure): on the seven finished examples' original runs, median error 7% per level, -39%..+30%). The 12 h are displayed timeline: the levels' measured durations inside their containers, one after another

Single-node full: 单节点完整版：estimate: the measured one check of the whole chain (gate build + check, 4,674 s); each level's import closure is 80-100% of the top level's (1,987-2,473 Submission modules), so one level with an empty ledger takes about as long

original: level 1 measured to its end (42,035 s); levels 2-12 estimated. The main page's model uses this tree's earlier node measurement: build 10,920 s, nanoda 46 min, serial Lean 26,422 s, parallel 53 min

Tree树: 209 obligations个义务, 164 accepted (live)个已接受（有效）, depth深度 13; checks that reached check.sh到达 check.sh 的检查 257 (205 proof checks次证明检查, 51 re-checks of glue proofs次胶水复查, 1 root次根检查); closing chains收口链 12 (lengths长度 2, 3, 2, 2, 4, 3, 2, 4, 3, 4, 2, 12), 226 checks after coalescing次检查（合并后）; historical check time in the tree树中历史检查时间合计 150.38 h; production生产配置: max_gate_builds 32, check_timeout 57,600 s. DAG + check plan检查计划 (JSON)

Baseline, each level from scratch (official pipeline: check.sh v12, LOT_LEAN_REPLAY=off)Baseline：每层从头检查（官方流程：check.sh v12，LOT_LEAN_REPLAY=off）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
hs-iso-orig-L1	ACCEPT	42,035.2	34.0	9,338.6	117.0	63.0	2,663.3	29,819.2	32,545.5	1	–	–
hs-iso-orig-L2	stopped at the 12 h cut	1,198.0	–	–	–	–	–	–	–	1	–	–

Full: one check of the whole chain (check-v13), gate build 2.5 min完整版：整链一次检查（check-v13），gate build 2.5 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
hs-iso-one-1	ACCEPT	4,522.9	31.0	66.0	137.0	77.6	4,211.3	3,878.3	4,288.8	12	141,560	0

Root, official check (not in the chain or node numbers)根，官方检查（不计入链和节点数字）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
hs-iso-root-orig	stopped at the 12 h cut	43,232.9	–	–	–	–	–	–	–	1	–	–

Root, LOT 4.5 fast root (check-v15), gate build 2.9 min根，LOT 4.5 快速根（check-v15），gate build 2.9 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
hs-iso-root-fast-1	ACCEPT	607.0	47.0	74.0	288.0	157.2	40.7	27.6	197.9	12	6,366	141,526

Cache build (the library's first build from scratch, a premise of build reuse, not counted)缓存构建（库第一次从头编译，编译复用的前提，不计入）: 4.73 h

Uniform Interior C^1,α Estimates for Infinity-Harmonic Functions (377)

Tree树: 48 obligations个义务, 39 accepted (live)个已接受（有效）, depth深度 4; checks that reached check.sh到达 check.sh 的检查 63 (52 proof checks次证明检查, 10 re-checks of glue proofs次胶水复查, 1 root次根检查); closing chains收口链 2 (lengths长度 2, 2), 61 checks after coalescing次检查（合并后）; historical check time in the tree树中历史检查时间合计 3.20 h; production生产配置: max_gate_builds 32, check_timeout 10,800 s. DAG + check plan检查计划 (JSON)

Baseline, each level from scratch (official pipeline: check.sh v12, LOT_LEAN_REPLAY=off)Baseline：每层从头检查（官方流程：check.sh v12，LOT_LEAN_REPLAY=off）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
ih-iso-orig-L1	ACCEPT	309.3	7.0	171.1	41.0	18.0	15.0	57.2	90.2	1	–	–
ih-iso-orig-L2	ACCEPT	411.7	7.0	237.3	47.0	21.0	20.0	79.4	120.4	1	–	–

run运行	verdict结论	total s总计 s	gate buildgate build	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
ih-iso-side-L1	ACCEPT	127.3	51.6	8.0	41.0	42.0	18.5	17.8	8.9	36.3	12	44,737	0
ih-iso-side-L2	ACCEPT	139.4	39.7	8.0	40.0	45.0	21.0	25.3	10.5	46.4	12	51,186	0

Full: one check of the whole chain (check-v13), gate build 1.4 min完整版：整链一次检查（check-v13），gate build 1.4 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
ih-iso-one-1	ACCEPT	161.6	8.0	55.0	49.0	22.8	26.8	11.4	49.6	12	51,187	0

Root, official check (not in the chain or node numbers)根，官方检查（不计入链和节点数字）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
ih-iso-root-orig	ACCEPT	735.1	7.0	465.5	97.0	26.0	29.0	110.6	165.6	1	–	–

Root, LOT 4.5 fast root (check-v15), gate build 1.5 min根，LOT 4.5 快速根（check-v15），gate build 1.5 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
ih-iso-root-fast-1	ACCEPT	238.0	14.0	65.0	94.0	43.7	21.3	9.6	65.0	12	8,876	51,163

Cache build (the library's first build from scratch, a premise of build reuse, not counted)缓存构建（库第一次从头编译，编译复用的前提，不计入）: 3.9 min

Shafarevich's theorem on solvable Galois groups (shafarevich_solvable_galois)

Tree树: 148 obligations个义务, 106 accepted (live)个已接受（有效）, depth深度 9; checks that reached check.sh到达 check.sh 的检查 180 (151 proof checks次证明检查, 27 re-checks of glue proofs次胶水复查, 2 root次根检查); closing chains收口链 5 (lengths长度 2, 5, 6, 2, 2), 168 checks after coalescing次检查（合并后）; historical check time in the tree树中历史检查时间合计 58.13 h; production生产配置: max_gate_builds 4, check_timeout 10,800 s. DAG + check plan检查计划 (JSON)

Baseline, each level from scratch (official pipeline: check.sh v12, LOT_LEAN_REPLAY=off)Baseline：每层从头检查（官方流程：check.sh v12，LOT_LEAN_REPLAY=off）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sh-iso-orig-L1	ACCEPT	852.4	9.0	398.3	125.0	66.0	49.0	205.1	320.1	1	–	–
sh-iso-orig-L2	ACCEPT	809.9	9.0	418.3	80.0	50.0	49.0	203.6	302.6	1	–	–
sh-iso-orig-L3	ACCEPT	1,034.5	9.0	507.8	114.0	77.0	63.0	263.6	403.6	1	–	–
sh-iso-orig-L4	ACCEPT	1,366.4	10.0	788.1	129.0	72.0	71.0	296.2	439.3	1	–	–
sh-iso-orig-L5	ACCEPT	1,573.9	10.0	965.4	150.0	70.0	69.0	309.5	448.5	1	–	–

run运行	verdict结论	total s总计 s	gate buildgate build	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sh-iso-side-L1	ACCEPT	214.6	77.7	10.0	29.0	69.0	38.2	68.4	27.7	106.6	12	89,374	0
sh-iso-side-L2	ACCEPT	217.3	50.9	10.0	31.0	71.0	39.1	66.2	27.5	105.3	12	89,461	0
sh-iso-side-L3	ACCEPT	193.3	22.5	10.0	30.0	78.0	44.3	31.0	14.5	75.3	12	7,433	89,438
sh-iso-side-L4	ACCEPT	262.1	47.6	10.0	37.0	106.0	78.3	30.7	15.1	109.0	12	7,485	89,438
sh-iso-side-L5	ACCEPT	213.0	91.0	11.0	31.0	88.0	48.5	22.2	34.4	83.0	12	1,475	96,900

Full: one check of the whole chain (check-v13), gate build 1.9 min, 2.0 min完整版：整链一次检查（check-v13），gate build 1.9 min, 2.0 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sh-iso-one-1	ACCEPT	273.5	11.0	44.0	82.0	48.8	87.7	53.2	136.5	12	98,379	0
sh-iso-one-2	ACCEPT	271.5	10.0	44.0	83.0	49.6	84.9	52.6	134.5	12	98,379	0

Root, official check (not in the chain or node numbers)根，官方检查（不计入链和节点数字）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sh-iso-root-orig	ACCEPT	2,488.6	15.0	1,650.0	111.0	58.0	118.0	536.6	712.6	1	–	–

Root, LOT 4.5 fast root (check-v15), gate build 18.1 min根，LOT 4.5 快速根（check-v15），gate build 18.1 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sh-iso-root-fast-1	ACCEPT	346.3	26.0	34.0	117.0	62.0	107.2	45.3	169.2	12	24,610	98,352

Cache build (the library's first build from scratch, a premise of build reuse, not counted)缓存构建（库第一次从头编译，编译复用的前提，不计入）: 16.2 min

Pannwitz–Kuperberg quadrisecant theorem (smooth_knot_has_quadrisecant)

Tree树: 47 obligations个义务, 36 accepted (live)个已接受（有效）, depth深度 6; checks that reached check.sh到达 check.sh 的检查 44 (33 proof checks次证明检查, 10 re-checks of glue proofs次胶水复查, 1 root次根检查); closing chains收口链 2 (lengths长度 2, 4), 40 checks after coalescing次检查（合并后）; historical check time in the tree树中历史检查时间合计 1.71 h; production生产配置: max_gate_builds 8, check_timeout 10,800 s. DAG + check plan检查计划 (JSON)

Baseline, each level from scratch (official pipeline: check.sh v12, LOT_LEAN_REPLAY=off)Baseline：每层从头检查（官方流程：check.sh v12，LOT_LEAN_REPLAY=off）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sk-iso-orig-L1	ACCEPT	115.8	6.0	71.0	25.0	5.0	2.0	6.7	13.7	1	–	–
sk-iso-orig-L2	ACCEPT	192.2	6.0	85.0	40.0	17.0	9.0	35.2	61.2	1	–	–
sk-iso-orig-L3	ACCEPT	200.0	6.0	88.0	38.0	17.0	10.0	40.9	68.0	1	–	–
sk-iso-orig-L4	ACCEPT	251.5	6.0	120.0	37.0	17.0	14.0	57.4	88.5	1	–	–

run运行	verdict结论	total s总计 s	gate buildgate build	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sk-iso-side-L1	ACCEPT	84.3	25.3	7.0	42.0	27.0	5.2	3.0	1.8	8.3	12	14,908	0
sk-iso-side-L2	ACCEPT	120.5	23.9	7.0	43.0	41.0	16.8	12.6	6.4	29.4	12	39,149	0
sk-iso-side-L3	ACCEPT	114.8	26.4	7.0	42.0	41.0	18.0	6.7	4.0	24.7	12	1,906	39,126
sk-iso-side-L4	ACCEPT	113.6	29.7	7.0	36.0	40.0	18.0	12.5	5.9	30.6	12	8,795	39,126

Full: one check of the whole chain (check-v13), gate build 48 s, 50 s完整版：整链一次检查（check-v13），gate build 48 s, 50 s

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sk-iso-one-1	ACCEPT	157.3	7.0	59.0	48.0	21.2	22.2	9.4	43.3	12	47,924	0
sk-iso-one-2	ACCEPT	145.7	7.0	52.0	44.0	20.5	22.1	9.4	42.7	12	47,924	0

Root, official check (not in the chain or node numbers)根，官方检查（不计入链和节点数字）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sk-iso-root-orig	ACCEPT	336.5	6.0	182.1	43.0	18.0	18.0	69.4	105.4	1	–	–

Root, LOT 4.5 fast root (check-v15), gate build 22 s根，LOT 4.5 快速根（check-v15），gate build 22 s

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sk-iso-root-fast-1	ACCEPT	114.0	11.0	37.0	40.0	18.7	7.3	4.7	26.0	12	1,547	47,898

Cache build (the library's first build from scratch, a premise of build reuse, not counted)缓存构建（库第一次从头编译，编译复用的前提，不计入）: 1.8 min

Differentiable sphere theorem (Brendle–Schoen) (sphere_theorem_differentiable)

Tree树: 167 obligations个义务, 111 accepted (live)个已接受（有效）, depth深度 8; checks that reached check.sh到达 check.sh 的检查 143 (112 proof checks次证明检查, 27 re-checks of glue proofs次胶水复查, 4 root次根检查); closing chains收口链 8 (lengths长度 2, 2, 2, 2, 2, 3, 3, 2), 133 checks after coalescing次检查（合并后）; historical check time in the tree树中历史检查时间合计 66.77 h; production生产配置: max_gate_builds 4, check_timeout 10,800 s. DAG + check plan检查计划 (JSON)

Baseline, each level from scratch (official pipeline: check.sh v12, LOT_LEAN_REPLAY=off)Baseline：每层从头检查（官方流程：check.sh v12，LOT_LEAN_REPLAY=off）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sp-iso-orig-L1	ACCEPT	1,286.9	14.0	785.9	95.0	50.0	61.0	281.0	392.0	1	–	–
sp-iso-orig-L2	ACCEPT	1,522.3	14.0	967.6	110.0	61.0	62.0	307.6	430.6	1	–	–
sp-iso-orig-L3	ACCEPT	1,718.7	14.0	1,150.8	107.0	73.0	63.0	310.8	446.8	1	–	–

run运行	verdict结论	total s总计 s	gate buildgate build	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sp-iso-side-L1	ACCEPT	361.1	107.4	17.0	78.0	123.0	63.1	79.9	36.8	143.0	12	70,415	0
sp-iso-side-L2	ACCEPT	281.2	47.2	17.0	45.0	83.0	44.2	92.0	41.7	136.2	12	75,283	0
sp-iso-side-L3	ACCEPT	290.2	26.0	16.0	71.0	107.0	77.2	18.9	15.8	96.1	12	301	75,260

Full: one check of the whole chain (check-v13), gate build 1.7 min完整版：整链一次检查（check-v13），gate build 1.7 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sp-iso-one-1	ACCEPT	286.5	16.0	58.0	79.0	44.9	88.6	39.2	133.5	12	75,563	0

Root, official check (not in the chain or node numbers)根，官方检查（不计入链和节点数字）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sp-iso-root-orig	ACCEPT	2,799.5	14.0	1,973.8	111.0	59.0	110.0	531.7	700.7	1	–	–

Root, LOT 4.5 fast root (check-v15), gate build 4.5 min根，LOT 4.5 快速根（check-v15），gate build 4.5 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
sp-iso-root-fast-1	ACCEPT	506.7	23.0	85.0	208.0	118.1	72.5	37.9	190.6	12	16,575	75,538

Cache build (the library's first build from scratch, a premise of build reuse, not counted)缓存构建（库第一次从头编译，编译复用的前提，不计入）: 25.6 min

Wang–Zahl: the three-dimensional Kakeya conjecture (wang_zahl_kakeya_dimH)

Tree树: 234 obligations个义务, 134 accepted (live)个已接受（有效）, depth深度 10; checks that reached check.sh到达 check.sh 的检查 193 (156 proof checks次证明检查, 33 re-checks of glue proofs次胶水复查, 4 root次根检查); closing chains收口链 8 (lengths长度 3, 3, 2, 2, 2, 4, 7, 4), 174 checks after coalescing次检查（合并后）; historical check time in the tree树中历史检查时间合计 89.26 h; production生产配置: max_gate_builds 4, check_timeout 10,800 s. DAG + check plan检查计划 (JSON)

Baseline, each level from scratch (official pipeline: check.sh v12, LOT_LEAN_REPLAY=off)Baseline：每层从头检查（官方流程：check.sh v12，LOT_LEAN_REPLAY=off）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
wz-iso-orig-L1	ACCEPT	223.8	6.0	96.0	41.0	18.0	14.0	48.8	80.8	1	–	–
wz-iso-orig-L2	ACCEPT	227.0	6.0	102.0	39.0	19.0	12.0	49.0	80.0	1	–	–
wz-iso-orig-L3	ACCEPT	286.0	6.0	136.0	43.0	20.0	17.0	64.0	101.0	1	–	–

run运行	verdict结论	total s总计 s	gate buildgate build	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
wz-iso-side-L1	ACCEPT	116.9	25.1	7.0	35.0	40.0	19.0	15.8	7.9	34.9	12	46,899	0
wz-iso-side-L2	ACCEPT	117.0	21.6	6.0	35.0	41.0	18.2	16.7	7.6	35.0	12	46,921	0
wz-iso-side-L3	ACCEPT	109.6	21.1	6.0	35.0	41.0	19.7	7.9	4.7	27.6	12	2,198	46,898

Full: one check of the whole chain (check-v13), gate build 37 s, 37 s完整版：整链一次检查（check-v13），gate build 37 s, 37 s

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
wz-iso-one-1	ACCEPT	131.9	7.0	48.0	40.0	19.5	17.4	8.3	36.9	12	49,098	0
wz-iso-one-2	ACCEPT	130.4	6.0	48.0	39.0	19.4	17.9	8.3	37.4	12	49,098	0

Root, official check (not in the chain or node numbers)根，官方检查（不计入链和节点数字）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
wz-iso-root-orig	ACCEPT	5,122.0	25.0	4,554.2	124.0	57.0	79.0	282.7	418.8	1	–	–

Root, LOT 4.5 fast root (check-v15), gate build 59.5 min根，LOT 4.5 快速根（check-v15），gate build 59.5 min

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
wz-iso-root-fast-1	ACCEPT	599.4	43.0	62.0	215.0	177.9	101.4	34.9	279.3	12	31,231	49,073

Cache build (the library's first build from scratch, a premise of build reuse, not counted)缓存构建（库第一次从头编译，编译复用的前提，不计入）: 1.9 min

Every four-dimensional Kakeya set has full Hausdorff dimension (074)

Chain baseline estimate: 链 baseline 估算方法：levels 1-3 ran to the end (36706 s, measured); level 4 was stopped at the 12 h cut after 6527 s, in its solution_export stage (235 s in it); its remainder, 1483 s, is the rest of that stage (136 s, at least 0) plus the later stages (1347 s): level 3's measured run (12415 s)'s stages times 0.642 (its solution_build stage took 6191 s against the reference's 9639 s); level 5 not started (the 12 h of timeline were used up): each estimated as level 3's time (12415 s, measured) times the square root of the import-closure ratio (L5 7476 vs 7434 Submission modules; time ~ sqrt(closure): on the seven finished examples' original runs, median error 7% per level, -39%..+30%). The 12 h are displayed timeline: the levels' measured durations inside their containers, one after another

Single-node full: 单节点完整版：estimate, as the chain's one check (see the inputs): the five levels' closures differ by under 1% (7,434-7,476 Submission modules); re-measure pending the nanoda-t fix

original: levels 1-3 measured to their end, level 4 to the 12 h cut, level 5 estimated

Tree树: 296 obligations个义务, 241 accepted (live)个已接受（有效）, depth深度 12; checks that reached check.sh到达 check.sh 的检查 358 (284 proof checks次证明检查, 73 re-checks of glue proofs次胶水复查, 1 root次根检查); closing chains收口链 20 (lengths长度 2, 3, 4, 2, 3, 3, 2, 2, 2, 4, 3, 2, 4, 3, 2, 4, 3, 2, 4, 5), 319 checks after coalescing次检查（合并后）; historical check time in the tree树中历史检查时间合计 55.14 h; production生产配置: max_gate_builds 32, check_timeout 10,800 s. DAG + check plan检查计划 (JSON)

Baseline, each level from scratch (official pipeline: check.sh v12, LOT_LEAN_REPLAY=off)Baseline：每层从头检查（官方流程：check.sh v12，LOT_LEAN_REPLAY=off）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
kk-iso-orig-L1	ACCEPT	13,076.0	74.0	10,418.7	517.1	222.0	225.0	1,619.1	2,066.2	1	–	–
kk-iso-orig-L2	ACCEPT	11,215.0	66.0	8,633.7	409.0	293.0	230.0	1,583.1	2,106.2	1	–	–
kk-iso-orig-L3	ACCEPT	12,415.3	63.0	9,661.4	594.1	379.0	217.0	1,500.7	2,096.8	1	–	–
kk-iso-orig-L4	stopped at the 12 h cut	6,529.0	–	–	–	–	–	–	–	1	–	–

Root, official check (not in the chain or node numbers)根，官方检查（不计入链和节点数字）

run运行	verdict结论	total s总计 s	setup准备	build编译	export导出	parse解析	nanodananoda	LeanLean	kernels wall内核墙钟	replay threads重放线程	constants checked检查常量	skipped (ledger)跳过（账本）
kk-iso-root-orig	ACCEPT	16,048.1	108.0	13,458.7	501.1	273.0	222.0	1,485.2	1,980.3	1	–	–

Cache build (the library's first build from scratch, a premise of build reuse, not counted)缓存构建（库第一次从头编译，编译复用的前提，不计入）: 2.50 h

FData数据

data.json — every number on this page with its source (seconds)本页全部数字及其来源（秒）. Per tree每棵树: direct_summand · 078 · 304 · 377 · shafarevich_solvable_galois · smooth_knot_has_quadrisecant · sphere_theorem_differentiable · wang_zahl_kakeya_dimH · 074 — obligations (id, parent, depth, state) and the check plan (kind, node, historical seconds, the check it waited for).义务（id、父节点、深度、状态）和检查计划（类型、节点、历史秒数、所等的检查）。