arXiv++ Combinatorics

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.

The two-dimensional bandwidth minimization problem (2DBMP) seeks an injective embedding of a guest graph into a square grid that minimizes the maximum Manhattan distance over its edges. Heuristic methods can provide strong upper bounds, but these bounds do not by themselves certify optimality. We present an efficient exact SAT-based approach for 2DBMP that incrementally searches for the minimum feasible bandwidth and certifies optimality through satisfiability and unsatisfiability results. On the standard $\lceil\sqrt n\rceil \times \lceil\sqrt n\rceil$ host grid, under a 3600 s time limit, the proposed SAT approach certifies optimal bandwidths for 41 of 43 Regular instances and 42 of 93 Harwell--Boeing instances, achieving substantially broader optimality certification within the 3600 s time limit than a previous exact approach evaluated with a 72-hour time limit. In addition, it certifies three bandwidth values that improve all previously published comparison values considered in this study and establishes all three as optimal. We further evaluate the approach on alternative host geometries, namely $2\times\lceil n/2\rceil$ and $n\times n$ grids, to assess its effectiveness beyond the standard host. Overall, the results demonstrate that the proposed SAT approach provides an effective exact method for the small- and medium-sized benchmark instances considered in this study, with fewer than 400 vertices, while heuristic methods remain important for larger and more challenging instances.

Two graphs $G$ and $H$ are homomorphism indistinguishable over a graph class $\mathcal{F}$ if they admit the same number of homomorphisms from every graph in $\mathcal{F}$. A wide range of relaxations of graph isomorphism arise this way: isomorphism itself over the class of all graphs [Lovász, Acta Math. Hung. 1967], equivalence under the $k$-dimensional Weisfeiler-Leman algorithm over the graphs of treewidth $\leq k$ [Dvořák, J. Graph Theory 2010], and quantum isomorphism over planar graphs [Mančinska-Roberson, FOCS 2020]. Since the class $\mathcal{F}$ is typically infinite, it is not clear a priori whether homomorphism indistinguishability over $\mathcal{F}$ is decidable; for planar graphs it is undecidable. Every class for which decidability was previously known is sparse. We give the first decidability results for dense graph classes: We introduce the dense Weisfeiler-Leman algorithm that decides homomorphism indistinguishability over the class of graphs of cliquewidth $\leq k$, the dense counterpart of treewidth. This relation was not previously known to be decidable. The algorithm colors $k$-tuples of vertex subsets rather than $k$-tuples of vertices. Beyond the class of all graphs of cliquewidth $\leq k$, we prove a general meta-theorem: homomorphism indistinguishability over every $\mathsf{CMSO}_1$-definable graph class of bounded cliquewidth is decidable, in randomized exponential time. For classes of bounded linear cliquewidth the bound improves to $\mathsf{PSPACE}$, and we show this is tight by exhibiting such a class for which the problem is $\mathsf{PSPACE}$-complete. These are the first general algorithms for homomorphism indistinguishability over dense graph classes.

Lokshtanov, Ramanujan, Saurabh, and Zehavi [ICALP 2018] proved that for any CMSO formula $φ$, testing $φ$ on arbitrary graphs can be reduced to testing it on $(q,k)$-unbreakable graphs for appropriate parameters. Their proof is non-constructive, and they ask whether it can be made constructive. We prove that this is impossible: specifically, the parameter $q$ cannot be a computable function of $φ$.

The queen domination problem asks for the minimum number of queens required to attack all squares on an $n \times n$ chessboard. Once this optimal number is known, determining the number of distinct solutions up to isomorphism has also attracted considerable attention. Previous work has introduced specialized and highly optimized search procedures to address open instances of the problem. While efficient in terms of runtime, confidence in their computational results ultimately depends on the correctness of these specialized implementations, motivating approaches that additionally provide independently verifiable correctness certificates. To this end, we present a proof-producing SAT framework for the queen domination problem based on an encoding that introduces auxiliary variables representing whether rows, columns, diagonals, and anti-diagonals contain queens, thereby exposing the geometric structure of the problem to the SAT solver. The framework is further strengthened through a novel literal-ordering strategy, symmetry breaking, a modern Cube-and-Conquer framework, and a unified proof-generation and verification pipeline. Together, these techniques yield both high performance and independently verifiable correctness. Our results uncover and correct a discrepancy in the previously reported enumeration for $n=16$ and resolve the previously open case $n=19$.

