arXiv++ Combinatorics

Start with four digits, arrange them in both descending and ascending order, subtract, and repeat. This simple process is known as the Kaprekar routine, famous in base ten for sending every nonconstant four-digit string to $6174$. We show that in every odd base $B>3$, the four-digit Kaprekar map has an unexpectedly rigid structure. After at most three iterations, every nonconstant orbit enters an explicit triangular region $\mathcal{T}_B$, and on this region the map is conjugate to projective doubling: \[ \{[r],[s]\}\longmapsto \{[2r],[2s]\}. \] This gives a complete finite description of all nonconstant terminal cycles, including an explicit formula for their lengths and counts. In particular, the longest terminal cycle has length at most $(B-1)/2$, and equality can occur only when $B$ is prime. For primes $p>5$, equality occurs precisely when the least positive $m$ with $2^m\equiv\pm1\pmod p$ is $m=(p-1)/2$. The results proved here were first formulated by Schwartz and Thakur. As a test case for AI-assisted formal mathematics, AxiomProver produced Lean/mathlib formalizations of these results.

In his 2009 paper, Thakur posed three conjectural hypotheses for the degrees of the power sums \[ S_d(k)=\sum_{\substack{a\in \mathbb F_q[t] \text{ monic}\\ °a=d}} a^{-k} \qquad\text{and}\qquad s_d(k)=-°_t S_d(k). \] For prime fields $q=p$, we prove Hypotheses H1 and H2, giving a unique greedy description of the extremal term in Carlitz's formula and establishing the recursion \[ s_d(k)=s_{d-1}(s_1(k))+s_1(k). \] As consequences, the prime-field recursion gives the strict Newton-polygon convexity used in the prime-field Carlitz-Goss Riemann-hypothesis theorem, and it recovers Thakur's nonvanishing theorem for positive multizeta values over $\mathbb F_p[t]$. We also prove Hypothesis H3 for all finite fields $q=p^f$, establishing the monotonicity \[ s_d(k)<s_d(k+1)\qquad (p\nmid k). \] We provide Lean formalizations of the arguments in this paper, generated by AxiomProver.

The Riemann--Roch theorem for graphs, due to Baker and Norine, is a foundational result establishing a powerful analogy between finite graphs and algebraic curves. We describe a complete formal proof of this theorem implemented in the Lean 4 theorem prover. Our formalization includes the existence and uniqueness of q-reduced divisors, a modified form of Dhar's burning algorithm, the bijection between acyclic orientations with unique source and maximal superstable configurations, and Clifford's theorem. We also include several challenges for future formalization.

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.

We present a short proof that the book Ramsey number $R(B_8,B_{10})$ equals 37. The lower bound $R(B_8,B_{10}) \ge 37$ is already available in the literature, so it is enough to rule out a 37-vertex graph containing neither a copy of $B_8$ nor a copy of $B_{10}$ in its complement. The problem as well as the proof were found with AutoMath, an AI-assisted mathematical discovery workflow developed by the first author. A Lean formalization of the upper-bound argument is available in the accompanying repository.

Complementarity is the case in which a human--AI interaction (HAI) outperforms the best prediction benchmark available among its members. Although this idea is central in HAI research, formal work on complementarity remains limited. Existing frameworks do not model how agents' predictions compose into workflow-sensitive multi-agent protocols. We close this gap by introducing a tree-based formalization of complementarity in multi-agent HAI. An HAI protocol is represented by an ordered agent-role configuration together with a rooted planar binary tree whose leaves are decorated by prediction vectors. A local binary composition rule is evaluated recursively along the tree, yielding a tree-relative complementarity functional relative to a pointwise-min oracle benchmark. We prove four results. First, selector-based HAIs, including self- or AI-reliance, cannot achieve complementarity regardless of task, loss, or prediction quality. Second, in regression under squared loss, complementarity is equivalent to Euclidean distance minimization from the ground-truth vector; for $N=2$, the optimal linear-pooling weight has a closed form and a residual-correction interpretation. Third, under linear local composition, every protocol tree defines a barycentric coordinate chart on the simplex of leaf weights; Tamari-cover reparameterizations of protocol trees preserve complementarity, and for $N=4$, they satisfy the pentagon identity. Fourth, in binary classification, no internal local composition can achieve complementarity under endpoint-monotone losses, including standard Bregman and many finite Bernoulli $f$-divergence losses; an analogous obstruction holds for multiclass aggregation under cross-entropy. In summary, our framework shows that complementarity is attainable in multi-agent regression, but obstructed in classification under natural conditions on local aggregation and loss functions.

