HEXAGONbeta

Nonexistence of DSRGs with ten parameter sets: the rank of A − θI versus a submatrix prescribed at a vertex

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

Contributed by Iurii Ivanov ↗

Version 1 / Nov 10, 2026 / CC BY 4.0

Abstract

For a directed strongly regular graph (DSRG), the parameters determine rank(A − θI) at nontrivial eigenvalues θ. For small λ or t = λ + 1 they almost determine a piece of this matrix at a vertex: a piece needing more rank excludes the graph, and a small margin leaves finitely many cases. We exclude (50, 11, 7, 0, 3), (68, 13, 7, 0, 3), (100, 16, 7, 0, 3), (108, 19, 9, 0, 4), (48, 9, 5, 0, 2), (55, 16, 12, 1, 6), (66, 10, 5, 4, 1) and (91, 12, 6, 5, 1), open in Hobart and Brouwer's table, and their complements. Counting twin classes reproves (96, 15, 10, 9, 1) and (28, 6, 3, 2, 1): for the first, rank replaces one counting bound; for the second, it is unused. Lean 4 with Mathlib proves nine exclusions; for (28, 6, 3, 2, 1) its kernel also checks a SAT certificate. (48, 9, 5, 0, 2) ends with a search by two separately written programs, the second certified by CaDiCaL unsatisfiability proofs checked by drat-trim.

Provenance statement

The arguments and proofs, the verification programs and the text of this work were written by AI agents based on Claude Opus 5.5 model (Anthropic) under my direction. I chose the problem, directed the work and take responsibility for the publication. I understand the statements of the results, the principle of the method and which check each result rests on, but neither i nor any other human has checked the proofs line by line. The correctness of the work therefore rests on machine checks. Nine of the ten nonexistence results are proved in Lean 4 with Mathlib and checked by the Lean kernel; for (28, 6, 3, 2, 1) the kernel also checks a SAT certificate. For (48, 9, 5, 0, 2) the reduction is proved in the text, and the last step is a search by two separately written programs; the unsatisfiability of the formulas of the second program is checked in every case of the search, but this step is not formally verified. Table 3 of the paper shows what each statement rests on; the steps proved only in the text were read by independent AI reviewers.

Tools used

Anthropic
Claude OpusVersion 5.5
Lean
LeanVersion 4.35.0
Python Software Foundation
PythonVersion 3.12
Armin Biere
CaDiCaLVersion 1.9.5
Marijn Heule
drat-trim
Lean
MathlibVersion 4.35.0

References

  1. A. M. Duval. A directed graph version of strongly regular graphs. Journal of Combinatorial Theory, Series A 47 (1988), 71--100. https://doi.org/10.1016/0097-3165(88)90043-XDOI
  2. S. A. Hobart, A. E. Brouwer. Parameters of directed strongly regular graphs. Table, version of 6 November 2026 (header Last-Modified: Fri, 06 Nov 2026 06:02:12 GMT). https://homepages.cwi.nl/~aeb/math/dsrg/dsrg.htmllink
  3. mira_loom. Nonexistence of DSRGs (50,35,28,23,28), (72,21,7,4,7), (81,24,8,5,8), (81,63,56,47,56), (96,80,75,65,75), (100,35,14,9,14) and all positive multiples. rStation, problem strongly_regular_graphs, paper 7, version 1, 2026. https://rstation.ai/problems/strongly_regular_graphs/papers/7/v1link
  4. mira_loom. Nonexistence of DSRGs (28m,21m,18m,15m,18m) for every odd m: (28,6,3,2,1), (28,21,18,15,18), (84,20,11,10,3), and (84,63,54,45,54). rStation, problem strongly_regular_graphs, paper 11, version 1, 2026. https://rstation.ai/problems/strongly_regular_graphs/papers/11/v1link
  5. S. Chung, W. J. Wesley. AI research conducted on rStation, with results available on GitHub, October 2026. Repository https://github.com/dualverse-ai/strong_regular_graph, accessed on 6 November 2026; the Lean theorem on the nonexistence of (96,15,10,9,1)(96, 15, 10, 9, 1) is DSRG.no_order96_complement in the file nonexistence/DSRG/Nonexistence96.lean , based on RS7 . The authors and the title are given as in the table HobartBrouwer2026 .link
  6. kirkman_loom. Nonexistence of 42 open DSRGs via rank-6 and rank-7 hyperplane duality, existence of DSRG(64,14,7,3,3) and DSRG(80,18,8,4,4), and closed-form abelian group-ring families. rStation, problem strongly_regular_graphs, paper 5, version 1, 2026. The title is not in the text of the paper; it is taken from citations in other papers of the platform. https://rstation.ai/problems/strongly_regular_graphs/papers/5/v1link
  7. Nonexistence of directed strongly regular graphs (50, 11, 7, 0, 3), (68, 13, 7, 0, 3), (100, 16, 7, 0, 3), (108, 19, 9, 0, 4), (55, 16, 12, 1, 6) and (48, 9, 5, 0, 2): the rank of A − θI against the neighbourhood of a vertex. rStation, problem strongly_regular_graphs, paper 74, version 2, 2026-11-01. Merged into the present paper and reworked; posted by an AI agent directed by the author. https://rstation.ai/problems/strongly_regular_graphs/papers/74/v2link
  8. Directed strongly regular graphs with t = λ + 1: twin classes of closed neighbourhoods and the nonexistence of (66, 10, 5, 4, 1) and (91, 12, 6, 5, 1). rStation, problem strongly_regular_graphs, paper 76, version 2, 2026-11-01. Merged into the present paper and reworked; posted by an AI agent directed by the author. Besides the two sets of the title, the text excludes (40,9,6,5,1)(40, 9, 6, 5, 1), (80,19,13,12,2)(80, 19, 13, 12, 2), (96,15,10,9,1)(96, 15, 10, 9, 1) and (28,6,3,2,1)(28, 6, 3, 2, 1) with their complements. https://rstation.ai/problems/strongly_regular_graphs/papers/76/v2link
  9. L. de Moura, S. Ullrich. The Lean 4 theorem prover and programming language. Automated Deduction --- CADE 28 , LNCS 12699 (2021), 625--635. https://doi.org/10.1007/978-3-030-79876-5_37DOI
  10. The mathlib Community. The Lean mathematical library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020) , 367--381. https://doi.org/10.1145/3372885.3373824DOI
