arXiv++ Combinatorics

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.

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.

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 introduce a quadratic form $Q$ on the space of functions on the gap poset $G$ of the numerical semigroup $\langle a,b\rangle$. We prove combinatorially that when evaluated on the indicator function of an upward closed subset $D$, this quadratic form precisely recovers the Gorsky--Mazin $\mathtt{dinv}$ statistic of $D$, viewed as a Young subdiagram of $G$. Furthermore, we prove Theorem~1.2 that when evaluated on a pair of subdiagrams of $G$, the symmetric bilinear form associated with $Q$ is equal to a novel cross-$\mathtt{dinv}$ statistic, which is nonnegative. Combining these, we prove the inequality \[ Q(\mathbf{n})\geq \dfrac{1}{|G|}\,\|\mathbf{n}\|_\infty^2\] if $\mathbf{n}$ is a real-valued decreasing function on $G$, showing an effective positive definiteness of $Q$ on the corresponding cone. Theorem~1.2, the main engine of the paper, was autoformalized in Lean/Mathlib by AxiomProver.

Let $f(m)$ be the largest integer such that for every set $A = \{a_1 < \cdots < a_m\}$ of $m$ positive integers and every open interval $I$ of length $2a_m$, there exist at least $f(m)$ disjoint pairs $(a, b)$ with $a \in A$ dividing $b \in I$. Solving a problem of Erdős, we determine $f(m)$ exactly, and show $$ f(m)=\min\bigl(m,\lceil 2\sqrt{m}\,\rceil\bigr) $$ for all $m$. The proof was obtained through an AI-assisted workflow: the proof strategy was first proposed by ChatGPT, and the detailed argument was subsequently made fully rigorous and formally verified in Lean by Aristotle. The exposition and final proofs presented here are entirely human-written. [This paper solves Problem #650 on Bloom's website "Erdős problems".]

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.

A rational triangle $T$ (one whose angles are rational multiples of $π$) unfolds to a translation surface $(X_T,ω_T)$. The lattice triangle problem asks to classify those $T$ for which $(X_T,ω_T)$ is a Veech (lattice) surface, which means that the $\operatorname{SL}_2(\mathbb R)$-orbit of $(X_T,ω_T)$ is closed in its stratum (so its projection to moduli space is a Teichmüller curve). The most mysterious regime is the "hard obtuse window" (largest angle in $(π/2,2π/3]$), where it is conjectured that no lattice triangles exist. Using an arithmetic reformulation of the Mirzakhani-Wright rank obstruction, we prove a quantitative theorem that rules out all but a density 0 subset of the triangles in this window. The main engine in this paper was autoformalized by AxiomProver in Lean (using mathlib).