Graph coloring with preferences offers a powerful framework for constraint satisfaction problems in which fulfilling every request is impossible but satisfying a guaranteed positive fraction is highly desirable. A \emph{request} on a graph $G$ equipped with a list assignment $L$ assigns to each vertex of some subset $dom(r)\subseteq V(G)$ a preferred color from its list. Following Dvořák, Norin, and Postle (2019), $G$ is \emph{$\varepsilon$-flexibly $k$-choosable} if, for every $k$-list assignment $L$ and every request $r$, there is an $L$-coloring of $G$ that agrees with $r$ on at least $\varepsilon|dom(r)|$ vertices. The corresponding notion for DP-coloring (correspondence coloring) was formalized by Bradshaw, Choi, and Kostochka (2025). Choi, Clemen, Ferrara, Horn, Ma, and Masařík (2022) proved that every planar graph without $4$-cycles and with $3$-cycle distance at least $2$ is $\varepsilon$-flexibly $4$-choosable. We improve the result in two respects: weakening the hypothesis from $3$-cycle distance $\geq 2$ to vertex-disjoint triangles, and strengthening the conclusion from list flexibility to weighted DP-flexibility: \emph{Every simple planar graph without $4$-cycles and without intersecting triangles is weighted $\varepsilon$-flexibly DP-$4$-colorable.} The list size $4$ is sharp: Montassier, Raspaud, and Wang constructed a planar graph without $4$-cycles, $5$-cycles, and intersecting triangles that is not $3$-choosable.

Ballantine--Beck--Feigon--Maurischat introduced the subsum polynomial \[ \operatorname{sp}(λ,x):=\prod_i (1+x^{λ_i}) \] attached to an integer partition $λ$, and studied rational functions obtained by summing reciprocals of these olynomials over natural classes of partitions. They posed ten conjectures which naturally divide into coprimality and divisibility questions, special-value and recurrence formulas, and coefficient-shape problems. We prove all of the conjectures in the first two families: the ordinary and binary coprimality/divisibility conjectures, and the odd and ternary special-value/recurrence conjectures. AxiomProver autonomously produced Lean/mathlib formalizations and machine-checkable proofs of these six conjectures, and also discovered the counterexample showing that the binary log-concavity conjecture is false as stated.

Let $D_d(m) = \operatorname{Cay}((\mathbb{Z}/m\mathbb{Z})^d, \{e_0, \ldots, e_{d-1}\})$ be the directed Cartesian product of $d$ directed $m$-cycles. We prove that $D_d(m)$ admits a directed Hamilton decomposition for every dimension $d \geq 2$ and every odd modulus $m \geq 3$. The proof combines two new closure mechanisms with a small set of base dimensions. The high-modulus count branch handles every odd $d \geq 5$ and every odd $m \geq d$ via triangular prefix coordinates and a primitivity criterion controlled by gcd conditions on symbol counts. The base-tail modular-trade branch handles the complementary range $m < d$ by decomposing a base multigraph into cylinders and scheduling active tail residues by local symbol trades; it yields the successor closure $b \mapsto 2b+1$ for $b \geq 5$. Together with multiplicative product closure, these reduce the all-dimensions theorem to the four base dimensions $d \in \{2, 3, 5, 7\}$. Dimensions $2$ and $3$ are proved here; dimensions $5$ and $7$ are imported from companion arXiv preprints. A Lean 4 formalization records the same all-dimensions endpoint. As an independent consequence, the dimensions $2$ and $3$ alone solve every odd $d \geq 29$, by a dyadic-triadic interval-hitting argument.

Erdős Problem 30 asks for sharp asymptotics of the Sidon extremal function $h(N)$, and Singer's construction is the classical source of lower-bound examples matching the main term. We present a Lean 4 formalization of Singer's Sidon set construction for prime fields, together with reusable Sidon-set infrastructure for additive combinatorics. For every prime $p$, we prove the existence of a Sidon set modulo $p^2+p+1$ of cardinality $p+1$. The proof proceeds through a non-trivial algebraic chain: construction of the Galois field $\mathrm{GF}(p^3)$, analysis of the trace kernel as a 2-dimensional subspace, a geometric argument via subspace intersections establishing the multiplicative Sidon property in the quotient group, and a combinatorial bridge transferring this to modular integer arithmetic. Around this central result, we develop a reusable Sidon set library for additive combinatorics. It comprises interval Sidon sets, modular Sidon sets, the extremal function $h(N)$, Lindstrom's cross-difference inequality, a Johnson-route shift-incidence upper bound of the form $h(N) \leq \sqrt{N} + N^{1/4} + O(1)$, exact representation-function identities, and unconditional two-sided $h(N)=Θ(\sqrt{N})$ bounds with exact floor-rounded finite statements for $N \geq 5$. We further formalize a conditional reduction: subpolynomial prime gaps together with a full subpolynomial upper-error hypothesis for $h(N)$ imply the Erdős Problem 30 estimate $h(N)=\sqrt{N}+O_\varepsilon(N^\varepsilon)$ for every $\varepsilon>0$. The core Singer/Sidon and transfer development comprises 6,382 lines of Lean 4 with zero active uses of sorry. We describe the mathematical lessons learned, focusing on how formalization clarifies the precise scope of classical arguments and forces explicit treatment of the algebraic-combinatorial interface.

