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, …, 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. Companion artifacts, version v1.0.0: Lean 4 development:https://github.com/chesshippo/leech18-lean-artifact Computational evidence:https://github.com/chesshippo/leech18-computational-evidenceThe computational results underlying this work, together with the associated repository, were publicly disclosed prior to the release of this preprint via X (formerly Twitter) and GitHub. The publication date listed here refers to the first public release of the present manuscript (Version 1), rather than to the earlier public disclosure of the computational results.