Show all 28 referencesShow fewer references
  1. L. K. Jørgensen. Non-existence of directed strongly regular graphs. Discrete Mathematics 264 (2003), 111--126. https://doi.org/10.1016/S0012-365X(02)00555-1DOI
  2. C. D. Godsil, S. A. Hobart, W. J. Martin. Representations of directed strongly regular graphs. European Journal of Combinatorics 28(7) (2007), 1980--1993. https://doi.org/10.1016/j.ejc.2006.08.008DOI
  3. L. K. Jørgensen. Rank of adjacency matrices of directed (strongly) regular graphs. Linear Algebra and its Applications 407 (2005), 233--241. https://doi.org/10.1016/j.laa.2005.05.005DOI
  4. L. K. Jørgensen. Directed strongly regular graphs with rank 5. Linear Algebra and its Applications 477 (2015), 102--111. https://doi.org/10.1016/j.laa.2015.03.019DOI
  5. J. Ma, B. Zhang, J. Liu, J. Zhao. Directed strongly regular graphs with rank 6. Discrete Mathematics 340(6) (2017), 1367--1373. https://doi.org/10.1016/j.disc.2016.10.013DOI
  6. S. A. Hobart, J. Williford. New feasibility conditions for directed strongly regular graphs. Electronic Journal of Combinatorics 24(1) (2017), #P1.16. https://doi.org/10.37236/5496DOI
  7. A. V. Bondarenko, A. Prymak, D. Radchenko. Non-existence of (76, 30, 8, 14) strongly regular graph. Linear Algebra and its Applications 527 (2017), 53--72. https://doi.org/10.1016/j.laa.2017.03.033DOI
  8. A. V. Bondarenko, D. V. Radchenko. On a family of strongly regular graphs with λ = 1. Journal of Combinatorial Theory, Series B 103(4) (2013), 521--531. https://doi.org/10.1016/j.jctb.2013.05.005DOI
  9. P. Rowlinson, B. Tayfeh-Rezaie. Star complements in regular graphs: old and new results. Linear Algebra and its Applications 432(9) (2010), 2230--2242. https://doi.org/10.1016/j.laa.2009.04.022DOI
  10. J. Azarija, T. Marc. There is no (75, 32, 10, 16) strongly regular graph. Linear Algebra and its Applications 557 (2018), 62--83. https://doi.org/10.1016/j.laa.2018.07.019DOI
  11. Directed strongly regular graphs: general construction and nonexistence theorems from 38 papers of the rStation problem. rStation, problem strongly_regular_graphs, paper 43, version 1, 2026-10-25. Posted by an AI agent directed by the author. https://rstation.ai/problems/strongly_regular_graphs/papers/43/v1link
  12. A. Ignatiev, A. Morgado, J. Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. Theory and Applications of Satisfiability Testing (SAT 2018) , LNCS 10929, 428--437. https://doi.org/10.1007/978-3-319-94144-8_26DOI
  13. C. Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. Principles and Practice of Constraint Programming (CP 2005) , LNCS 3709, 827--831. https://doi.org/10.1007/11564751_73DOI
  14. A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, F. Pollitt. CaDiCaL 2.0. Computer Aided Verification (CAV 2024) , LNCS 14681, 133--152. https://doi.org/10.1007/978-3-031-65627-9_7. The paper describes version 2.0; we used version 1.9.5 from PySAT Ignatiev2018 .DOI
  15. D. E. Knuth. Estimating the efficiency of backtrack programs. Mathematics of Computation 29 (1975), 121--136. https://doi.org/10.1090/S0025-5718-1975-0373371-6DOI
  16. N. Wetzler, M. J. H. Heule, W. A. Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. Theory and Applications of Satisfiability Testing (SAT 2014) , LNCS 8561, 422--429. https://doi.org/10.1007/978-3-319-09284-3_31DOI
  17. L. Cruz-Filipe, M. J. H. Heule, W. A. Hunt Jr., M. Kaufmann, P. Schneider-Kamp. Efficient certified RAT verification. Automated Deduction --- CADE 26 , LNCS 10395 (2017), 220--236. https://doi.org/10.1007/978-3-319-63046-5_14DOI
  18. S. Szeider. lrat-catcher, version 0.2.1. A Lean 4 program, 2026. https://github.com/leansolving/lrat-catcherlink

Version history

  1. v1 · 32 pagesSubmitted by Iurii IvanovInitial depositCurrentNov 09, 2026