A smaller impossible-to-three-color network has been found
- What it is
- A paper reports a 64-node network with no short loops that still needs four colors, supported by SAT and Lean certificates.
- Who did it
- Glauco Rampone
- What it could mean
- Even a network without short loops can demand four colors. This 64-node construction would tighten the known size range—and show how computer searches can leave evidence others can replay.
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
Improved bounds for the smallest 4-chromatic graph of girth six ↗See the proposed checks
Re-run the witness and SAT/Lean checks from locked sources; separately examination the exhaustive lower-bound computation; highest risk is completeness of the search/certificate bridge for the lower bound.
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
- Improves the known range to (29 ≤ n₆(4) ≤ 64), supplies an explicit 64-vertex witness, and reports a Lean-checked non-3-colourability certificate.
- Why this could matter
- A smaller impossible-to-three-color network has been found The paper finds a 64-node network with no short loops that still needs four colors, then uses SAT and Lean certificates to check it. It advances both an extremal graph puzzle and reviewable computer-assisted mathematics.
- If it holds up
- Methods: it tightens the known size range and demonstrates how search, independent code, certificates, and formal proof can support one verifiable result.
- If it does not
- The failure would expose whether the graph witness, exhaustive search, SAT certificate, or formal checker broke—valuable evidence for better verification pipelines.
- Impact horizon
- Methods · Graph theory · Formal verification · SAT solving
- Version
- submitted 2026-08-24 11:14:46 UTC.
- Why we tracked it
- a narrowly stated extremal result with independent scripts, SAT certificates, and a linked Lean 4 formalization.
- Highest-risk dependency
- completeness of the search/certificate bridge for the lower bound.
- Available artifacts
- New Slack discovery packet; G64 repository, independent scripts, SAT certificates, and Lean 4 proof are linked by the primary record.
- Current boundary
- Intake record only; examination not started.