arXiv++ Combinatorics

Let $k$ be a field of characteristic $p\ge0$. We prove that $m$ points and $n$ lines in $k^2$ determine at most $3(mn)^{2/3}+m+n+2mn/p$ incidences, the last term being omitted in characteristic zero. Over the prime field $\mathbb{F}_p$ the coefficient of $mn/p$ can be replaced by $1$. The proof uses the polynomial method, and for $m=n$ the bound is sharp up to an absolute constant over prime fields. As applications, over prime fields in which $-1$ is not a square we obtain the $L^2\to L^r$ extension estimate for the paraboloid in $\mathbb{F}_p^3$ for $r>10/3$. Over every odd prime field, we show that a two-source extractor construction of Bourgain has exponentially small error at every min-entropy rate greater than $1/3$. We also improve sum-product estimates for small sets in positive characteristic and obtain projection and Furstenberg estimates over prime fields. The incidence inequalities with exact constants have been formalized in Lean.

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. Zhang has given a complete proof of this conjecture by a centered pseudoinverse and spectral variance method. We present an independently obtained, structurally different proof of the strict even-dimensional inequality. Starting from the structural identities of Frankel and Urschel, we derive an exact global defect budget and combine binary rounding, fixed intersections, and Gram projection. A ten-row obstruction handles every even $n\ge66$; a finite exact calculation handles $4\le n\le64$, $n\ne6$; and a multi-column energy argument treats $n=6$. The order-two case is elementary. The even-dimensional argument is formalized in Lean 4, conditional on Frankel--Urschel Lemma 2.1 as an explicit external mathematical input. The finite evaluations use Lean's native evaluator; their trust boundary and exact certificates are documented. Together with Cheng's odd-dimensional theorem, the argument recovers the full S-matrix theorem and its equality characterization.

We prove Sabidussi's compatibility conjecture. Let $G$ be a finite connected multigraph in which every vertex has even degree and the minimum degree is at least four, and let $T$ be an Euler tour of $G$. The edges of $G$ can be partitioned into circuits (connected $2$-regular subgraphs) so that no circuit contains two edges used consecutively anywhere in $T$. In fact, the edges can be four-coloured so that every such pair receives different colours and every colour class has even degree at every vertex. We use a counting argument based on the Chevalley-Warning theorem to show that a four-colouring with the required properties exists. Splitting each colour class into circuits then gives the desired compatible decomposition. Formalization in Lean 4 is also available in the author's github.

In 1965, D. H. Lehmer conjectured that the permutations of every multiset admit an imperfect Hamiltonian traversal by adjacent swaps: a walk in the neighbor-swap graph that visits every word, with some words visited twice in order to reach a neighbor and return. The question is posed as an unsolved research problem in Knuth's Art of Computer Programming. Verhoeff (2017) chose the stutter words, in which every domino is a double, as the words to be reached this way, and reformulated the conjecture as the Hamiltonicity of the graph $N(S)$ on the non-stutter words, with two exceptional families --- binary signatures with an odd multiplicity, and the permutations of $(2k,1,1)$ --- that admit a Hamiltonian path but no cycle. This article proves the reformulated conjecture, and with it Lehmer's conjecture. The key structure is a partition of the words into hypercubes: the swaps inside dominoes turn each class of words with the same domino contents into a hypercube, and the stutters are exactly the $0$-dimensional classes. When every multiplicity is even, Hamiltonian cycles of the hypercubes are glued along a spanning tree, with no finite check. The case of exactly one odd multiplicity reduces to the all-even case and to a theorem of Stachowiak (1992), the one inherited Hamiltonicity input, which also settles two or more odd multiplicities. The only finite ingredients are two explicit cycles, of 28 and 84 words. Every construction is implemented in Python and checked against brute-force graphs, and the proof is formalized in Lean 4 over Mathlib.

