There is no strongly regular graph with parameters (300,117,60,36)

We show that no strongly regular graph with parameters (300,117,60,36) exists, and hence none with the complementary parameters (300,182,100,126). The parameter set is marked "?" in Brouwer's table, and it is one of the twelve open cases with smallest eigenvalue -3 listed by Koolen and Gebremichel. No symmetry is assumed. The matrix A+3I+J is positive semidefinite of rank 27, so the vertices span an even lattice of rank 27; we choose a maximal even overlattice M containing (1/30) times the sum of the vertex vectors. We prove by hand that the discriminant form of M is one of exactly eight forms; besides Milgram's formula the proof uses a parity congruence satisfied by the classes of M#/M. For each form we glue M to an explicit even lattice of rank 5 and obtain an even unimodular lattice of rank 32. Its harmonic theta series give linear equations in the numbers of vectors of M# of each class, norm and inner product with w = (1/420) times the sum of the vertex vectors; elementary necessary conditions on the integer vector ((x,v_i))_i set many of these numbers to zero, and the vertex vectors and their differences give lower bounds. For each of the eight forms the resulting system has no nonnegative solution, as shown by exact rational Farkas certificates. Verification. Two independently written generators of the systems agree over Q, each produced its own certificates for all eight forms, and every vanishing condition was re-decided by an independent solver-free program. Controls on graphs that exist (the line graph of AG(3,3), srg(117,36,15,9), at shells 2,4 and 2,4,6, and a Latin-square srg(100,27,10,6)) satisfy every generated equation exactly, and planted wrong counts are rejected. A single standard-library Python script in the archive (verify_all.py) re-checks all certificates, vanishing conditions and controls in about ten minutes. The proof is computer-assisted in the admissibility of vector types and in the infeasibility of the eight systems; it has not yet been refereed by an independent human reader. Formal verification. The finite core of the proof is in addition checked by the Lean 4 kernel (directory lean/ of the archive; Lean v4.35.0-rc4 with a pinned Mathlib; axioms only propext, Classical.choice and Quot.sound): the infeasibility of the eight systems with the independent generator's exact Farkas certificates, the finite classification count (512 candidate forms, 16 without the parity congruence, exactly the eight forms with it), all 779 vanishing conditions (including the 185 that use the neighbourhood equation), the complements and anti-isometries, the modular-form relations, the lower bounds of all eight systems, all equations of degree 0 for all eight forms, and every equation used by the certificate of the form g4, of every degree. The equations of positive degree of the other seven forms and the reduction from a graph to the linear systems (vertex lattice, gluing, modularity of theta series) are not formalised, and the nonexistence statement itself is not a Lean theorem.