HEXAGONbeta

The independence number of the generalized Johnson graph J(13,5,3)J(13,5,3)

A mix of human-written and AI-generated textHuman understanding: all partsmath.CO — Combinatoricsmath.MG — Metric Geometry

Contributed by Mustafa Stanikzai

Version 2 / Nov 12, 2026 / CC BY 4.0

Abstract

Let J(13,5,3)J(13,5,3) be the graph on the 5-element subsets of a 13-element set, two subsets being adjacent when they share exactly 3 elements. We prove that α(J(13,5,3))=33\alpha(J(13,5,3)) = 33. The graph is an explicit unit-distance graph in R12\mathbb{R}^{12}, so χ(R12)≥⌈1287/33⌉=39\chi(\mathbb{R}^{12}) \ge \lceil 1287/33 \rceil = 39; earlier bounds from explicit finite graphs give at most 38. A recent preprint of Davies gives much larger bounds, none from an explicit finite graph. An explicit independent set gives α≥33\alpha \ge 33. For the upper bound, a symmetry reduction splits the problem into 200 clique subproblems, and a certifying solver refutes each one with a proof log that the checker VeriPB accepts. An uncertified computation reproduces the value α(J(13,6,4))=46\alpha(J(13,6,4)) = 46 reported by Exoo and Ismailescu, which gives χ(R12)≥38\chi(\mathbb{R}^{12}) \ge 38.

Author comments: 16 pages. Programs, certificates and proof logs: https://doi.org/10.5281/zenodo.24145863 Changes from version 1: 28 cross-references to lemmas, propositions, claims, definitions and corollaries were printed with the word "Theorem" (for example "Theorem 2.4" for Lemma 2.4). They now carry the correct names. The reference numbers were already correct. Statements, proofs, results and bibliography are unchanged.

Provenance statement

I directed the work, ran the computations, and reviewed the manuscript, the code and the reported computations. AI tools: I used Claude Code (Anthropic) with the Claude Fable 5, Fable 5.1, Fable 5.2 and Opus 5.5 models to plan, draft, revise and review the paper and to write its code, including the programs for the computation and the verification programs. I used OpenAI Codex with the GPT-5.6 Sol model to evaluate plans and, on some occasions, to review drafts of the paper. Computation: the lower bound is an explicit independent set of size 33, listed in the paper. For the upper bound, programs in R build the graph and split the problem into 200 clique subproblems. The clique solver of the Glasgow Subgraph Solver refuted each subproblem with a proof log, and the proof checker VeriPB 3.0.2 accepted all 200 logs. Three Python programs that share no code with the R implementation or with each other recompute the graph, the decomposition and the subproblem files, and a further Python program checks that each pseudo-Boolean formula encodes its subproblem. An uncertified search with a modified MaxCliqueDyn, rerun with MoMC and cliquer, reproduces α(J(13,6,4)) = 46. Limits: VeriPB, the encoding checker and the programs that check the decomposition are not formally verified. The programs, certificates, proof logs and run records are on Zenodo: https://doi.org/10.5281/zenodo.24145863

Tools used

Anthropic
Claude FableVersion 5
Anthropic
Claude FableVersion 5.1
Anthropic
Claude FableVersion 5.2
Anthropic
Claude OpusVersion 5.5
Anthropic
Claude Code
OpenAI
ChatGPTVersion GPT-5.6 Sol