We prove that the directed seven-dimensional equal-side torus D_7(m) = Cay((Z/mZ)^7, {e_0, e_1, ..., e_6}) admits a directed Hamilton decomposition for every odd integer m >= 3. The proof has two main contributions. First, we introduce the root-flat certificate: a named verification framework in which a Hamilton decomposition of D_n(m) follows from three local conditions on a single root flat -- row Latinness, layer bijectivity, and primitive return maps. This abstraction was used informally in the earlier odd D_5(m) construction; here it appears as a definition and a theorem, providing a common verification interface for prime-dimensional base cases. Second, for every odd m >= 7, we give a uniform prefix-coordinate construction: one-layer prefix maps, a symbol-count criterion, and explicit 7x7 count matrices produce all seven Hamilton factors without a finite search. The remaining moduli m = 3 and m = 5 are exactly the boundary where the prefix-count method provably cannot work; they are handled by finite root-flat certificates whose validity is checked in Lean 4. A Lean 4 formalization verifies the Cayley statement, with the symbolic branch and the finite boundary certificates checked in the same development.

We prove that the directed five-dimensional torus $D_5(m) = \operatorname{Cay}((\mathbb{Z}_m)^5, \{e_0, e_1, e_2, e_3, e_4\})$ has a Hamilton decomposition for every odd integer $m \geq 3$. This is the first higher-dimensional case in which the return-map method requires a genuine zero-set selector rather than an odometer-type correction. The construction assigns the five outgoing generators by a cyclic layer schedule with one non-constant layer determined by a zero-set Latin table; an explicit finite exact-cover certificate proves that this layer is a matching. By cyclic symmetry, Hamiltonicity of all color classes reduces to a single normalized return map. For $m \geq 5$, an explicit first-return calculation on the section $p = 2$ gives one induced cycle whose excursion lengths sum to $m^4$. The remaining modulus $m = 3$ is settled by a printed finite cycle certificate. A companion Lean 4 formalization provides an independent machine verification of the Cayley statement and the finite certificates; source, audit scripts, and ancillary search code are available at https://github.com/aria1th/Torus-Hamilton-Decomposition-Program.

We study Chebyshev quotients that arise in the representation theory of Lie algebras, specifically within the theory of Demazure flags for fusion products of $\mathfrak{sl}_2[t]$-modules. Motivated by a recent formula that expresses certain Demazure multiplicities as coefficients of such quotients, we prove a general eventual non-negativity theorem: each quotient either terminates or has strictly positive coefficients for sufficiently large degrees, which we in turn interpret in terms of matchings and bounded walks. In several natural infinite families, these are unsigned bounded Dyck path models, giving both a structural explanation for the observed positivity phenomenon and concrete combinatorial models for key families of Demazure multiplicities. The theorems in this paper were autonomously produced and formalized in Lean/Mathlib by AxiomProver from natural-language statements.

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 generalize the well-studied notion of a modular pair of a finite matroid to arbitrary families of sets in infinite matroids, and use it to develop the theory of infinite matroids in several as-yet-unexplored areas. Our results include a complete theory of single-element extensions, a description of the relationship between quotients and projections, a proof that matroids for which every flat is modular must be finitary, and two new perspectives on the infinite matroid connectivity parameter λ. In most cases, existing theory for finite matroids either fails completely or does not extend in obvious ways, and as a result we develop multiple new techniques for reasoning about infinite matroids, including establishing well-behaved infinite analogues of nullity, local connectivity and skewness. We also point to an online repository containing formalized proofs of all our results using the lean4 proof assistant

Erdős asked whether every $n$-point set in Euclidean space whose $\binom{n}{2}$ pairwise distances are mutually at least $1$ apart must have diameter at least $(1+o(1))n^2$. We disprove this statement by constructing for every prime power $q$ a set $\mathcal X_q\subset \mathbb R^{q^2+q}$ of $n=q+1$ points such that all pairwise distances in $\mathcal X_q$ are mutually at least $1$ apart, while $$\operatorname{diam}(\mathcal X_q)\le\Bigl(1-\frac{1}{π^2}+o(1)\Bigr)n^2.$$ The proof is fully formalized in Lean 4.

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.