Razborov's flag algebra method is a powerful tool for proving asymptotic inequalities in extremal graph theory, often reducing the task to finding a finite certificate by semidefinite programming. We present a machine-checked formalization of the method for finite simple graphs, together with a certificate-to-proof compiler that turns externally generated certificate data into algebraic proofs checked by Lean. The formalization covers the foundations of the method: partially labeled graphs, their densities in large graphs, the quotient algebra of density expressions, graph-limit semantics through positive homomorphisms, and the downward operators used to average out labels. The compiler treats the external semidefinite programming output as candidate data rather than trusted input: Lean independently computes the required density and multiplication facts, verifies positive semidefiniteness exactly over $\mathbb{Q}$, and carries out the algebraic normalization steps of flag-algebra proofs. Our case studies yield formal proofs of seven Turán-type upper bounds, including Mantel's theorem and the Erdős pentagon theorem, a $C_4$-density bound for triangle-free graphs, and edge-density bounds for $K_4$-free, $K_5$-free, and $C_5$-free graphs. Independently of the compiler, we formalize the matching constructions that complete the exact Turán densities of Mantel's theorem and the Erdős pentagon theorem, and prove two inequalities of Goodman. Our constrained semantics also prompted a meta-theoretic comparison of two ways of imposing graph constraints: building a hereditary constraint into the flag algebra from the start, or testing inequalities afterward on constrained graph limits with labels chosen at random. We state the resulting root-plantability criterion characterizing when the two approaches agree; a forthcoming paper will present the complete account.