References

  1. Cherkashin, D.; Kulikov, A.; Raigorodskii, A. On the chromatic numbers of small-dimensional Euclidean spaces. Discrete Applied Mathematics, vol. 243, pp. 125–131. 2018DOI
  2. Bachoc, C.; Passuello, A.; Thiery, A. The density of sets avoiding distance 1 in Euclidean space. Discrete & Computational Geometry, vol. 53, no. 4, pp. 783–808. 2015DOI
  3. Balogh, J.; Chen, C.; Li, B. Forbidding exactly one Hamming distance. 2026
  4. Davies, J. Measurable obstructions for unmeasurable colourings. 2026
  5. de Bruijn, N. G.; Erdős, P. A colour problem for infinite graphs and a problem in the theory of relations. Indagationes Mathematicae, vol. 13, pp. 371–373. 1951
  6. Erdős, P.; Ko, C.; Rado, R. Intersection theorems for systems of finite sets. The Quarterly Journal of Mathematics, vol. 12, pp. 313–320. 1961DOI
  7. Lovász, L. Kneser's conjecture, chromatic number, and homotopy. Journal of Combinatorial Theory, Series A, vol. 25, pp. 319–324. 1978DOI
  8. Schrijver, A. New code upper bounds from the Terwilliger algebra and semidefinite programming. IEEE Transactions on Information Theory, vol. 51, pp. 2859–2866. 2005DOI
  9. Scheinerman, E. R.; Ullman, D. H. Fractional Graph Theory: A Rational Approach to the Theory of Graphs. John Wiley & Sons. 1997
  10. Exoo, G.; Ismailescu, D. On the chromatic number of Rn\mathbb{R}^n for small values of nn. 2014
Show all 22 referencesShow fewer references
  1. Konc, J.; Janežič, D. An improved branch and bound algorithm for the maximum clique problem. MATCH Commun. Math. Comput. Chem., vol. 58, pp. 569–590. 2007
  2. Ostrowski, J.; Linderoth, J.; Rossi, F.; Smriglio, S. Orbital branching. Mathematical Programming, vol. 126, pp. 147–178. 2011DOI
  3. Delsarte, P. An algebraic approach to the association schemes of coding theory. Philips Research Reports Supplements, vol. 10. 1973
  4. Li, C.-M.; Jiang, H.; Manyà, F. On minimization of the number of branches in branch-and-bound algorithms for the maximum clique problem. Computers & Operations Research, vol. 84, pp. 1–15. 2017DOI
  5. Kahle, M.; Taha, B. New lower bounds on χ(Rd)\chi(\mathbb{R}^d) for d=8…12d=8\dots 12. 2014. Journal version: Geombinatorics 24 (2015), no. 3, pp. 109–116
  6. Raigorodskii, A. M.; Sinelnikov-Murylev, P. S. Johnson graphs, their random subgraphs, and some of their extremal characteristics. Russian Mathematical Surveys, vol. 80, no. 3, pp. 471–530. 2025DOI
  7. Bogaerts, B.; Gocht, S.; McCreesh, C.; Nordström, J. Certified dominance and symmetry breaking for combinatorial optimisation. Journal of Artificial Intelligence Research, vol. 77, pp. 1539–1589. 2023DOI
  8. Gocht, S.; McBride, R.; McCreesh, C.; Nordström, J.; Prosser, P.; Trimble, J. Certifying solvers for clique and maximum common (connected) subgraph problems. Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP '20), vol. 12333, pp. 338–357. 2020DOI
  9. Brélaz, D. New methods to color the vertices of a graph. Communications of the ACM, vol. 22, no. 4, pp. 251–256. 1979DOI
  10. McCreesh, C.; Prosser, P.; Trimble, J. The Glasgow Subgraph Solver: Using Constraint Programming to Tackle Hard Subgraph Isomorphism Problem Variants. ICGT 2020, pp. 316–324. 2020
  11. R Core Team. R: A Language and Environment for Statistical Computing. 2026DOI
  12. Anders, M.; Bogaerts, B.; Bogø, B.; Gontier, A.; Koops, W.; McCreesh, C.; Myreen, M. O.; Nordström, J.; Rebola-Pardo, A.; Oertel, A.; Tan, Y. K. Documentation of VeriPB and CakePB for the SAT Competition 2026link

Version history

  1. v1 · 16 pagesSubmitted by Mustafa Stanikzai16 pages. Programs, certificates and proof logs: https://doi.org/10.5281/zenodo.24145863SupersededNov 12, 2026
  2. v2 · 16 pagesSubmitted by Mustafa Stanikzai16 pages. Programs, certificates and proof logs: https://doi.org/10.5281/zenodo.24145863 Changes from version 1: 28 cross-references to lemmas, propositions, claims, definitions and corollaries were printed with the word "Theorem" (for example "Theorem 2.4" for Lemma 2.4). They now carry the correct names. The reference numbers were already correct. Statements, proofs, results and bibliography are unchanged.CurrentNov 12, 2026