arXiv++ Combinatorics

We develop a directional formalism for the partition graph G_n based on several canonical reference sets: the main chain, the self-conjugate axis, the spine, and the boundary framework. For each such set S, the graph distance d_S induces a shell structure and a local trichotomy of edges into inward, outward, and level classes. Passing from edges to paths, we define directional corridors as monotone inward geodesics toward a chosen reference set and prove that every vertex admits at least one. We then prove a structural non-equivalence theorem: for connected G_n, two nonempty reference sets induce the same edgewise directional field if and only if the difference of their distance functions is constant; in particular, distinct reference sets induce distinct directional fields. This gives a first precise formalization of anisotropy in G_n. We also show that every bounded neighborhood of a reference set is accessible by a monotone inward corridor, which gives a directional interpretation to previously established controlled regions around the axis, the spine, and the framework. Finally, we complement the strict theory with a computational atlas illustrating edgewise directional statistics, directional mixing, local invariant drift, and corridor-based transport profiles.

We prove that the directed 3-torus D_3(m), or equivalently the Cartesian product of three directed m-cycles, admits a decomposition into three arc-disjoint directed Hamilton cycles for every integer m >= 3. The proof reduces Hamiltonicity to the m-step return maps on the layer section S=i+j+k=0. For odd m, five Kempe swaps of the canonical coloring produce return maps that are explicitly affine-conjugate to the standard 2-dimensional odometer. For even m, a sign-product invariant rules out Kempe-from-canonical constructions, and a different low-layer witness reduces after one further first-return map to a finite-defect clock-and-carry system. The remaining closure is a finite splice analysis, and the case m=4 is handled separately by a finite witness. A Lean 4 formalization accompanies the construction.

We prove Ehrenborg's conjecture that every connected bipartite graph $G$ with parts of size $m$ and $n$ has at most $\frac{1}{mn}\prod_{v\in V(G)} \operatorname{deg}(v)$ spanning trees, and that equality holds if and only if $G$ is a Ferrers graph. The proof is fully formalized in Lean 4.

These lecture notes provide an introduction to combinatorics on words and its interactions with dynamics, algebra, and arithmetic. The central theme is the notion of low factor complexity for infinite words. We investigate the following guiding questions: What is the minimal complexity of a non-trivial infinite word over a binary, ternary, or more generally finite alphabet? How should ''non-triviality'' be formalized? Which words achieve this minimal complexity? Are there many? Are they interesting? In exploring these questions, we introduce classical objects and tools from combinatorics on words -- such as Sturmian words and Rauzy graphs -- as well as little-known and new results. In particular, the third chapter is devoted to a theorem by R. Tijdeman from 1999, which generalizes a seminal result of M. Morse and G. Hedlund from 1938. We provide a new, algebraic proof of this theorem (due to J. Cassaigne and the author, 2022) and develop its consequences.

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.

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.