Nonexistence of a Leech Tree of Order 18: A Computer-Assisted Proof
Maseeh Ghodsi
math.CO
Sep 17, 2026 · v1
TL;DR
Lean 4 with Mathlib verifies the structural facts (configuration classification, forced weights, parity bounds) underpinning a computer-assisted nonexistence proof of an order-18 Leech tree.
Abstract
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.
Problem
A Leech tree of order n is a tree with positive integer edge weights whose n(n-1)/2 pairwise distances are exactly 1,...,n(n-1)/2. Order 18 was the smallest order whose existence remained open.
Approach
The proof has three layers. A Lean 4 development (Lean 4.24.0, Mathlib) kernel-checks structural facts: Taylor's order restriction, order-18 parity split, hop-diameter bound, first physical weights, forced least-missing distances, persistent merge blocks, and the eight-configuration exhaustiveness classification. Conventional (non-Lean) mathematics proves a component-pair whole-block exact-cover pruning condition and search completeness. A C++ exhaustive search with certificate generation closes all eight local configurations.
Results
No Leech tree of order 18 exists. Exhaustive computation over the eight initial configurations produced 39,672 exact-zero terminal receipts across 8,567,320,605 node visits, with no accepting leaf or abandoned branch. The Lean development uses no sorry/admit/native_decide, relying only on propext, Classical.choice, and Quot.sound.
| Configuration | Receipts | Result |
|---|
| 1 | 5,202 | exact zero |
| 5 | 25,684 | exact zero |
| 6 | 3,983 | exact zero |
| 7 | 3,301 | exact zero |
| Total | 39,672 | — |
Exhaustive computations for all eight configurations
