Nonexistence of a Leech Tree of Order 18: A Computer-Assisted Proof

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,\dots ,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.

Computer-assisted proof with a Lean 4 structural formalization. Companion artifacts (v1.0.0): https://github.com/chesshippo/leech18-lean-artifact/tree/v1.0.0 and https://github.com/chesshippo/leech18-computational-evidence/releases/tag/v1.0.0 . Earlier preprint: https://zenodo.org/records/22180940