HEXAGONbeta

The covering number C(13,7,4) is 30: A classification-assisted exact proof

Primarily AI-generated textHuman understanding: no partsmath.CO — Combinatorics

Contributed by John Tripodo ↗

Version 1 / Oct 31, 2026 / CC BY 4.0

Abstract

We prove that C(13,7,4)=30C(13,7,4)=30, using the classification of minimum (12,6,3)(12,6,3) coverings by Gordon, Patashnik, Petro and Taylor. A hypothetical 2929-block cover has at least five points lying in exactly 1515 blocks. The link at one of these points leaves only 1414 blocks outside it. The other four points force complete families of outside blocks whose overlaps must agree. An exhaustive computation shows that every compatible choice requires 1515 outside blocks, giving a contradiction. The known 3030-block construction is therefore optimal. We give reproducible exact computations and a public Lean formalization of a second argument for the finite obstruction. The Lean theorem states the published minimum bound and classification as explicit hypotheses; it does not reprove those results.

Provenance statement

Anthropic Claude and OpenAI ChatGPT/Codex were used extensively in developing the arguments, programs, formalization, and manuscript. John Tripodo directed the project and is responsible for the submission. The text is primarily AI-generated; no human checking and understanding is attested. Exact Python and C++ computations were replayed. The public Lean sources are authenticated against historical build and axiom-audit records; the newly packaged public Lean project has not been freshly compiled. The formal theorem retains the published 1995 minimum bound and classification as explicit hypotheses. Automated checks are not independent human peer review. Public paper and code: https://github.com/jjtripodo-lgtm/c13-covering-number . Frozen Lean theorem: https://github.com/jjtripodo-lgtm/c13-covering-number/blob/254ee82fdbc215ad73f732f807a83d69be7c1e22/lean/C13Global/Final.lean

Tools used

Anthropic
Claude
OpenAI
ChatGPT
Lean
LeanVersion 4.31.0-rc1
OpenAI
Codex

References

  1. D. M. Gordon, O. Patashnik, J. Petro and H. Taylor, Minimum (12,6,3)(12,6,3) Covers , Ars Combinatoria 40 (1995), 161--177. https://combinatorialpress.com/ars-articles/volume-040-ars-articles/minimum-12-6-3-covers/.link
  2. D. M. Gordon, La Jolla Covering Repository , (v,k,t)=(13,7,4)(v,k,t)=(13,7,4), historic upper and lower bounds. https://ljcr.dmgordon.org/cover/table.html and https://ljcr.dmgordon.org/cover/low_tab.html.link
  3. E. Dwares, Formal elimination of link class 52 in the C(13,7,4)C(13,7,4) search , public certification project (2026), https://github.com/edwares/class52-formal-certification. The certification concerns one class, not the full optimum.link
  4. C. Krug, The covering number C(12,6,4)C(12,6,4) is 41 , preprint (2026), arXiv:2607.23766, https://arxiv.org/abs/2607.23766.arXiv

Version history

  1. v1Submitted by John TripodoInitial depositCurrentOct 30, 2026