不存在18阶Leech树：一个计算机辅助证明
Nonexistence of a Leech Tree of Order 18: A Computer-Assisted Proof
浏览论文内容
中文总结 AI 辅助
本文通过Lean 4形式化结构事实、常规数学论证与穷举计算三层方法，计算机辅助证明了不存在18阶Leech树，并给出可验证的计算证书。
中文摘要 AI 辅助
Leech树（阶为$n$）是一棵具有正整数边权的树，其$n(n-1)/2$个两两加权距离恰好为$1,2,\ldots,n(n-1)/2$。本文给出了一个计算机辅助证明，证明不存在18阶的Leech树。论证分为三个层次。首先，在Lean 4中的一次开发验证了本文使用的结构事实。这些事实将每个候选例子归结为八种局部构型之一，并证明了若干必要条件。其次，常规数学论证证明了分量对整块精确覆盖条件以及递归搜索的完备性。第三，穷举计算关闭了所有八种构型。该计算记录了精确覆盖、源文件和输入哈希、终端收据以及检查过的精确为零的结果。结构层经过内核检查，但搜索程序、其执行以及证书检查器尚未在Lean中形式化。因此，该结果是一个计算机辅助证明，而非端到端的Lean证明。
英文摘要
A Leech tree of order $n$ is a tree with positive integral edge weights whose $n(n-1)/2$ pairwise weighted distances are precisely $1,2,\ldots,n(n-1)/2$. This paper gives a computer-assisted proof that no Leech tree of order $18$ exists. The argument has three layers. First, a development in Lean 4 verifies the structural facts used in the paper. These facts reduce every putative example to one of eight local configurations and justify several necessary conditions. Second, conventional mathematical arguments prove a component-pair whole-block exact-cover condition and the completeness of a recursive search. Third, exhaustive computations close all eight configurations. The computation records exact coverage, source and input hashes, terminal receipts, and checked exact-zero results. The structural layer is kernel-checked, but the search program, its execution, and the certificate checker have not been formalized in Lean. The result is therefore a computer-assisted proof, not an end-to-end Lean proof.