Model checking is the automated verification of properties (specified in some modal logic) in labeled transition systems (LTSs); it is an essential tool in ensuring software systems function as intended. State spaces of software grow exponentially, and heuristics are needed to ensure model checking remains feasible in real-world applications. Heuristics, in turn, require a good understanding on the typical behaviour of LTSs. In this paper, we use random graph theory to create a probabilistic model of large LTSs. From a theoretical analysis of the creation of large LTSs, backed by empirical data from the Model Checking Contest, we endow these models with realistic parameter values. Then, we analyze the asymptotic behaviour of this model under LTL and CTL, two modal logics popular in model checking. We show that, depending on the precise model, as the size grows to infinity we either have a convergence law (for every formula, the probability that it holds converges to a limit) or a 0-1 law (...and this limit is 0 or 1). We also discuss the theoretical complexity of determining these limits, and give algorithms for doing so. These results are the starting point towards a deep theoretical understanding of typical LTS behaviour, and highlight the promising applicability of random graph theory to model checking. \keywords{Model checking \and Random graphs \and 0-1 laws

A graph class is $k$-WQO if its $k$-labeled graphs are well-quasi-ordered under label-preserving induced subgraph embeddings. We show that every hereditary graph class that is $2$-WQO has bounded clique-width. Combined with the recent result of Dumas and Lopez, this confirms a long-standing conjecture of Pouzet: A hereditary graph class is $2$-WQO if and only if it is $k$-WQO for all $k\geq 2$, if and only if it is $\forall$-WQO, that is, its labeled graphs are well-quasi-ordered for every possible well-quasi-ordered label set. Our proof builds on a recent structure/non-structure dichotomy for the model theoretic notion of monadic dependence by Dreier, Mählmann, and Toruńczyk. Through the non-structure characterization by forbidden induced subgraphs, we show that every hereditary $2$-WQO graph class is monadically dependent. Leveraging the Ramsey-theoretic structural properties provided by monadic dependence, we then establish bounded clique-width by ruling out the existence of large well-linked sets, which are the canonical obstructions for clique-width.

Monadic dependence is a proposed structural dividing line for fixed-parameter tractability of first-order model checking on hereditary graph classes. A graph class is \emph{monadically dependent} if the class of all graphs cannot be interpreted in its vertex-colored members using a fixed first-order formula. We prove two structural consequences of monadic dependence. First, every monadically dependent class has \emph{almost linear neighborhood complexity}: for every graph $G$ in the class and every set $A\subseteq V(G)$, the family $\{N_G(v)\cap A : v\in V(G)\}$ has size $|A|^{1+o(1)}$. Second, every $n$-vertex graph in a monadically dependent class has radius-1 merge-width $n^{o(1)}$. Here, merge-width is the decomposition parameter of Dreier and Toruńczyk based on construction sequences; its radius-$r$ version measures local reachability among parts through already resolved pairs. This settles the radius-1 case of the conjectured connection between monadic dependence and almost bounded merge-width and provides the first decomposition-based structural description of monadically dependent graph classes. Our proof is algorithmic: we give an $\mathcal{O}(n^5)$-time algorithm that, given an $n$-vertex graph $G$ such that $|\{N_G(v)\cap A : v\in V(G)\}|\le O(|A|^d)$ for every $A\subseteq V(G)$, computes a construction sequence witnessing radius-1 merge-width $\mathcal{O}(n^{1-1/d}\log n)$.

We study solution discovery in the token-sliding model from a logical and cost-value optimization perspective. In solution discovery, we are given a graph, an initial placement of $k$ tokens, and a movement budget $b$. The task is to find a reachable target configuration satisfying a prescribed condition. Our results are inspired by \textsc{Partial Vertex Cover Discovery}, where the condition is that the~$k$ tokens cover at least $t$ edges of the input graph. This objective is not merely a sum of independent occupied vertex contributions: each selected vertex contributes its degree, but edges with both endpoints selected have to be subtracted once. To capture this phenomenon, we introduce \textsc{FO Value Discovery}, an optimization problem in which the value of a selected tuple is given by unary vertex weights together with first-order definable correction terms. We further generalize the setting to \textsc{FO Cost-Value Decision}, where vertices carry both costs and values, and the task is to decide whether there is a tuple whose first-order value expression reaches a prescribed value threshold while respecting a cost bound. Finally, we study the parameterized complexity of \textsc{Partial Vertex Cover Discovery} and \textsc{Vertex Cover Discovery}. As a consequence of the logical meta-theorems, we obtain fixed-parameter tractability of \textsc{Partial Vertex Cover Discovery} on several graph classes, including classes of locally bounded cliquewidth. We also show that \textsc{Partial Vertex Cover Discovery} is W[1]-hard parameterized by $k+b$ and fixed-parameter tractable on $d$-degenerate graphs parameterized by $k+d$. For \textsc{Vertex Cover Discovery}, we prove NP-hardness on planar graphs, W[1]-hardness parameterized by the clique cover number, even when a clique cover is supplied with the input, and W[1]-hardness with respect to parameter cutwidth.

This theoretical note studies the finite axiomatizability of strict majority reasoning in finite social decision frames. Moss and Pedersen (2026) <doi: 10.48550/arXiv.2606.23853> introduce a coherence criterion that characterizes exactly when qualitative majority judgments are representable by a finitely additive measure. The question addressed here is whether that coherence criterion can be replaced, in the finite setting, by any bounded finite fragment. We prove that it cannot. For every $k\ge 1$, we construct a maximal standard frame whose shortest coherence violation has length exactly $2k+2$. Hence there is no uniform finite bound on the incoherence index of social decision frames, resolving Conjecture 5.7 stated by Moss and Pedersen (2026). The construction is geometric, in the sense that it proceeds via orthogonality and dimension in rational vector spaces, and self-contained: it isolates a symmetric family of half-sized voting blocs and extends it to a maximal frame in which every shorter balanced obstruction is excluded. Along the explicit infinite sequence of universe sizes obtained in the construction, this also establishes the middle-layer family predicted by Conjecture B.25 by Moss and Pedersen (2026). Together with the soundness and completeness theorem for the Moss-Pedersen minimal logic for strict majorities, this establishes that measurable social decision frames are not finitely axiomatizable in that language.

We study monadic dependence of binary relational structures including at least one antisymmetric relation. Our cornerstone result gives sufficient conditions for proving that a structure is monadically dependent by only considering some of its reducts, assuming they are structurally well-behaved and compatible enough. As an application, we consider some reorientation rules preserving monadic dependence of binary structures, as well as replacement of one antisymmetric relation with bounded independence number by another. Then, we apply our main (technical) result to the study of twin-width in two ways. First, generalizing the fact that twin-width boundedness is equivalent to being expandable by a linear order into a monadically dependent class, we prove that it is also equivalent to being expandable by an oriented graph with bounded independence number (for instance by a poset with bounded width or by a tournament), and that FO-model checking is fixed-parameter tractable on such an expansion. Second, we show delineation by twin-width for some new classes of oriented graphs, including oriented split graphs and local tournaments. In all these cases, we also obtain fixed-parameter tractability of FO-model checking.

We present Trellis: an autoformalization system that leverages LLM agents in a deterministically constrained workflow to enforce incremental progress in Lean autoformalization tasks through iterative refinement of natural language proofs. Our approach is motivated by the common mathematician's notion of what it means to have a rigorous proof in the first place: namely, that it would be routine to elaborate any part of the proof in further detail. The result is a system which aims to achieve reliable autoformalization on a modest budget and with generalist agents, with specialization to autoformalization coming not from any task-specific agent training but instead from a meaning-of-rigor inspired workflow enforced by process semantics. We link to an end-to-end Lean formalization of a recent Ramsey theory breakthrough produced by the process.

An infinite structure has the finite length property (over a given field) if, for each of its finite powers, chains of equivariant subspaces in the corresponding free vector space are bounded in length. Prior work showed that the countable pure set and the countable dense linear order without endpoints have this property. We generalise these results to (a) any structure approximated by finite substructures with few orbits, provided the field is of characteristic zero, and (b) any Fraïssé limit with free amalgamation in a finite vocabulary consisting of unary and binary relations, possibly expanded with a generic total order. As a special case, we deduce the finite length property of the Rado graph using both methods. We also describe some connections with function spaces, weighted register automata, and orbit-finite systems of linear equations.

Width-based automated theorem proving is a framework where counterexamples to graph-theoretic conjectures are searched width-wise relative to some graph width measure, such as treewidth or pathwidth. In a recent work it has been shown that dynamic programming algorithms operating on tree decompositions can be combined together with the purpose of width-based theorem proving. This approach can be used to show that several long-standing conjectures in graph theory can be tested in time \(2^{2^{k^{O(1)}}}\) on the class of graphs of treewidth at most \(k\). In this work, we give the first steps towards evaluating the viability of this framework from a practical standpoint. At the same time, we advance the framework in two directions. First, we introduce a state-canonization technique that significantly reduces the number of states evaluated during the search for a counterexample of the conjecture. Second, we introduce an early-pruning technique that can be applied in the study of conjectures of the form \(\mathcal{P}_1 \rightarrow \mathcal{P}_2\), for graph properties \(\mathcal{P}_1\) and \(\mathcal{P}_2\), where \(\mathcal{P}_1\) is a property closed under subgraphs. As a concrete application, we use our framework in the study of graph-theoretic conjectures related to coloring triangle-free graphs. In particular, our algorithm is able to show that Reed's conjecture for triangle-free graphs is valid on the class of graphs of pathwidth at most 5, and on graphs of treewidth at most 3. Perhaps more interestingly, our algorithm is able to construct in a completely automated way counterexamples to invalid strengthenings of Reed's conjecture. These are the first results showing that width-based automated theorem proving is a promising avenue in the study of graph-theoretic conjectures.

In this work, we introduce TreeWidzard, an engine for developing dynamic programming algorithms that decide graph-theoretic properties parameterized by treewidth and pathwidth. Besides providing a unified framework for algorithms deciding atomic graph-theoretic properties, our engine allows one to combine such algorithms for two purposes: to obtain dynamic programming algorithms for more complex graph properties, and to support treewidth-based automated theorem proving. Within this context, given the specification of a Boolean combination \(P\) of graph properties \(P_1, P_2, \ldots, P_r\), and a positive integer \(k\), our engine can be used to determine whether all graphs of treewidth at most \(k\) satisfy \(P\). The main goal of the present work is to provide a system description of TreeWidzard. In particular, we provide a step-by-step account of how to implement dynamic programming algorithms in our framework and how to combine these algorithms for model checking and automated theorem proving.

Combinatorial curve neighborhoods are somewhat foundational when setting up the quantum Schubert calculus for affine flag manifolds. In the specific case of type $A_1^{(1)}$, you can encode these neighborhoods entirely within the moment graph of the infinite dihedral group $D_\infty$. Building on the framework developed by Mihalcea and Norton, this paper presents a complete, axiom-free formalization of these combinatorial curve neighborhoods in Lean 4. Rather than just wrapping mathematical statements, we formalized $D_\infty$ directly as a Coxeter system to explicitly compute length functions and degree maps. Reachable sets are defined through edge chains bounded by specific degrees, and we ultimately characterize the curve neighborhood by the maximal vertices inside these sets. The core effort here lies in formally verifying the explicit combinatorial formulas for curve neighborhoods of arbitrary elements. Interestingly, by restricting our search space to finite sets, we also managed to extract a fully computable version of these neighborhoods.

We present a search for small Kochen-Specker (KS) sets in dimension 3, specifically targeting extensions of the 13-ray Yu-Oh set, which has been proven to be the minimal witness to state-independent contextuality. To enable this search, we introduce a novel SAT-based orderly generation framework integrating recursive canonical labeling (RCL) with the graph isomorphism tool NAUTY. We demonstrate that previous SAT approaches relying on lexicographical canonicity suffer from exponential scaling on canonical graphs. This limitation renders them intractable on the large instances (25 to 33 vertices) encountered in our search, whereas our RCL check maintains consistent millisecond-level performance, effectively eliminating the bottleneck. Overcoming this bottleneck allows us to perform the first exhaustive enumeration of all KS sets with up to 33 rays containing the complete 25-ray state-independent contextuality (SI-C) set obtained by rigid extensions of the Yu-Oh set in 1,641 CPU hours. We found and verified that the 33-ray set discovered by Schütte is the smallest three-dimensional KS set containing the complete 25-ray SI-C set. All non-existence results are backed by independently verifiable proof certificates via an extension of the DRAT proof format.

Tree-ordered weakly sparse models have recently emerged as a robust framework for representing structures in an ``almost sparse'' way, while allowing the structure to be reconstructed through a simple first-order interpretation. A prominent example is given by twin-models, which are bounded twin-width tree-ordered weakly sparse representations of structures with bounded twin-width derived from contraction sequences. In this paper, we develop this perspective further. First, we show that twin-models can be chosen such that they preserve linear clique-width or clique-width up to a constant factor. Then, we introduce \emph{merge-models}, a natural analog of twin-models for merge-width. Merge-models represent binary relational structures by tree-ordered weakly sparse structures. The original structures can then be recovered by a fixed first-order interpretation. A merge-model can be constructed from a merge sequence. Then, its radius-$r$ merge-width will be, up to a constant factor, bounded by the radius-$r$ width of the merge sequence from which it is derived. Finally, we show that twin-models arise naturally as special cases of merge-models, and that binary structures with bounded twin-width are exactly those having a loopless merge-model with bounded radius-$r_0$ merge-width (for some sufficiently large constant $r_0$).