A stubborn graph pattern may be impossible
- What it is
- The paper claims a Lean proof that no strongly regular graph with parameters (266, 45, 0, 9) exists.
- Who did it
- Kay Akiyama
- What it could mean
- Some perfectly balanced networks may be impossible to build, however long you search. This proof could rule out one elusive pattern with a computer-checkable argument instead of a giant search certificate.
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 Strongly Regular Graph with Parameters (266,45,0,9): A Certificate-Free Lean Proof ↗See the proposed checks
Obtain the archive in a separate ephemeral environment; check its release hash/dependencies, compile the public root with Lean, independently run the stated checker, and examination the arXiv theorem-to-formal-statement correspondence.
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 →
- What it claims
- The paper claims there is no strongly regular graph with parameters ((266,45,0,9)), via a classification-free Lean proof that reduces the remaining case to an impossible projection identity. It is a current example of formal proof construction without external infeasibility certificates.
- Why this could matter
- A stubborn graph pattern may be impossible Strongly regular graphs are highly symmetric networks with exact local rules. This paper claims one long-sought parameter set cannot exist, using a Lean formalization that follows the contradiction through lattice and design arguments rather than an external infeasibility certificate.
- If it holds up
- It would close this specific existence question and supply a formally checkable example of a classification-free nonexistence proof.
- If it does not
- The parameter translation, lattice argument, or formal statement may need repair; the graph’s existence question would remain open.
- Impact horizon
- Methods · Combinatorics · Formal verification · Graph theory
- Version
- submitted 2026-09-08 06:43:09 UTC
- Why we tracked it
- a fresh finite nonexistence claim with an archived Lean 4 formalization and an explicit independent nanoda check claim; not independently replayed.
- Highest-risk dependency
- The high-level combinatorial claim depends on exact parameter and theorem-statement correspondence; a successful checker run would not establish that the prose claim has been modeled without omission.
- Available artifacts
- arXiv links a Zenodo Lean 4 formalization archive and states the theorem uses standard Lean axioms and was also checked with nanoda. No artifact was downloaded, executed, or replayed.
- Current boundary
- Intake record only; examination not started.