arXiv++ Combinatorics

Local complement is a graph operation formalized by Bouchet which replaces the neighborhood of a chosen vertex with its edge-complement. This operation induces an equivalence relation on graphs; determining the size of the resulting equivalence classes is a challenging problem in general. Bouchet obtained formulas only for paths and cycles, and brute-force methods are limited to very small graphs. In this work, we extend these results by deriving explicit formulas for several broad families of distance-hereditary graphs, including complete multipartite graphs, clique-stars, and repeater graphs. Our approach uses a technique known as split decomposition to establish upper bounds on equivalence class sizes, and we prove these bounds are tight through a combinatorial enumeration of the graphs' decomposed structure up to symmetry.

We study "dead ends" in square-free digit walks: square-free integers $N$ such that, in base $b$, every one-digit extension $bN+d$ is non-square-free. In base $10$, the stochastic independence model of Miller et al. suggests that infinite square-free walks occur with probability near $1$, corresponding to an asymptotic dead-end density of $\approx 5.218\times 10^{-5}$. We prove that the true asymptotic dead-end density satisfies \[ c_{\mathrm{dead}} \approx 1.317\times 10^{-9}, \] roughly a factor of $\sim 4\times 10^4$ smaller than the prediction. For every base $b\geq 2$, we prove that dead-end densities exist and are given by a closed-form expression (as a finite alternating sum of Euler products). The argument is fully formalized in Lean/Mathlib, and was produced automatically by AxiomProver from a natural-language statement of the problem.

Let $S=\langle d_1,\dots,d_m\rangle$ be a numerical semigroup and $k[S]$ its semigroup ring. The Hilbert numerator of $k[S]$ determines normalized alternating syzygy power sums $K_p(S)$ encoding alternating power sums of syzygy degrees. Fel conjectured an explicit formula for $K_p(S)$, for all $p\ge 0$, in terms of the gap power sums $G_r(S)=\sum_{g\notin S} g^r$ and universal symmetric polynomials $T_n$ evaluated at the generator power sums $σ_k=\sum_i d_i^k$ (and $δ_k=(σ_k-1)/2^k$). We prove Fel's conjecture via exponential generating functions and coefficient extraction, solating the universal identities for $T_n$ needed for the derivation. The argument is fully formalized in Lean/Mathlib, and was produced automatically by AxiomProver from a natural-language statement of the conjecture.

This paper develops an invariant--geometric interpretation of the canonization problem for simple undirected weighted graphs based on the {discrete moving frame method} for finite groups. We consider the action of the {pair group} $S_n^{(2)}$ on the space of edge weights of a graph. It is emphasized that the classical algebraic approach aimed at describing the ring of polynomial invariants of this action quickly becomes computationally impractical due to the explosive growth in the number and degrees of generators. The main result is a formalization of a canonical labeling of a graph as a {discrete moving frame} in the sense of Olver: a discrete orbit cross-section is fixed, in particular by a lexicographic rule, and for each configuration of edge weights one defines a permutation in $S_n^{(2)}$ that maps it to its canonical representative. The coordinates of the canonical representative are interpreted as a {complete system of invariants} for the action of $S_n^{(2)}$ that separates orbits, i.e., isomorphism classes of graphs. It is shown that the invariants obtained via such orbit canonization are of a non-algebraic nature and belong to the class of {semi-algebraic functions}. We do not propose a new computational algorithm; instead, we provide a rigorous theoretical foundation for the very concept of canonization by viewing it as a process of constructing a discrete moving frame and the corresponding system of semi-algebraic invariants.

This document is a blueprint for the formalization in Lean of the structural theory of regular matroids underlying Seymour's decomposition theorem. We present a modular account of regularity via totally unimodular representations, show that regularity is preserved under $1$-, $2$-, and $3$-sums, and establish regularity for several special classes of matroids, including graphic, cographic, and the matroid $R_{10}$. The blueprint records the logical structure of the proof, the precise dependencies between results, and their correspondence with Lean declarations. It is intended both as a guide for the ongoing formalization effort and as a human-readable reference for the organization of the proof.

