arXiv++ Combinatorics

For integer vectors R,S let A(R,S) denote the class of (0,1)-matrices with row sum vector R and column sum vector S. Its interchange graph G(R,S) has A(R,S) as its vertex set, two matrices being adjacent when they differ by a single 2 x 2 interchange. Brualdi conjectured that G(R,S) is Hamiltonian for every R,S. We prove the stronger statement that G(R,S) is maximally Hamiltonian: Hamilton-laceable when bipartite, and Hamilton-connected when not. The proof is a structural induction on the number of matrices in the class, organized by the structure theory of interchange graphs. Deleting inactive lines and splitting invariant positions expresses any class as a Cartesian product, reducing the argument to the prime factors. The bipartite classes are products of complete transposition graphs; we settle them together, without induction, by proving they are paired 2-disjoint-path-coverable and hence Hamilton-laceable, using a recent theorem of Coleman, Fischberg, Gong, Harrington and Wong on paired disjoint path covers. The non-bipartite classes divide into three cases: products assembled from smaller factors, a base of Johnson graphs and small classes, and the large prime classes, treated by a pivot-and-fiber construction whose line quotients are matroid base-exchange graphs. The complete argument has been machine-checked in the Lean 4 proof assistant from first principles together with seven cited results of the literature; the disjoint-path-cover results it imports are themselves proved within the formalization.

Let $p$ be a prime number. We introduce a sparseness condition on the supports of $p$-adic Hahn series, and prove that this condition implies transcendence over $\breve{\mathbf Q}_p$, the completed maximal unramified extension of $\mathbf{Q}_p$. As an application, we prove the order-type conjecture of $\mathbf{Q}_p$-algebraic $p$-adic Hahn series with bounded support under the condition that the support has only finitely many accumulation points. All results in this paper have been fully formalized in the Lean theorem prover (v 4.31.0), building over Mathlib.

For $n\ge1$, we let $$x_n:=\tan\bigl(\sum_{k=1}^{n}\arctan k\bigr).$$ In 2008, Amdeberhan, Medina, and Moll conjectured that $x_n\not \in \mathbb{Z}$ for every $n\ge5$. This was known for a set of positive integers of density $\tfrac{120}{817}\approx0.1469$. We prove that an integer value $x_n=m$ satisfies $|m|\ge e^{(1/2+o(1))\,n\log n}$, which we use to deduce that $$\#\{\,1\leq n\le N:x_n\in\mathbb{Z}\,\}=O(\log N). $$ In particular, the conjecture holds for a density-one set of $n$. The results in this note were formalized in Lean/Mathlib and produced autonomously by AxiomProver from natural-language statements.

The theory of $q$-series and basic hypergeometric series plays a crucial role at the intersection of combinatorics, number theory, and representation theory. From the classical partition identities of Euler and Jacobi to modern developments in class field theory, vertex operator algebras, and the Monstrous Moonshine conjecture, $q$-series provide the analytic framework for a wide range of profound applications. In this paper, we discuss the formalization of this theory in the Lean proof assistant, a process that requires careful design of scalable and versatile structures to reconcile formal algebraic identities with analytic convergence properties. We address these foundational challenges by focusing on the construction of $q$-Pochhammer symbols, $q$-binomial coefficients, Bailey's Lemma and similar primitives. To demonstrate the utility of this work, we provide fully verified proofs of the Jacobi Triple Product formula and the celebrated Rogers-Ramanujan identities, which serve as both historical and technical benchmarks for the field. This work establishes a rigorous computational foundation for the future formalization of mock theta functions, modular forms, and the diverse algebraic structures that underpin their applications across mathematics and physics.

Let $f_3(N)$ be the least integer such that every set $A\subseteq\{1,\ldots,N\}$ of size at least $f_3(N)$ contains distinct elements $a,b,c\in A$ such that $a+b\in A$, $a+c\in A$, and $b+c\in A$. We prove that $f_3(N)\le 5N/8+O(1)$. Together with the standard construction $[N/8,N/4]\cup[N/2,N]$, this gives $f_3(N)=5N/8+O(1)$, resolving Erdős Problem 865. The proof is self-contained. An earlier conditional version of the reduction has also been formalized in Lean 4/Mathlib with no sorries and no added axioms.

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.

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.