For a graph $H$, let $f(n,e,H)$ be the least number of colors in an edge-coloring of some $n$-vertex graph with at least $e$ edges in which every copy of $H$ is rainbow. Burr, Erdős, Graham, and Sós conjectured that $f(n,\lfloor n^2/4\rfloor+1,C_{2k+1})=(1/8+o(1))n^2$ for every fixed $k\ge3$, and Bucić, Chen, and Ma recently proved this for all $k\ge4$. We prove the remaining case $k=3$: \[ f\left(n,\left\lfloor n^2/4\right\rfloor+1,C_7\right) =\left(\frac18+o(1)\right)n^2. \] The lower bound rests on a weighted palette inequality, which we prove with an exact rational certificate on five sampled vertices. Its main ingredients are a fractional matching of compatible triangular edges and private resources attached to nontriangular edges. A stable form of the inequality, combined with regularity, triangle removal, and a direct argument for graphs close to bipartite, transfers the bound to arbitrary edge-colorings. We also describe a Lean 4 formalization of the conjecture for every fixed $k\ge3$, which combines the new seven-cycle proof with a formalization of the Bucić-Chen-Ma argument for $k\ge4$.

The stacking number of a graph is the least integer t >= 2 such that every configuration of t pebbles can be transformed by pebbling moves into a configuration supported on one vertex. We prove that, for every finite tree T with at least two vertices, this number equals the rooted distance-and-degree estimator conjectured by Csernák and Soukup. The proof uses an exact recursive characterization of stackability at a prescribed vertex, an explicit zero-score obstruction, and a weighted cancellation argument for arbitrary nonstackable configurations. The complete theorem is formalized in Lean 4; the formal result has also passed Palomar mechanical verification and is publicly registered as PALOMAR-2026-09-25-000010.

Autocatalysis, the ability of a chemical subsystem to sustain its own constituents when supplied with sufficient food molecules, has been closely related to the origin of life on Earth. Emerging from Wilhelm Ostwald's considerations about an explicit autocatalytic reaction, different notions of autocatalysis have been developed over the years. The two most prominent are reflexively autocatalytic F-generated sets (RAFs) and stoichiometric autocatalysis. After having shown that each RAFs is, under reasonable conditions, in general stoichiometrically autocatalytic, we examine here the relationship between the two notions of minimality: irreducible RAFs and autocatalytic cores. To this end, we overcome the obstacle that RAFs and stoichiometric autocatalysis have been formalized in distinct systems of chemical reactions, i.e., catalytic reaction systems (CRS) and chemical reaction networks (CRNs), respectively. We show that reactions in a CRS constitute equivalence classes of reactions of the corresponding CRNs w.r.t. their specific catalyzations. Using the fact that CRN and CRS can be canonically identified whenever each CRS reaction is associated with a single catalyzation, we demonstrate that the Kőnig graph of a monocatalyzed, irreducible RAF is composed of strong blocks devoid of food and waste species that are separated by reaction vertices, each of which contains an autocatalytic core. In fact, a single irreducible RAF can, in general, contain exponentially many autocatalytic cores.

Godsil, Roberson, Šámal and Severini conjectured that the quantum chromatic number of the categorical product of two graphs equals the minimum of the quantum chromatic numbers of the factors. We disprove this conjecture: we construct explicit finite graphs $G,H$ with \[ χ(G\times H) \leq 1538 < 1539 = \min(χ_q(G),χ_q(H)).\]The graphs are obtained from Zhu's counterexample to Hedetniemi's conjecture by using a base graph for which the Lovász theta number of the complement, and not only the fractional chromatic number, is large. The lower bound for the first factor is the theta bound. For the second factor we adapt Zhu's argument to projections that do not commute: the step that fixes the colors of a clique is replaced by identities between operators. Both lower bounds hold for colorings by projections in an arbitrary nonzero unital $C^*$-algebra. Hence the conjecture also fails for the spatial, approximate, commuting-operator and $C^*$-algebraic variants of the quantum chromatic number. We also give smaller counterexamples certified by exact integer data. The graph constructions, the certificates and the counterexample statements in the projective formulation are formalized in Lean~4.