Vizing's theorem states that every simple undirected graph can be edge-colored using fewer than $Δ+ 1$ colors, where $Δ$ is the graph's maximum degree. The original proof was given through a polynomial-time algorithmic procedure that iteratively extends a partial coloring until it becomes complete. In this work, I used the Lean theorem prover to produce a verified implementation of the Misra and Gries edge-coloring algorithm, a modified version of Vizing's original method. The focus is on building libraries for relevant mathematical objects and rigorously maintaining required invariants.

Webs are a kind of planar, directed, edge-labeled graph that encode invariant vectors for quantum representations of $\mathfrak{sl}_n$. The theory of webs developed organically for $\mathfrak{sl}_2$, where they are also known as noncrossing matchings and the Temperley-Lieb algebra, before being formalized by Kuperberg for $\mathfrak{sl}_2$ and $\mathfrak{sl}_3$ as the morphisms in a diagrammatic categorification of quantum representations called the spider category. Various models extend webs to $n \geq 4$. Only Cautis-Kamnitzer-Morrison prove a full set of relations for their webs, though Fontaine's webs are better adapted to computations, more graph-theoretically natural, and directly generalize webs for $n=2$ and $n=3$. This paper formalizes the theory of Fontaine's webs, proving the existence of a deep and powerful global structure on these webs called strandings. We do three key things: 1) give a state-sum formula to construct ($U_q(\mathfrak{sl}_n)$-invariant) web vectors from the orientation of strandings on Fontaine's webs; 2) list and prove a complete set of relations, connecting strandings to the local data of binary labelings that are well-established in the literature; and 3) provide applications and examples of how strandings facilitate computations.

In a seminal work, Cheng and Xu showed that if $S$ is a square or a triangle with a certain property, then for every positive integer $r$ there exists $n_0(S)$ independent of $r$ such that every $r$-coloring of $\mathbb{E}^n$ with $n\ge n_0(S)$ contains a monochromatic or a rainbow congruent copy of $S$. Gehér, Sagdeev, and Tóth formalized this dimension independence as the canonical Ramsey property and proved it for all hypercubes, thereby covering rectangles whose squared aspect ratio $(a/b)^2$ is rational. They asked whether this property holds for all triangles and for all rectangles. (1) We resolve both questions. More precisely, for triangles we confirm the property in $\mathbb{E}^4$ by developing a novel rotation-sphereical chaining argument. For rectangles, we introduce a structural reduction to product configurations of bounded color complexity, enabling the use of the simplex Ramsey theorem together with product Ramsey theorem. (2) Beyond this, we develop a concise perturbation framework based on an iterative embedding coupled with the Frankl-Rödl simplex super-Ramsey theorem, which yields the canonical Ramsey property for a natural class of 3-dimensional simplices and also furnishes an alternative proof for triangles.

Seymour's decomposition theorem is a hallmark result in matroid theory presenting a structural characterization of the class of regular matroids. Formalization of matroid theory faces many challenges, most importantly that only a limited number of notions and results have been implemented so far. In this work, we formalize the proof of the forward (composition) direction of Seymour's theorem for regular matroids. To this end, we develop a library in Lean 4 that implements definitions and results about totally unimodular matrices, vector matroids, their standard representations, regular matroids, and 1-, 2-, and 3-sums of matrices and binary matroids given by their standard representations. Using this framework, we formally state Seymour's decomposition theorem and implement a formally verified proof of the composition direction in the setting where the matroids have finite rank and may have infinite ground sets.

In a seminal work, Cheng and Xu proved that for any positive integer \(r\), there exists an integer \(n_0\), independent of \(r\), such that every \(r\)-coloring of the \(n\)-dimensional Euclidean space \(\mathbb{E}^n\) with \(n \ge n_0\) contains either a monochromatic or a rainbow congruent copy of a square. This phenomenon of dimension-independence was later formalized as the canonical Ramsey property by Geheér, Sagdeev, and Tóth, who extended the result to all hypercubes, and to rectangles whose side lengths \(a\), \(b\) satisfy \((\frac{a}{b})^2\) is rational. They further posed the natural problem of whether every rectangle admits the canonical Ramsey property, regardless of the aspect ratio. In this paper, we show that all rectangles exhibit the canonical Ramsey property, thereby completely resolving this open problem of Geheér, Sagdeev, and Tóth. Our proof introduces a new structural reduction that identifies product configurations with bounded color complexity, enabling the application of simplex Ramsey theorems and product Ramsey amplification to control arbitrary aspect ratios.

