When a proof has both a kernel and a search
- What it is
- A paper claims a weighted tree whose distances are exactly 1 through 153 cannot exist when it has 18 vertices.
- Who did it
- Maseeh Ghodsi
- What it could mean
- A finite graph puzzle can be impossible for reasons a computer helps expose. This work also makes the proof boundary visible: Lean checks some structure, while a separate search still needs its own scrutiny.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
Nonexistence of a Leech Tree of Order 18: A Computer-Assisted Proof ↗See the proposed checks
Source-lock the tagged artifacts; verify hashes and provenance; inspect the Lean declarations and axiom closure; then map the structural reduction to the separate computation/checker boundary. Any future execution must be isolated and must not silently turn a component replay into a whole-proof verdict.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
A tree with unusually demanding distances
In a weighted tree, the distance between two vertices is the sum along their unique connecting path. The paper claims that the required all-distinct distance pattern is impossible for an 18-vertex Leech tree. This is a generic tree illustration, not such a configuration or a search certificate.
Read the source · Abstract · nonexistence of an order-18 Leech tree ↗- Source kind
- Mathematical research record
- Evidence reported
- Manuscript; independent examination not started
- Source date
- ; added 2026-09-18
- What it claims
- The abstract claims that no Leech tree of order 18 exists. It says Lean 4 verifies structural facts reducing a putative example to eight local configurations; conventional mathematics establishes an exact-cover condition and search completeness; exhaustive computation closes the eight cases. The source explicitly calls this a computer-assisted proof rather than an end-to-end Lean formalization.
- Why this could matter
- When a proof has both a kernel and a search Can one weighted tree realize every whole-number distance from 1 through 153 exactly once? This paper says no—and carefully divides its evidence between Lean-checked reductions and an exhaustive search.
- If it holds up
- Methods: it would resolve this finite graph puzzle while offering a candid map of what a proof kernel certifies and what remains in the computation-and-checker trust boundary.
- If it does not
- The split record helps locate the problem: a formal reduction, a conventional argument, the search program, its run, or the checker may need correction.
- Impact horizon
- Methods · Graph theory · Computer-assisted proof · Formal verification
- Version
- submitted 2026-09-17 14:41:05 UTC
- Why we tracked it
- a fresh computer-assisted finite nonexistence claim with a clearly stated formal/computational boundary. Intake is not an end-to-end proof validation or an independent reproduction.
- Highest-risk dependency
- Kernel checking of the structural layer does not certify the unformalized search, its execution, or the theorem-to-artifact correspondence. Conversely, a gap in the computational layer would not automatically negate every formal structural fact.
- Available artifacts
- The arXiv record links a version-v1.0.0 Lean artifact, a version-v1.0.0 computational-evidence release, and an earlier Zenodo preprint. The source expressly says the search program, its execution, and certificate checker are not formalized in Lean. No artifact was downloaded, executed, or replayed.
- Current boundary
- Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Source-lock the tagged artifacts; verify hashes and provenance; inspect the Lean declarations and axiom closure; then map the structural reduction to the separate computation/checker boundary. Any future execution must be isolated and must not silently turn a component replay into a whole-proof verdict.