We prove the conjecture of Huang, Jiang, and Oblomkov (HJO) giving a geometric extension of the Rogers--Ramanujan and Andrews--Gordon identities for every torus-knot singularity $X^a=Y^b$ with coprime $1<a<b.$ For a prime power $q$, let $\mathcal{NC}_n^{a,b}(\mathbb F_q)$ denote the set of pairs of commuting nilpotent $n\times n$ matrices $(A,B)$ over $\mathbb F_q$ satisfying $A^a=B^b$. We establish the threefold equality between their normalized counts, the HJO $q$-series $Z_{a,b}$, and the explicit infinite product $P_{a,b}$: \[ \underbrace{\vphantom{\Bigg|} \prod_{m\geq1}(1-q^{-m}) \Biggl(\sum_{n=0}^{\infty} \frac{\lvert\mathcal{NC}_n^{a,b}(\mathbb F_q)\rvert} {\lvert\operatorname{GL}_n(\mathbb F_q)\rvert}\Biggr) }_{\text{point count}} = \underbrace{\vphantom{\Bigg|}Z_{a,b}(q^{-1}) }_{\text{\(q\)-series}} = \underbrace{\vphantom{\Bigg|}P_{a,b}(q^{-1}) }_{\text{infinite product}}. \] Our main result is a stronger finite identity: the rank $N$ HJO sum equals $(q;q)_N$ times the generating function for balanced cylindric partitions with entries bounded by $N$. Taking $N\to\infty$ yields the HJO conjecture. The proof combines the compositional rational shuffle theorem of Bergeron--Garsia--Leven--Xin and Mellit with a multiplicativity theorem for slope operators and a determinantal model for bounded cylindric partitions, linked by a common $q$-difference equation. The finite identity and the HJO conjecture have been formalized in Lean by AxiomProver, conditional on two stated literature inputs.

A Leech tree of order $n$ is a tree with positive integral edge weights whose $n(n-1)/2$ pairwise weighted distances are precisely $1,2,\ldots,n(n-1)/2$. This paper gives a computer-assisted proof that no Leech tree of order $18$ exists. The argument has three layers. First, a development in Lean 4 verifies the structural facts used in the paper. These facts reduce every putative example to one of eight local configurations and justify several necessary conditions. Second, conventional mathematical arguments prove a component-pair whole-block exact-cover condition and the completeness of a recursive search. Third, exhaustive computations close all eight configurations. The computation records exact coverage, source and input hashes, terminal receipts, and checked exact-zero results. The structural layer is kernel-checked, but the search program, its execution, and the certificate checker have not been formalized in Lean. The result is therefore a computer-assisted proof, not an end-to-end Lean proof.

We prove that a path maximizes the expected range of a uniformly chosen graph homomorphism into the integers, with one vertex pinned at zero, among all connected bipartite graphs of the same order. This establishes the expectation form of the Benjamini--Häggström--Mossel conjecture. The proof restricts and rescales a homomorphism on each bipartition class, then contracts the edges on which the resulting height function is constant. A quantitative estimate for the rank of these zero edges compensates for a parity term in the expected range of a simple random walk, allowing an induction on the number of vertices. We then prove that the BHM inequality implies the Loebl--Ne\v set\v ril--Reed inequality for uniformly chosen integer 1-Lipschitz functions on arbitrary connected graphs, and hence obtain the LNR conjecture as a corollary of BHM. The proof was obtained through interaction with OpenAI GPT-6 Astra and verified by the author. The main results have also been formalized and checked in Lean~4.

Recent major breakthroughs in $q,t$-combinatorics include the introduction of the Dyck path algebra $\mathbb{A}_{q,t}$ by Carlsson and Mellit and of the Catalanimals by Blasiak et al., both of which led, among other things, to independent proofs of different extensions of the rational shuffle conjecture of Bergeron et al. The first main contribution of this paper is a simple, explicit formula inside the algebra $\mathbb{A}_{q,t}$ for the Negut operators, yielding a direct, elementary connection between the original operators of the rational shuffle conjecture and the corresponding Catalanimals. Our formula bypasses the elliptic Hall algebra, turning these operators into transparent, workable tools whose action we can compute exactly and efficiently on any symmetric function, not just constants. Our second main contribution consists of a series of explicit formulas relating the Negut operators to the Theta operators introduced by D'Adderio et al. To prove these formulas, we provide an extension of the aforementioned Theta operators to the entire algebra $\mathbb{A}_{q,t}$, allowing us to obtain a series of new combinatorial results. The algebraic computations underlying this extension have been formalized in Lean. To showcase the power of our results, we give a proof, also partially formalized in Lean, of the Theta conjecture of D'Adderio et al., first stated in 2019.

