We prove that no strongly regular graph with parameters (69,20,7,5) exists. Consequently, there is no quasi-symmetric 2-(46,16,8) design with block intersection numbers 4 and 6, and we obtain an independent proof that there is no Steiner system S(2,6,46). The proof assumes no automorphisms. • The vertices of such a graph are norm-4 vectors spanning an even lattice L_X of rank 24, and L_X contains u = s/23, where s is the sum of the vertices.• Every maximal even overlattice of L_X has determinant 1 or 8; in the second case the discriminant form is determined.• The unimodular case gives the 24 Niemeier lattices. The determinant-8 case gives one genus, which we list completely using Borcherds' classification of the 665 odd unimodular lattices of dimension 25. In every host lattice, exact identities reduce the vertex set to a finite search, and all remaining cases are decided by exact computer calculations. The solver verdicts on the remaining determinant-8 candidate sets come from two independent programs: a CP-SAT model, and a CNF encoding solved by kissat whose UNSAT results carry DRAT proofs checked by drat-trim and, converted to LRAT, by the formally verified checker cake_lpr. Both programs recovered known strongly regular graphs of the same shape. Section 10 states which computations were re-implemented independently and which rest on one implementation. The appendices contain data, algorithms, reproduction instructions and a manifest of the source code, which is distributed in a public archive and as ancillary files.
No takes yet. Share an insight, caveat, or question.
Anton Koval (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: