arXiv++ Combinatorics

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 prove that every natural number is a finite sum of distinct unit fractions whose denominators are semiprimes (products of two distinct primes). This is the $ω=2$ integer case of a problem of Erdős and Graham, stated only as a conjecture by Butler, Erdős and Graham (Integers 15 (2015), A51), who proved the $ω=3$ analogue. Counterintuitively the problem hardens as $ω$ decreases -- the induction's feed thins -- so $ω=2$ is the hard case; our proof adapts the Butler-Erdős-Graham induction to this thin-feed regime, where the entire content of the induction step reduces to an explicit onset inequality $Y_0(N)\le\min\{β(N),β'(N)\}$, proved for all $N\ge10$ by Olson's addition theorem and elementary Chebyshev bounds above a finite, machine-checked base range. The same engine extends to the rationals: for every squarefree $b$, every $a/b$ above an explicit threshold $\min\{B_{N_b}/6,\,1/5\}$ is $ω=2$ representable, unconditionally. As an application we give the first complete proof of the rational $ω=3$ statement -- every $a/b$ with squarefree $b$ is a sum of distinct sphenic unit fractions -- that Butler, Erdős and Graham conjectured but left unpublished; a descent settles every $ω\ge3$. What remains open is the $ω=2$ regime below this threshold, which we reduce to a single explicit conjecture -- that the gap-free floor of a semiprime subset-sum set tends to zero. This work is a human-AI collaboration: AI tools (notably Anthropic's Claude, used through Claude Code) contributed substantially to the Lean formalisation, the experiments, and the writing; correspondingly, every result is machine-checked in Lean 4 / Mathlib (no sorry; two cited classical axioms, plus the native_decide compiler-trust base for the finite computations), so its correctness is independent of the tools used.

A function $f \colon X^k \to X$ on a finite set embeds into a polynomial of total degree $d$ over a commutative ring $R$ if there is an injection $j \colon X \to R$ and a polynomial $g$ of total degree at most $d$ with $j \circ f = g \circ j^k$, where $j^k$ applies $j$ in each coordinate. These are the transition functions of $k$-neighbour cellular automata, and the injection $j$ is an enlargement of the alphabet that preserves the transitions. We prove three results, all verified in Lean~4 with Mathlib~\cite{bacik2026finbin}. Every unary function $f \colon X \to X$ embeds into a polynomial of total degree $1$. Every binary Kronecker delta embeds into a polynomial of total degree $4$. For every $d$ there is a binary function that does not embed into any polynomial of total degree $d$.

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.

Let $K_\mathrm{KR}$ denote the optimal Kalton--Roberts constant for approximately additive real-valued set functions on algebras of sets. Kalton and Roberts proved $K_\mathrm{KR}\le89/2$, and Bondarenko, Prymak, and Radchenko improved the upper bound to $38.8$. We prove that $$K_\mathrm{KR}\le\frac{694,198,146,664,396,294,486,127,753}{34,994,834,677,886,019,996,000,000}\,\approx 19.837.$$ Thus the original Kalton--Roberts upper bound is more than halved. The proof changes the source collections fed into the expander-recombination step however still uses expander graphs as the other proofs do. The four expander families used in the final recombination are certified by exact rational interval arithmetic, and the proof has been formalised in Lean.

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.

The 2026 disproof of Erdős's unit-distance conjecture and Sawin's subsequent explicit quantitative refinement show that the maximum number $u(n)$ of unit distances among $n$ planar points can exceed $n^{1+\varepsilon}$ for a fixed positive $\varepsilon$. Sawin's explicit bound gives more than $n^{1.014}$ unit distances for arbitrarily large $n$ and exposes integer parameters whose choice is not fully optimized. This report starts from Sawin's nonlinear integer optimization problem and develops an open-source Python verification pipeline. The pipeline is first validated by reproducing Sawin's published parameter choice and is then applied to computationally improved certificates. We optimize and verify certificates involving sets of primes $T$ and $S_Q$, integer multiplicities $k(p)$, and a rationally encoded real parameter $R$. The implementation is deliberately lean, so that all results can be replicated on standard hardware and the procedures can be extended. We compare a deterministic greedy heuristic, a tailored integer evolution strategy with two-sided geometric, or discrete-Laplace, integer mutation and repair operators for number-theoretic feasibility, and a two-parent discrete-recombination variant. Four certificate levels are reported: Sawin's published example with $δ=0.0141144286784982\ldots$, a greedy certificate with $δ=0.0151718056372133\ldots$, a tailored integer evolution strategy certificate with $R=6672416/100000$ and $δ=0.0152616610684193\ldots$, and a recombination variant with the same $R$ and $δ=0.0152628688170072\ldots$. Consequently, the best current certificate supports the cautious statement $u(n)>n^{1.0152}$ for arbitrarily large $n$. Beyond this unit-distance application, the work illustrates how randomized optimization heuristics can improve explicit certificates in pure mathematics and combinatorial geometry.