We prove the Colomo-Pronko conjecture for alternating sign matrices with a prescribed square of zeros at a corner, for all matrix sizes and freezing parameters. A known multiple-integral formula for the frozen-corner count yields determinant representations built from fixed polynomial kernels. We relate these kernels to the conjectured determinant through an inverse identity for the commutator of a signed Pascal matrix with reversal. In odd dimension, the comparison uses the one-dimensional nullspace and projection along it to eliminate the central coordinate. Combined with the asymptotic analysis of Colomo and Pronko, our result removes the conjectural assumption from their GUE Tracy-Widom fluctuation theorem for the intersection of the frozen boundary with the main diagonal in uniformly random alternating sign matrices. The finite-dimensional algebraic core of the proof has been formalized in Lean 4.

Kolokolnikov conjectured that, among all simple graphs on \(n\) vertices with exactly \(2(n-2)\) edges, the complete bipartite graph maximizes algebraic connectivity. This paper proves the conjecture. The underlying Lean~4 formalization was generated with MerLean and checked by the Lean kernel.

We classify the polyominoes obtained by adjoining four straight arms to a single square, allowing zero arm lengths, according to their ability to tile rectangles, half-strips, bent strips, quadrants, strips, half-planes, and the plane. We also classify their ability to tile an integer enlargement of themselves. Tiles occupy whole square-grid cells; translations, rotations, and reflections are permitted. Exactly five capability profiles occur. For the family $P(n,1,1,0)$, the rectangle profile holds for $n\le3$ and the bent-strip profile, with no half-strip or rep-tiling, for every $n\ge4$. A cross with four positive arms tiles the plane precisely when two opposite arms have length one; it never tiles a half-plane. Explicit periodic constructions and geometric obstructions are combined with finite symbolic case certificates. A Lean 4 development verifies the full classification for every natural four-tuple, including the interpretation of the certificates as statements about arbitrary infinite tilings. The account incorporates the author's 2020--2021 L- and T-polyomino work, reconstructs Dahlke's gun argument, and documents the subsequent AI-assisted proof development and formalization.

Pate proved ordinary irreducible-immanant permanental dominance through order $13$ and identified $(4,4,3,3)$ as the sole remaining order-$14$ case, with $(5,4,3,3)$ and $(3^5)$ forming the order-$15$ frontier. These three cases are settled here; consequently $d_λ(A)/f^λ\le \operatorname{per}(A)$ for every partition $λ\vdash n$ with $n\le15$ and every complex Hermitian positive-semidefinite matrix $A$. The argument also yields results beyond this finite frontier: an exact four-term bridge for $(4,4,3,3)$, the uniform family $(m,4,3,3)$, a two-parameter family $(a,b,3,3)$ for $a\ge b\ge4$ and $5a\ge8b$, and a long-first-row criterion for arbitrary fixed tails. These results arise from explicit specializations of Pate's $W$-function positivity framework using partial swaps, Young projectors, Pieri--content identities, and branching data. For $(3^5)$, an exact Farkas certificate shows that the central-projector partial-swap cone is insufficient; a branching-refined one-swap construction escapes this obstruction and yields a positive $106+19$-witness certificate. Boundary-compression and node-moving results further describe the reach and limitations of the local-filter method. All finite certificates are checked by exact integer or rational arithmetic and are supplied as ancillary material. The order-$14$ bridge is additionally formalized and kernel-checked in Lean 4 for all complex Hermitian positive-semidefinite matrices, including the exact coefficient normalization and the deduction of $(4,4,3,3)$ permanental dominance from four explicitly stated Pate inequalities.

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.

We prove the conjecture of Borowiecki and Broere that every finite simple planar graph admits a generalized total coloring with four colors: a proper vertex coloring with four colors together with an edge coloring with four colors in which each edge color class is a forest and no edge receives the color of either endpoint. In fact every proper four-coloring of such a graph extends to an edge coloring of the required kind. The proof combines a component-count inequality for planar graphs whose vertices are partitioned into four independent sets, obtained by completing to a triangulation, with the matroid partition theorem applied to four graphic matroids. A Lean 4 formalization relative to six named background assumptions is described below.

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.