{"id":"arxiv/2609.20492","url":"https://arxiv.org/abs/2609.20492","tags":["math.CO"],"score":0,"title":"Nonexistence of a Leech Tree of Order 18: A Computer-Assisted Proof","domain":"math.CO","source":"arxiv","authors":["Maseeh Ghodsi"],"reviews":0,"subject":"math.CO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-17","reactions":{}}