18頂点のLeech木が存在しないことの計算機援用証明
Nonexistence of a Leech Tree of Order 18: A Computer-Assisted Proof
この論文をやさしく読む
ひとことで言うと
全頂点対の重み付き距離が1から順に一度ずつ現れる木について、18頂点のものは存在しないと計算機支援で示します。
何に役立つ？
組合せ論の非存在問題を、数学的な帰着・形式検証・全探索を組み合わせて解く事例です。
この研究の面白いところ
構造を八つの局所配置に絞り、各配置を完全探索で排除します。入力やソースのハッシュ、探索範囲、終了記録も記録しています。
どこまで分かった？
Leanで検証したのは構造部分です。探索プログラム・実行・証明書検査器はLean形式化されておらず、端から端までのLean証明ではないと著者が明記しています。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
位数nのLeech木とは、各辺が正の整数の重みを持ち、頂点対の間のn(n−1)/2個の重み付き距離が、ちょうど1, 2, …, n(n−1)/2となる木である。本論文は、位数18のLeech木が存在しないことの計算機援用証明を与える。議論は3層からなる。 第1に、Lean 4による形式化で、論文中で使用する構造上の事実を検証する。これらの事実により、存在すると仮定したすべての例を8つの局所配置のいずれかへ帰着し、いくつかの必要条件を正当化する。第2に、通常の数学的議論によって、成分対に関するブロック全体の完全被覆条件と、再帰的探索の完全性を証明する。第3に、網羅的な計算によって8つすべての配置を排除する。計算では、厳密な網羅範囲、ソースと入力のハッシュ値、終了時の実行記録、および検査済みの厳密にゼロという結果を記録している。 構造に関する層はカーネルによって検査されているが、探索プログラム、その実行、および証明書の検査器はLeanで形式化されていない。したがって、この結果は計算機援用証明であり、最初から最後までLeanで完結した証明ではない。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-17（UTC）
- 最新改訂
- 2026-09-17 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-17 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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.
著者のコメント
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
arXiv ID: 2609.20492 ／ 要約の誤りについて