The relationship between the concepts of network and knowledge graph is explored. A knowledge graph can be considered a special type of network. When using a knowledge graph, various networks can be obtained from it, and network analysis procedures can be applied to them. RDF is a formalization of the knowledge graph concept for the Semantic Web, but some of its solutions are also extensible to a format for describing general networks.

In this work, we present two results: The first result is the formalization of Tutte's theorem in Lean, a key theorem concerning matchings in graph theory. As this formalization is ready to be integrated in Lean's mathlib, it provides a valuable step in the path towards formalizing research-level mathematics in this area. The second result is a framework for doing educational formalization projects. This framework provides a structure to learn to formalize mathematics with minimal teacher input. This framework applies to both traditional academic settings and independent community-driven environments. We demonstrate the framework's use by connecting it to the process of formalizing Tutte's theorem.

Frankl's conjecture, also known as the union-closed sets conjecture, can be equivalently expressed in terms of intersection-closed set families by considering the complements of sets. It posits that any family of sets closed under intersections, and containing both the ground set and the empty set, must have a ``rare vertex'' -- a vertex belonging to at most half of the members of the family. The concept of \emph{average rarity} describes a set family where the average degree of all the elements is at most half of the number of its members. Average rarity is a stronger property that implies the existence of a rare vertex. This paper focuses on ideal families, which are set families that are downward-closed (except the ground set) and include the ground set. We present a proof that the normalized degree sum of any ideal family is non-positive, which is equivalent to saying that every ideal family satisfies the average rarity condition. This proof is formalized and verified using the Lean 4 theorem prover.

Generalized abelian equivalence compares words by their factors up to a certain bounded length. The associated complexity function counts the equivalence classes for factors of a given size of an infinite sequence. How practical is this notion? When can these equivalence relations and complexity functions be computed efficiently? We study the fixed points of substitution of Pisot type. Each of their $k$-abelian complexities is bounded and the Parikh vectors of their length-$n$ prefixes form synchronized sequences in the associated Dumont--Thomas numeration system. Therefore, the $k$-abelian complexity of Pisot substitution fixed points is automatic in the same numeration system. Two effective generic construction approaches are investigated using the \texttt{Walnut} theorem prover and are applied to several examples. We obtain new properties of the Tribonacci sequence, such as a uniform bound for its factor balancedness together with a two-dimensional linear representation of its generalized abelian complexity functions.

The aim of the present paper is to extend the concept of a congruence from lattices to posets. We use an approach different from that used by the first author and V. Snášel. By using our definition we show that congruence classes are convex. If the poset in question satisfies the Ascending Chain Condition as well as the Descending Chain Condition, then these classes turn out to be intervals. If the poset has a top element 1 then the 1-class of every congruence is a so-called strong filter. We study congruences on relatively pseudocomplemented posets which form a formalization of intuitionistic logic. For such posets we define so-called deductive systems and we show how they are connected with congruence kernels. We prove that every strong filter F of a relatively pseudocomplemented poset induces a congruence having F as its kernel. Finally, we consider Boolean posets which form a natural generalization of Boolean algebras. We show that congruences on Boolean posets in general do not share properties known from Boolean algebras, but congruence kernels of Boolean posets still have some interesting properties.

We use the automatic theorem prover Walnut to resolve various open problems from the OEIS and beyond. Specifically, we clarify the structure of sequence A260311, which concerns runs of sums of upper Wythoff numbers. We extend a result of Hajdu, Tijdeman, and Varga on polynomials with nonzero coefficients modulo a prime. Additionally, we settle open problems related to the anti-recurrence sequences A265389 and A299409, as well as the subsumfree sequences A026471 and A026475. Our findings also give rise to new open problems.