The Membership Problem for Pedigree Polytope (M3P) asks, given $X\in\mathbb{Q}^{\binom{n}{3}}$, whether $X\in\mathrm{conv}(P_n)$, where $P_n$ is the set of all pedigrees. A pedigree is a structured encoding of a Hamiltonian cycle construction in $K_n$. We establish that M3P is solvable in strongly polynomial time via a recursively constructed layered network $(N_k, R_k, μ)$ and a multicommodity flow problem MCF$(k)$. The necessary and sufficient condition for membership established is that the optimal total flow in MCF$(n-1)$ equals the maximum possible flow $z_{\max}$. The complexity analysis, grounded in Tardos's strongly polynomial algorithm for combinatorial linear programs (1986), shows that this condition can be checked in strongly polynomial time in the dimension of the matrix involved. By sufficiency, this implies M3P~$\in$~P. Since the Symmetric Travelling Salesman Problem (STSP) reduces to M3P via the Multistage Insertion (MI) formulation (Arthanari 1983), STSP is solvable in polynomial time, and the P vs.NP question is resolved. The proofs leading to this result are fully machine-verified in Lean~4/Mathlib4, with zero unresolved \texttt{sorry}s in the main proof chain. The main contribution is the Lean~4 machine verification of all proofs in the main chain, resulting in \texttt{theorem p\_equals\_np}: P = NP. The Lean~4 formal verification covers the sufficiency of MCF(n-1) for membership in $\mathrm{conv}(P_n)$, and the P = NP chain via Maurras (2002), Grötschel--Lovász--Schrijver (1988), Cook (1971), and Karp (1972). The complete lean project (36 Lean~4 files, 2968/2968 build targets clean) is available at https://github.com/TiruArt/Pedigree-Polytopes-Lean4.

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.

For a positive integer $n$, let $g(n)$ denote the infimum of all real numbers $L$ such that there exists a multiplicative Sidon set $A\subseteq\{1,2,\dots,n\}$ that intersects every interval $[x,x+L]\subseteq[1,n]$. Sárközy asked for estimates on $g(n)$, and he in particular asked whether one has $g(n)\le\sqrt n$ for every $n\in\mathbb{N}$. We first show that this estimate does indeed hold, with a proof that was autonomously discovered and formally verified in Lean by Aristotle. Next, we improve the upper bound further and, with $ρ= \frac{13-\sqrt{69}}{10} < 0.47$, prove that $g(n)\ll_{\varepsilon} n^{ρ+\varepsilon}$ for every $\varepsilon > 0$.

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.

Ramsey-good graphs are graphs that contain neither a clique of size $s$ nor an independent set of size $t$. We study doubly saturated Ramsey-good graphs, defined as Ramsey-good graphs in which the addition or removal of any edge necessarily creates an $s$-clique or a $t$-independent set. We present a method combining SAT solving with bespoke LLM-generated code to discover infinite families of such graphs, answering a question of Grinstead and Roberts from 1982. In addition, we use LLMs to generate and formalize correctness proofs in Lean. This case study highlights the potential of integrating automated reasoning, large language models, and formal verification to accelerate mathematical discovery. We argue that such tool-driven workflows will play an increasingly central role in experimental mathematics.

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

For a family $(A_q)_{q\in Q}$ of subsets of a semigroup, the product intersection set records those exponents $h \in \mathbb{N}$ for which the $h$-fold product set of the intersection, $(\bigcap_q A_q)^h$, is equal to $\bigcap_q A_q^h$, the intersection of the product sets. Nathanson recently asked which subsets of $\mathbb{N}$ can occur as a product intersection set, both for arbitrary and for decreasing families $(A_q)_{q\in Q}$. We solve both problems by giving a complete classification. In particular, when $|Q| \ge 2$, we show that in either case any subset $X \subseteq \mathbb{N}$ with $1 \in X$ occurs as a product intersection set. Both classifications were autonomously discovered and formally verified in Lean by Aristotle, a formal reasoning agent developed by Harmonic.