How LOT checks machine-written Lean proofs, what each optimization of the trusted check removes, and how long a chain of obligations takes to check with and without them. Numbers are measured on the proof tree of The Hilbert–Smith conjecture in every finite dimension[1].
LOT 如何检查机器写出的 Lean 证明，可信检查的每项优化省掉了哪一部分，以及一条义务链在有无这些优化时各要查多久。数字来自 The Hilbert–Smith conjecture in every finite dimension[1] 这棵证明树的实测。
LOT (Lean Option Tree) proves a hard Lean 4[2] theorem by splitting it into a tree of frozen sub-theorems, called obligations. Many LLM agent sessions work on the tree at once: some try to prove an obligation directly, others split it into child statements plus a glue proof of the parent from them. Nothing is accepted on an agent's word. Every glue proof and every proof enters the tree only after a trusted check with the Lean-Eval checker[3]: the comparator[4], the independent nanoda kernel[5] and the Lean kernel itself. A visual tour of how LOT schedules this work is in [6].
LOT（Lean Option Tree）把一个困难的 Lean 4[2] 定理拆成一棵由冻结子定理（称为义务）组成的树。许多 LLM agent 会话同时在这棵树上工作：有的直接证明某个义务，有的把它拆成若干子命题，再写一个由子命题推出父命题的胶水证明。agent 自己说了不算：每个胶水证明和每个证明，都要先通过 Lean-Eval 检查器[3] 的可信检查才能进入树里，也就是 comparator[4]、独立的 nanoda 内核[5] 和 Lean 内核本身。LOT 如何调度这些工作，可以看 [6] 的可视化。
As trees grew to hundreds of obligations, checking rather than proving became the bottleneck. Our running example is the main theorem of The Hilbert–Smith conjecture in every finite dimension[1]. Its proof tree has 156 obligations; the root and the obligations below it that each have a single open child form a chain of 12 non-root levels. Every check on that chain re-verifies the same few very heavy proofs, about 11.5 hours per check with the original pipeline.
当一棵树长到几百个义务时，瓶颈从证明变成了检查。本文的例子是 The Hilbert–Smith conjecture in every finite dimension[1] 的主定理。它的证明树有 156 个义务；根和它下面各自只剩一个未完成子义务的那些义务连成一条链，共 12 个非根层。链上的每次检查都要重新验证同样几份非常重的证明，用原始流程每次约 11.5 小时。
When Lean compiles a file[7], the kernel already checks every declaration before it is written to an .olean file. The trusted check trusts neither the elaborator nor the .olean files: it rebuilds in a sandbox, exports the whole environment as plain terms[8], has two independently written kernels re-check all of it, and finally confirms that the theorem's statement matches the frozen problem statement and that only permitted axioms are used. This is the validation procedure the Lean reference manual recommends for untrusted proofs[9].
Lean 编译时[7]，每条声明在写进 .olean 文件之前就已经被内核检查过一次。可信检查不信任编译器和 .olean 文件：它在沙箱里重新编译，把整个环境导出成纯文本的项[8]，交给两个独立实现的内核从头重查，最后核对定理命题与冻结的题面一致、只用了允许的公理。这正是 Lean 官方参考手册对不可信证明推荐的验证方式[9]。
Almost all the time goes into step ④. One node of the Hilbert–Smith tree[1] exports about 1.28 GB with 120,385 declarations, and the Lean kernel checks them one at a time on one thread. 0.1% of the declarations (120) take 60% of the time and 1% take 97%; the slowest single declaration takes 487 s. Mathlib's 93,000 constants check in under 1 ms at the median; the slow ones are all proofs written by our agents.
时间几乎全在第 ④ 步。Hilbert–Smith 证明树[1] 的一个节点导出约 1.28 GB、120,385 条声明，Lean 内核一条一条单线程检查：0.1% 的声明（120 条）占 60% 的时间，1% 占 97%；单条最慢 487 s。Mathlib 的 9.3 万个常量中位数不到 1 ms，慢的全是 agent 自己写的证明。
lake build[10] runs in a sandbox with no network and read-only dependencies. Modules compile in parallel along the import graph; each is parsed, macro-expanded and elaborated (tactics, type-class search, unification), and every declaration is checked by the kernel before it is written to an .olean file[7].propext, Quot.sound, Classical.choice).lake build[10]（没有网络，依赖只读）。各模块按 import 依赖图并行编译：解析、宏展开、精化（策略执行、类型类搜索、合一），每条声明经内核检查后写入 .olean 文件[7]。propext、Quot.sound、Classical.choice）。The 12 non-root levels of the Hilbert–Smith chain[1], with all proofs written; the clock runs until every level is accepted. The root check is left out: by our rule it always runs the official pipeline above, unchanged.
Hilbert–Smith 链[1] 上的 12 个非根层，证明都已写好，从这一刻算到每层都被接受。根检查不算在内：按我们的规则，它永远原样走上面的官方流程。
The same chain under each configuration, on one shared clock. A dashed circle is waiting, a filling circle is being checked (its color is the current step), a solid circle is accepted. A row named "Your toggles" appears when the toggles above match none of the presets.
同一条链在各种配置下的检查过程，共用一个时钟。虚线圈表示在等，环形填充表示正在检查（颜色是当前步骤），实心圈表示已接受。上面的开关组合不属于任何预设时，会多出一行“你的开关”。
Same verdicts. We re-ran the complete root check of every proof that LOT or our colleagues have produced, with the Lean kernel replayed in parallel. So far 18 of 18 re-checked proofs (of 48) give exactly the recorded serial result: the verdict, the exit code, the comparator's protocol lines in order, and the build output.
结论一致。我们把 LOT 和同事证完的每一份证明都完整重跑了一次根检查，Lean 内核用并行重放。目前已重检的 18 份（共 48 份）中，18 份与当时的串行检查完全一致：结论、退出码、comparator 的检查记录（含顺序）和编译输出。
Faster checks. To compare speed under identical conditions we took six representative problems and, from each proved tree, the chain of intermediate theorems that closed together. Each chain was checked twice at the same time on two identical workers: once with Lean's original pipeline and once with all six optimizations on. Each problem has its own page with the measured run played back.
检查更快。为了在相同条件下比较速度，我们挑了 6 道代表题，从每棵已证树里取一条同时收口的中间定理链，在两台相同的 worker 上同时检查两遍：一遍用 Lean 原始流程，一遍打开全部 6 项优化。每道题有一个单独页面，回放实测的检查过程。
smooth_knot_has_quadrisecant13.2 → 0.8 min · 15.95×Watch both checks →看两遍检查 →wang_zahl_kakeya_dimH11.9 → 3.2 min · 3.75×Watch both checks →看两遍检查 →direct_summandbeing measured测量中shafarevich_solvable_galoisbeing measured测量中sphere_theorem_differentiablebeing measured测量中Measured on 2026-10-24; cards fill in as the remaining measurements finish.测于 2026-10-24；其余测量完成后补齐。
LOT is written in Python: a controller schedules agent sessions, and a gate runs every trusted check on dedicated check workers. The source is in the private repository humanfia/tree-flow, directory lot/; paths below are relative to it, and each optimization has a design note under lot/docs/.
LOT 用 Python 编写：控制器调度 agent 会话，网关在专用检查 worker 上执行每一次可信检查。源码在私有仓库 humanfia/tree-flow 的 lot/ 目录下，下表路径都相对于该目录；每项优化在 lot/docs/ 下都有设计说明。
| Part部分 | Implemented实现日期 | Code代码 | Status状态 |
|---|---|---|---|
| Trusted check and gate可信检查与网关 | Oct 7–13, 20262026-10-07 至 10-13 | trusted/, lean_option_tree/gate.py, lake.py, backbone.py | released已发布 |
| Scheduling and infrastructure调度与基础设施 | local-disk checks Oct 12; pull-based workers Oct 13; sealed nodes first Oct 14; spill-over workers Oct 15, 2026本地盘检查 10-12；拉取式 worker 10-13；封卷节点优先 10-14；本机溢出 10-15（2026 年） | lean_option_tree/workers.py, placement.py, nodepool.py, dockergate.py | released已发布 |
| Build reuse编译产物复用 | library cache Oct 13; per-content reuse and deltas Oct 14, 2026库缓存 10-13；按内容复用与增量包 10-14（2026 年） | lean_option_tree/backbone.py, refresher.py | released已发布 |
| Parallel kernel replay并行内核重放 | Oct 23, 2026; in production Oct 242026-10-23；10-24 投入生产 | a fork of the comparator[4] plus a new trusted check script; lean_option_tree/checkerswitch.py, lake.pycomparator[4] 的分支加新的可信检查脚本；lean_option_tree/checkerswitch.py、lake.py | in production use, not yet released已在生产使用，尚未发布 |
| Verified-constant ledger已验证常量账本 | Oct 13, 2026; local-worker fix Oct 232026-10-13；10-23 修复本机 worker | lean_option_tree/ledger.py and the comparator fork 及 comparator 分支 | released已发布 |
| Speculative level checking链上各层推测并行检查 | checking ahead Oct 17; one-step close Oct 19, 2026提前检查 10-17；一步收链 10-19（2026 年） | lean_option_tree/prewarmdep.py, chains.py, chains_view.py, policy.py, rootonce.py | released已发布 |
| One check per chain一链一检 | Oct 24, 20262026-10-24 | lean_option_tree/chainone.py and a new trusted check script 及新的可信检查脚本 | implemented, under review; new trees only已实现，评审中；只用于新树 |
All times are measured on the Hilbert–Smith tree[1] unless noted. Build from scratch 3.03 h (5,533 modules on 16 cores; 10,920 s measured for 5,521 of them); with build reuse 1–2 min (we use 2 min). Export and parse 3 min (estimate). nanoda 46 min; serial Lean replay 7.34 h (26,422 s); parallel kernel replay 53 min with 16 threads and nanoda running at the same time, its verified output byte-identical to the serial run. Ledger: on another large proof tree the kernel phase was 85% shorter and 93.1% of constants were skipped, with 7/7 spot checks identical; in the model it only helps checks that start after another check has finished (an inference, not a measurement). Closing a chain level by level adds 0.05–0.2 h per level (we use 0.1 h). Before the scheduling work a check waited 16–20 min to start at the median (we use 18 min), afterwards about 8 s. At most 4 chain levels are checked at once. One check per chain is in development; its time is modeled as one check of the top level's closure.
除特别说明外，时间都在 Hilbert–Smith 证明树[1] 上实测。从头编译 3.03 h（16 核 5,533 个模块，实测 10,920 s 编到 5,521 个）；复用后 1–2 min（模型取 2 min）。导出与解析 3 min（估计）。nanoda 46 min；Lean 串行重放 7.34 h（26,422 s）；并行内核重放 16 线程、nanoda 同时运行共 53 min，验证输出与串行逐字节一致。账本：在另一棵大证明树上内核阶段缩短 85%，跳过 93.1% 的常量，抽查 7/7 一致；模型中它只对在别的检查完成后才开跑的检查有效（推算，非实测）。逐层收链每层多等 0.05–0.2 h（模型取 0.1 h）。调度优化前检查开跑前的等待中位数 16–20 min（模型取 18 min），优化后约 8 s。链上最多 4 层同时检查。一链一检在开发中，用时按一次顶层闭包的检查估算。