Hofstadter's $G$ function is recursively defined via $G(0)=0$ and then $G(n)=n-G(G(n-1))$. Following Hofstadter, a family $(F_k)$ of similar functions is obtained by varying the number $k$ of nested recursive calls in this equation. We study here some Fibonacci-like sequences that are deeply connected with these functions $F_k$. In particular, the Zeckendorf theorem can be adapted to provide digital expansions via sums of terms of these sequences. On these digital expansions, the functions $F_k$ are acting as right shifts of the digits. These Fibonacci-like sequences can be expressed in terms of zeros of the polynomial $X^k{-}X^{k-1}{-}1$. Considering now the discrepancy of each function $F_k$, i.e., the maximal distance between $F_k$ and its linear equivalent, we retrieve the fact that this discrepancy is finite exactly when $k \le 4$. Thanks to that, we solve two twenty-year-old OEIS conjectures stating how close the functions $F_3$ and $F_4$ are from the integer parts of their linear equivalents. Moreover we establish that $F_k$ can coincide exactly with such an integer part only when $k\le 2$, while $F_k$ is almost additive exactly when $k \le 4$. Finally, a nice fractal shape a la Rauzy has been encountered when investigating the discrepancy of $F_3$. Almost all this article has been formalized and verified in the Coq/Rocq proof assistant.

In the critical beta-splitting model of a random $n$-leaf rooted tree, clades are recursively split into sub-clades, and a clade of $m$ leaves is split into sub-clades containing $i$ and $m-i$ leaves with probabilities $\propto 1/(i(m-i))$. Study of structure theory and explicit quantitative aspects of the model is an active research topic. It turns out that many results have several different proofs, and detailed studies of analytic proofs are given elsdewhere (via analysis of recursions and via Mellin transforms). This article describes two core probabilistic methods for studying $n \to \infty$ asymptotics of the basic finite-$n$-leaf models. (i) There is a canonical embedding into a continuous-time model, that is a random tree CTCS(n) on $n$ leaves with real-valued edge lengths, and this model turns out to be more convenient to study. The family (CTCS(n), $n \ge 2)$ is consistent under a ``delete random leaf and prune" operation. That leads to an explicit inductive construction (the {\em growth algorithm}) of (CTCS(n), $n \ge 2)$ as $n$ increases, and then to a limit structure CTCS$(\infty)$ which can be formalized via exchangeable partitions, in some ways analogous to the Brownian continuum random tree. (ii) There is an explicit description of the limit fringe distribution relative to a random leaf, whose graphical representation is essentially the format of the cladogram representation of biological phylogenies.

We present a library of formalized results around symmetric functions and the character theory of symmetric groups. Written in Coq/Rocq and based on the Mathematical Components library, it covers a large part of the contents of a graduate level textbook in the field. The flagship result is a proof of the Littlewood-Richardson rule, which computes the structure constants of the algebra of symmetric function in the schur basis which are integer numbers appearing in various fields of mathematics, and which has a long history of wrong proofs. A specific feature of algebraic combinatorics is the constant interplay between algorithms and algebraic constructions: algorithms are not only in computations, but also are key ingredients in definitions and proofs. As such, the proof of the Littlewood-Richardson rule deeply relies on the understanding of the execution of the Robinson-Schensted algorithm. Many results in this library are effective and actually used in computer algebra systems, and we discuss their certified implementation.

The procedure for simulating the nuclear magnetic resonance spectrum linked to the spin system of a molecule for a certain nucleus entails diagonalizing the associated Hamiltonian matrix. As the dimensions of said matrix grow exponentially with respect to the spin system's atom count, the calculation of the eigenvalues and eigenvectors marks the performance of the overall process. The aim of this paper is to provide a formalization of the complete procedure of the simulation of a spin system's NMR spectrum while also explaining how to diagonalize the Hamiltonian matrix with a quantum computer, thus enhancing the overall process's performance. Two well-known quantum algorithms for calculating the eigenvalues of a matrix are analyzed and put to the test in this context: quantum phase estimation and the variational quantum eigensolver. Additionally, we present simulated results for the later approach while also addressing the hypothetical noise found in a physical quantum computer.