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.
Related
- A computer-assisted proof of robust transitivity
- An independent computer-assisted proof of the Chen-Raspaud conjecture for k=4
- A Computer-Assisted Proof that R(5,10;5,8)=21 for the Generalized Threshold Ramsey Number
- A computer-assisted proof of Krzyż's conjecture for the sixth coefficient
- Star-shaped periodic solutions of a system of delay differential equations: A computer-assisted proof
BibTeX
@misc{ghodsi2026nonexistence,
title = {{Nonexistence of a Leech Tree of Order 18: A Computer-Assisted Proof}},
author = {Maseeh Ghodsi},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.20492},
eprint = {2609.20492},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.20492},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Nonexistence of a Leech Tree of Order 18: A Computer-Assisted Proof
AU - Maseeh Ghodsi
PY - 2026
DA - 2026/09/17
PB - arXiv
DO - 10.48550/arxiv.2609.20492
UR - https://arxiv.org/abs/2609.20492
AB - 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.
ER -