arXiv++ Combinatorics

We prove that no strongly regular graph with parameters $(266, 45, 0, 9)$ exists. The proof is formalized in Lean 4 and Mathlib without external infeasibility certificates or assumed classification theorems. A hypothetical graph gives a rank-$12$ integral Gram lattice with an integral centroid. A Lorentzian change of form, a marked $D_7$ gluing, and an explicit rank-six complement produce a positive-definite even unimodular lattice of rank $24$, together with the original indexed family of $220$ vectors. Harmonic theta identities and a root-isolation inequality force the root system $A_{11} \perp D_7 \perp E_6$. First and second moments then exclude the possible complements: the final case reduces to an impossible binary projection identity $4x + 4y - 2z = 50$. A type-$A$ subcase is closed by a separate classification-free proof of the known nonexistence of a quasi-symmetric $2$-$(56, 12, 9)$ design with intersections $0, 3$. That argument constructs a Krein graph and forces a Steiner $3$-$(12, 4, 1)$ design, contradicting its replication equation. The formal theorem depends only on the three standard Lean axioms and has also been checked independently with nanoda. The archived formalization is release v2.0.0.

For each integer $n\geq 1$, let $N(n)$ denote the number of distinct subsets of $\{2,\ldots,n+1\}$ obtained by choosing one forbidden residue class modulo each integer from $2$ to $n$; this is OEIS sequence A396595 (https://oeis.org/A396595). Equivalently, $N(n)$ is the initial-restriction complexity of the family of global residue-profile survivor sequences. We derive a closed formula, depending on the parity of $n$, for the number of locally distinct residue profiles, and an exact inclusion--exclusion formula for profiles realizing a prescribed survivor set. We prove that $\log N(n)$ has order $n/\log n$, with any possible leading constant between $\log 2$ and $2\log 2$. For prime traces, the logarithm of their number is asymptotic to $(\log 2)n/\log n$. Our main comparison theorem shows that $N(n)$ is exponentially equivalent to the block complexity of prime-admissible subsets of an interval of length $n$. The combinatorial component of the private composite coordinates argument used in the comparison theorem is formalized in Lean 4/Mathlib. We also establish an exact structural recurrence, characterize extendibility by a residue-class covering criterion, and give a dynamic enumeration algorithm. As further illustrations of the model, we exhibit purely periodic global profiles generating prime-valued survivor sequences for which we have not identified corresponding OEIS entries.

Let $A\in\mathbb{R}^{m\times n}$ have columns of Euclidean norm at most one. We prove that $\operatorname{disc}(A)\le2395\left(1+\log_+\frac n9\right)^{1/4}+2\sqrt2$. Here $\log_+t=\max\{0,\log t\}$. Building on Bansal and Jiang's affine spectral independence framework, we remove the $(\log\log n)^{7/4}$ factor from their bound. The fourth root comes from balancing the logarithmic decrease in the alive dimension against the fourth power of the row thresholds. Historical exponential sums control the covariance budget across size classes with summable thresholds. An exact threshold-sum certificate gives the coefficient $2395$, and rounding at most eight remaining fractional coordinates costs $2\sqrt2$. The finite construction also gives partial colourings from any prescribed starting point and at any prescribed depth, preserving existing signs. We formalize the partial- and full-colouring theorems in Lean, including the finite trajectory, exact threshold sum and final rounding, with Bansal--Jiang Theorem A.4 as the sole external research theorem assumption.

For a fixed graph F, the F-degree of a vertex v in a host graph H is the number of subgraphs of H isomorphic to F that contain v, and H is F-irregular if its F-degrees are pairwise distinct. We show that every finite connected graph F on at least three vertices admits a finite connected F-irregular host. For noncomplete F, the proof builds the host from a threshold graph with one deleted edge; when the minimum degree is at least two, a small incidence gadget with distinct weighted column sums separates the remaining exceptional vertices. The construction also yields infinitely many pairwise non-isomorphic finite connected F-irregular hosts for every noncomplete F. The complete-pattern case follows from a theorem of Chartrand, Holbert, Oellermann and Swart. A Lean 4 formalization of Theorem 1.1 is described, taking the published complete-pattern theorem as its sole custom axiom.

We prove that the realization graph of every graphical degree sequence is maximally Hamiltonian: it is Hamilton-laceable when bipartite on more than one vertex, and Hamilton-connected otherwise. This answers Problem P59 of Mütze's survey of combinatorial Gray codes, and the Hamiltonicity question recorded as open by Barrus, in the strongest form either admits. The argument is an induction on the number of ground vertices, cutting the realization graph at a single ground vertex into fibers and the quotient they lie over. The proof is formalized in Lean 4 and checked by its kernel, with seven results cited from the literature and nothing else assumed. Its engine is a classification. The realizable neighborhoods of a ground vertex form a shifted family -- one closed under replacing an element by a smaller one -- and the quotient is the Johnson graph of that family. Such a Johnson graph can fail to be Hamilton-connected, and we determine exactly when: the failures are one explicit family of examples, the Y-families, and each of them fails between a single pair of its members. A shifted family with a greatest member never fails, and those families are exactly the shifted matroids, where the conclusion already follows from the theorem of Naddef and Pulleyblank on the graphs of 0/1-polytopes. The obstruction lives entirely outside the matroid case, which is why it has not been met before.

For every finite $P\subset\mathbb{R}^2$ we prove $|\{p\cdot q: p,q\in P\}|\gg |P|^{199/295}$, with an absolute constant and no logarithmic loss, where $199/295 = 2/3+7/885$. This improves the bound $2/3+7/1425$ of Kokkinos (arXiv:2502.12727), which in turn had improved the first superthreshold bound of Hanson, Roche-Newton, and Senger. The main new ingredient is the inequality $|F^{(2)}G^{(2)}/(F^{(2)}G)| \le |AB|(|AF|/|A|)^4(|BG|/|B|)^3$: each radial profile retains its own Petridis growth-minimizing subset, and the product of the two subsets serves as a common base for both growth operators; a prime-power construction shows this is sharp under its hypotheses. The second ingredient is a weighted-median replacement for the dyadic selection in the squeezing argument of Roche-Newton and Wong, upgrading their seven-factor expander to a logarithm-free form; an appendix gives the complete proof from the Solymosi-Zahl incidence theorem. We complement the lower bound with a third-moment structure theorem for near-extremal configurations and a construction showing that the pinned problem admits no linear lower bound: $\max_{p\in P}|p\cdot P| = O(|P|/\sqrt{\log |P|})$ is attainable. The algebraic core, the median lemma, the surface identities, and the pinned construction are formally verified in Lean 4 and included as ancillary files.

We report on our ongoing project to develop a computational pipeline, AutoGraphForge, for an automated graph-theoretic conjecturing-refuting-formalizing-proving system. Conjecture generation is counterexample-guided and runs in rounds: a Graffiti3 generator proposes conjectures over a small, evolving snapshot table $T$ (initially a few hundred graphs with their computed invariants) that grows only by counterexamples to its own conjectures. A novelty filter of $559$ classical and folklore relations, closed under transitive composition and linear identity substitution, decides via a linear program whether a candidate is already implied by known results. Surviving candidates are tested against a dataset of about $348,000$ graphs, unioning the complete House of Graphs invariant export, the exhaustive census of all connected graphs on at most nine vertices, several extremal families (strongly regular, minimal Ramsey, Cayley, cages, barbells, lollipops, spiders), and random models. Counterexample-search algorithms then attack the remainder. Run for several rounds on an HPC cluster, the loop yields $6,522$ conjectures that survived the refutation dataset, the novelty filter and every active-search run -- among them nontrivial relations between the annihilation number and the edge-cover number for bipartite and regular graphs, which we prove by hand. A subsequent formalization and proving stage deterministically translates each surviving conjecture into a Lean 4 statement skeleton; every candidate proof is kernel-verified against a pinned mathlib4 and our custom invariant preamble. This stage integrates two neural provers -- DeepSeek-Prover-V2-671B (served with vLLM) and the Lean-specialised OProver-32B -- behind the independent kernel check. It is implemented end-to-end and passes initial sanity checks, with the full pipeline currently running on the cluster.

Harwit and Sloane conjectured that every nonsingular entrywise-nonnegative matrix $A\in\mathbb R^{n\times n}$ satisfies $\|A^{-1}\|_F\ge 2n(n+1)^{-1}\|A\|_{\max}^{-1}$, with equality precisely for positive multiples of $S$-matrices. Cheng proved the conjecture in odd dimensions, while Frankel and Urschel proved the even-dimensional case for $n\ge1000$. We complete the remaining even-dimensional cases. Starting from the structural identities in Frankel--Urschel Lemma 2.1, we derive an exact global defect budget and combine binary rounding with Gram projection. A refined ten-row obstruction handles every even $n\ge66$; a finite exact calculation handles $4\le n\le64$, $n\ne6$; and a separate multi-column energy argument treats $n=6$. The order-two case follows from a direct calculation. The new even-dimensional proof has been formalized in Lean 4, with Frankel--Urschel Lemma 2.1 as its sole external mathematical input. Together with Cheng's odd-dimensional theorem, this proves the S-matrix conjecture in every dimension.

A $p$-ary bent partition of $\mathbb{F}_p^n$ is a partition into $K$ nonempty cells such that every balanced assignment of its cells to $\mathbb{F}_p$ produces a bent function. It was asked whether every possible depth $K$ is a power of $p$; for general $p$, previous affirmative results required regularity or cell-symmetry hypotheses. We prove the stronger unconditional statement that, for every nonzero $h$, exactly $p^n/K$ points remain in the same fine cell under translation by $h$. Thus the fine cells form a partitioned difference family and the fine label map is zero-difference balanced. Consequently $K\mid p^n$, so $K=p^t$; nonempty cells further give $1\le t<n$. In even dimension, the classical cell-size theorem yields $K\mid p^{n/2}$. Together with the known odd-dimensional ternary three-fibre parameter restriction, this gives the global bound $t\le\lfloor n/2\rfloor$. The proof is an exact finite average over balanced coarsenings. The main counting identity and selected consequences are formalized and kernel-checked in Lean 4.

For integers $k,g \ge 3$ let $n_g(k)$ denote the minimum order of a graph with chromatic number $k$ and girth at least $g$. Exoo and Goedgebeur (DMTCS 2019) proved $26 \le n_6(4) \le 66$; their 66-vertex witness has remained the smallest known 4-chromatic graph of girth 6. We improve both bounds to $29 \le n_6(4) \le 64$. The upper bound is witnessed by an explicit 4-chromatic graph of girth 6 on 64 vertices with 152 edges; it is vertex- and edge-critical, and its automorphism group is cyclic of order 8 and acts semiregularly. The lower bound is an exhaustive isomorph-free computation in the SAT modulo symmetries framework with co-certificate learning, driven by the Liu-Postle edge-density bound for 4-critical graphs of girth five; it re-derives $n_6(4) \ge 26$ by a disjoint method and is validated on the known values $n_4(4)=11$ and $n_5(4)=21$. We complement the bounds with structural obstructions: no smaller witness arises from either known witness by local modifications; no 4-chromatic Cayley graph of girth 6 exists on 54-63 vertices (for orders 59 and 61 no vertex-transitive witness exists at all); and no witness on at most 63 vertices admits a semiregular automorphism group with two or three vertex orbits, for any finite group. Since every known witness of an $n_g(4)$ record with $g \ge 6$ is a lift of a small base graph along a semiregular action, these results close the most symmetric part of that regime below 64 vertices. All properties of the new graph are verified by independent programs and formally certified in the Lean 4 proof assistant: the non-3-colourability is established inside Lean by a formally verified checker that re-validates a 219,532-node refutation certificate, with a machine-checked soundness theorem.

The Rogers--Ramanujan identities equate a $q$-series whose exponents are governed by a quadratic form with an infinite product supported on two residue classes modulo~$5$. Identities of this shape are scarce, and a central problem is to identify the structures that produce them in families. Huang, Jiang, and Oblomkov have proposed a source of a new kind: to each pair of coprime integers $a,b>1$ they attach an infinite-rank $q$-series $Z_{a,b}(q)$, assembled from counts of commuting nilpotent matrix pairs $(A,B)$ with $A^a=B^b$ over finite fields, and they conjecture that it equals an explicit product of $(a-1)(b-1)/2$ modular units of level $a+b$. The $a=2$ cases are the Andrews--Gordon identities; no case with $a>2$ was known. We prove the conjecture for $(a,b)=(3,4)$, $(3,5)$, $(3,7)$, and $(3,8)$. Our proofs pass through a finer sum-to-sum identity, which we conjecture for all $b$ coprime to $3$ and establish for all $b$ when $q=1$. Lau and Ono have since proved that identity in general, and with it the full $a=3$ case. These identities have been formalized and verified in Lean by AxiomProver.

In the transversal achievement game on the $n\times n$ board, two players alternately claim cells, and the first to own a transversal---a set of $n$ cells of which no two share a row or column---wins. Ranđelović showed that the first player wins for every $n\ge4$, while the game is a draw for $n=2,3$. We give an independent proof that the first player wins for $n\ge4$ that additionally establishes a bound on the length of the win: the given strategy forces a win by ply $2n+3$, i.e.\ on the first player's $(n+2)$-nd move, for every $n\ge4$. The proof yields a strategy that is fully determined by a fixed rule on the current position and can thus be implemented directly. We isolate the use of the hypothesis $n\ge4$ to two steps in the analysis, explaining why the argument fails at $n=3$. An exhaustive computational search implementing the strategy verifies it against every legal defense for $n=4,5,6$, confirming both the strategy's validity and that the $2n+3$ bound is attained in these cases. The main theorem has also been formalized and machine-checked in Lean 4.

For an odd prime $p$, let $m(p)$ be the minimum cardinality of a set $A\subseteq \mathbb Z/p\mathbb Z$, with $|A|\geq2$, such that no sum in $A+A$ has a unique representation as an unordered pair from $A$, with repetition allowed. Bedert proved \[ m(p)\gg \log p\, \frac{\sqrt{\log^{(3)}p}}{\log^{(4)}p}. \] We prove the stronger lower bound \[ m(p)\gg \log p\,\log\log p. \] More generally, if $G$ is a finite Abelian group and $q(G)$ is the least prime divisor of $|G|$, then the same explicit estimate holds whenever $q(G)>2$, and in particular every subset $A\subseteq G$ with $|A|\geq2$ and no unique sum has cardinality $\gg \log q(G)\,\log\log q(G)$ as $q(G)\to\infty$. The proof has two structural inputs. First, a maximum subset of $A$ whose distinct-element subset sums of size at most four are all different has cardinality $\gg\log p$. This follows from a short-coordinate lemma and a collision-lattice determinant argument. Second, we refine Bedert's density increment. Alternative representations are oriented toward an uncovered endpoint, coalesced by their translation, and separated into wide, exposed, and recurrent batches. A load-sensitive entropy lemma codes the recurrent translations using their actual final fibre multiplicities. The resulting global shift-set complexity is $\exp(O(K))$, where $K$ is the ratio of $|A|$ to the level-four additive dimension. This forces $K\gg\log\log p$, and the theorem follows. All headline statements and the structural implications used to derive them have also been checked in Lean~4 with explicit integer constants. As a secondary and logically independent result, we construct weakly ternary-balanced sets and obtain \[ m(p)\leq \frac{(\log p)^2}{2(\log 3)^2} +\left(\frac{2}{\log 3}+o(1)\right) \frac{(\log p)^2}{\log\log p}. \]

Kolokolnikov conjectured that, among finite simple graphs on $n$ vertices with exactly $2(n-2)$ edges, the complete bipartite graph $K_{2,n-2}$ maximizes algebraic connectivity. We prove the conjectured statement for every $n\ge123$: every such graph has algebraic connectivity at most $2$, while $K_{2,n-2}$ attains $2$. The proof begins with explicit Rayleigh-quotient certificates that exclude several local configurations from a hypothetical counterexample. A global degree count then controls the number and total excess of vertices of degree at least $5$ and bounds the edge excess of the subgraph induced by vertices of degree at most $4$. A Moore-type breadth-first-search criterion uses this excess to guarantee a short cycle, while a spectral criterion excludes cycles in the same length range. An explicit arithmetic estimate shows that the two criteria apply simultaneously once $n\ge123$. A Lean formalization covering every $n\ge4$, including the complementary range $4\le n\le122$, has been produced with MerLean and checked by the Lean kernel; the present paper gives a self-contained mathematical account of the large-order component.

For coprime $1<a<b$, let $M_n^{a,b}(\mathbb{F}_q)$ be the set of commuting pairs of nilpotent $n\times n$ matrices over $\mathbb{F}_q$ with $X^a=Y^b$. Huang, Jiang, and Oblomkov assembled their orders as an Eulerian $q$-series $Z_{a,b}(q)$. They conjectured that it is an explicit product $P_{a,b}(q)$ involving Jacobi's theta function and Dedekind's eta-function, implying the threefold equality $$\underbrace{\prod_{n\ge1}(1-q^n)\cdot\Biggl(\sum_{n=0}^{\infty}\frac{|M_n^{a,b}(\mathbb{F}_q)|}{|\mathrm{GL}_n(\mathbb{F}_q)|}\Biggr)\Biggr|_{q\mapsto q^{-1}}}_{\text{point count}}\;=\;\underbrace{Z_{a,b}(q)}_{q\text{-series}}\;=\;\underbrace{P_{a,b}(q)}_{\text{theta quotient}}$$ If true, the point count on $X^a=Y^b$ is essentially a modular function on $Γ(a+b)$. The conjecture is layered in $a$, with an identity for each $b$. The $a=2$ layer is classical, including identities of Rogers--Ramanujan and Andrews--Gordon. For $a\geq3,$ nothing was known. We prove the $a=3$ layer in full: a new infinite family of Rogers--Ramanujan identities, and a geometric origin for Warnaar's products. AxiomProver verified these new identities in Lean assuming existing literature.

In 2016, Berkovich and Uncu proved that, for all nonnegative integers $i$, $j$, and $n$, the number of strict partitions of $n$ with $i$ odd-indexed odd parts and $j$ even-indexed odd parts equals the number of strict partitions of $n$ with $i$ parts congruent to $1$ modulo $4$ and $j$ parts congruent to $3$ modulo $4$. Their proof used generating functions, and they asked for a combinatorial proof. We answer their question with an explicit bijection, assembled from three classical ingredients: $2$-modular diagrams, an insertion algorithm of Chen, Gao, Ji, and Li, and Glaisher's bijection. AxiomProver autonomously formalized and verified the proof of the main theorem in Lean.

Erdős Problem 725 asks for an asymptotic formula for the number $L_{k,n}$ of ordered, labelled $k\times n$ Latin rectangles. Godsil and McKay proved that $L_{k,n}\sim (n!)^k((n)_k/n^k)^n(1-k/n)^{-n/2}e^{-k/2}$ for $k=o(n^{6/7})$. We provide a partial solution to Erdős Problem 725 by proving this asymptotic for every $k=o(n)$. More precisely, set $\widetilde A_{k,n}=(n!)^k((n)_k/n^k)^n\exp\{[n(H_n-H_{n-k})-k]/2\}$. For every $K(n)=o(n)$, uniformly for $0\leq k\leq K(n)$, we prove $\log(L_{k,n}/\widetilde A_{k,n})=O(k^2/n^2)$, with an absolute implied constant. The results of this paper have been formally verified in Lean.

For a finite simple graph $G$, let $t(G)$ be the largest order of an induced tree and let $g(G)$ be the girth. We prove three consecutive conjectures of DeLaViña's Graffiti.pc program. First, writing $\ell(v)$ for the independence number of the subgraph induced by the neighbourhood of $v$, we prove $t(G) \ge \lfloor g(G)/2 \rfloor - 1 + \max_{v \in V(G)} \ell(v)$. Second, if $\mathrm{Per}(G)$ is the periphery and $f(G) = \max_x d(x, \mathrm{Per}(G))$, we prove $t(G) \ge \frac{2}{3} g(G) + f(G)$, and establish the stronger integral bound $t(G) \ge f(G) + \lceil 2g(G)/3 \rceil$ when $G$ contains a cycle. Third, if $δ'(G)$ is the second-smallest degree, counted with multiplicity, then every connected non-tree graph satisfies $t(G) δ'(G) \ge g(G) + 1$. These are Conjectures 141, 142, and 143 of Written on the Wall II. Complete, machine-checked Lean 4 proofs of all three formal statements accompany the manuscript.

The spectral sensitivity $λ(f)$ of a Boolean function is the largest eigenvalue of the adjacency matrix of its sensitivity graph. It lower-bounds every standard measure of query complexity, and Aaronson, Ben-David, Kothari, Rao and Tal, who introduced it, asked whether block sensitivity is at most quadratic in it: is $bs(f)=O(λ(f)^{2})$? We show that it is not. We construct a total Boolean function on $2017584$ variables with $bs(f)\ge 14011$ and $λ(f)\le 89.0162$, so that $bs(f)\geλ(f)^{2.127}$, and hence by composition a family with $λ(f_n)\to\infty$ and $bs(f_n)=Ω(λ(f_n)^{2.127})$. The function is the indicator of a union of $k$ subcubes indexed by the vertices of a doubly regular tournament, and the freedom left in the construction is fixed by the Lovász local lemma. The main result has been formally verified in Lean. We also give numerical evidence that a member of the same family on $1255$ variables reaches an exponent near $2.20$, and exhibit a member on $30$ variables whose exponent already exceeds $2$ and whose spectral sensitivity can be computed exactly.

We give new lower bounds for the Shannon capacities of small odd cycles: $Θ(C_7)\geq3.258805369885\ldots$, $Θ(C_{11})\geq5.294502522149\ldots$, $Θ(C_{13})\geq6.302455083464\ldots$, $Θ(C_{15})\geq7.301600534487\ldots$, $Θ(C_{19})\geq9.357192705918\ldots$, $Θ(C_{21})\geq10.342455853338\ldots$, and $Θ(C_{23})\geq11.328224257774\ldots$. The bounds are obtained by an iterative procedure due to Gao (2026) which is based on a method by Itty, Rosin, Carstensen and Reichman (2026). The bounds are fully formalised in Lean.