Motivation

Error-correcting codes protect information against corruption by adding controlled redundancy. For a code, the distribution of Hamming weights records how its words are spread across possible distances from the zero word and determines basic quantities such as its minimum distance. Linear codes also carry an algebraic duality: every linear code $C$ over a finite field has a dual code $C^\perp$ consisting of the words orthogonal to all words of $C$ under the standard coordinatewise bilinear form.

The MacWilliams identity states that the full Hamming-weight distribution of $C^\perp$ is determined by that of $C$ through one linear change of variables. It is the principal result of Chapter 5 of F. J. MacWilliams and N. J. A. Sloane's The Theory of Error-Correcting Codes. The binary identity appears there as Theorem 1, while the arbitrary-finite-field Hamming-weight-enumerator identity formalized here is Theorem 13 on p. 146. The surrounding chapter develops related transformations for complete, Lee, exact, joint, and split weight enumerators, nonlinear-code distance distributions, orthogonal arrays, and Krawtchouk polynomials.

This development isolates the arbitrary-$q$ Hamming identity as a first reusable result. Its declarations are designed to support later formalizations drawn from the same chapter and, more broadly, from the book, without enlarging the present target beyond the MacWilliams identity.

Setting

Let $F$ be a finite field of cardinality $q$, let $\iota$ be a finite coordinate type, and let a word be a function $c:\iota\to F$. A linear code $C$ is an $F$-linear subspace of the word space. The standard bilinear form is

$$\langle c,v\rangle=\sum_{i\in\iota}c_i v_i,$$

and the dual code is

$$C^\perp=\{v:\iota\to F:\langle c,v\rangle=0\text{ for every }c\in C\}.$$

The Hamming weight $\operatorname{wt}(c)$ is the number of coordinates at which $c$ is nonzero. Writing $n=|\iota|$, the homogeneous Hamming weight enumerator of $C$ is the integer-coefficient polynomial

$$W_C(X,Y)=\sum_{c\in C}X^{n-\operatorname{wt}(c)}Y^{\operatorname{wt}(c)}.$$

Thus the coefficient of $X^{n-j}Y^j$ is the number of codewords of weight $j$. The Lean development represents this object symbolically in MvPolynomial (Fin 2) ℤ; its complex-valued form is obtained by evaluation, so the symbolic and evaluated presentations share a single definition.

Formalization targets

Character orthogonality over a code

For a primitive complex additive character $\psi$ of $F$, define

$$S_C(v)=\sum_{c\in C}\psi(\langle c,v\rangle).$$

The first milestone states that $S_C(v)=|C|$ when $v\in C^\perp$ and $S_C(v)=0$ otherwise. The binary statement occurs as Problem 13 on p. 134 of MacWilliams--Sloane; Lemmas 9 and 11 on pp. 143--145 give the finite-field character and Fourier formulation.

Coordinatewise Hamming transform

For every word $c$ and all $X,Y\in\mathbb C$, the second milestone records the full character-weighted transform of the Hamming monomial:

$$\sum_{v\in F^\iota} X^{n-\operatorname{wt}(v)}Y^{\operatorname{wt}(v)} \psi(\langle c,v\rangle) = \bigl(X+(q-1)Y\bigr)^{n-\operatorname{wt}(c)} (X-Y)^{\operatorname{wt}(c)}.$$

This is a separately reusable formulation of the coordinate calculation appearing in the proofs of Theorems 10 and 13 on pp. 144--146.

MacWilliams identity

The capstone is the following equality of integer polynomials:

$$|C|\,W_{C^\perp}(X,Y) = W_C\bigl(X+(q-1)Y,\,X-Y\bigr).$$

This is the denominator-free form of Chapter 5, Theorem 13. After evaluation over a characteristic-zero field it is equivalent to the normalized textbook formula

$$W_{C^\perp}(X,Y) = \frac{1}{|C|}W_C\bigl(X+(q-1)Y,\,X-Y\bigr).$$

Significance

The identity turns duality into an enumerative operation: knowing the weight enumerator of a linear code determines the weight enumerator of its dual. It supplies immediate consistency restrictions on possible weight distributions and is a basic input to the study of self-dual codes, Krawtchouk transforms, association schemes, invariant-theoretic properties of enumerators, and linear-programming bounds.

The formalization contributes a small common interface for finite-field words, linear codes, standard duals, and homogeneous Hamming weight enumerators. These declarations are absent from the selected Mathlib environment even though Mathlib already provides Hamming weight, finite-field algebra, additive characters, finite sums, bilinear-form orthogonals, and multivariate polynomials. Establishing the interface and its first central theorem makes those general libraries directly usable for subsequent coding-theory developments.

Difficulty

The paper statement is short, but its formal representations live in several different layers. Codes are submodules whose elements are subtypes; Hamming weight is a natural-number count; duality is expressed through a bilinear form; character identities take values in $\mathbb C$; and the final result is most reusable as an equality of symbolic polynomials over $\mathbb Z$. The central formalization burden is maintaining exact agreement while transporting the same enumerative data among these layers, including finite instances for codeword subtypes and the natural-number exponents of the homogeneous monomials.

The theorem must also retain the genuine finite-field statement. Replacing the code by an arbitrary finite set, hard-coding the binary field, defining the dual by its expected cardinality, or proving only equality at one chosen pair of evaluation points would not establish the target.

Formalization scope

The coordinate type is an arbitrary finite type rather than only Fin n; its cardinality plays the role of the code length. A word is CodingTheory.Word F ι := ι → F, and a linear code is a submodule of this common word space. This representation provides the linear structure and canonical orthogonal dual required here while leaving room for a future nonlinear-code type built from finite sets of the same words.

The polynomial CodingTheory.hammingWeightEnumeratorPolynomial has coefficients in $\mathbb Z$ and variables indexed by Fin 2. Variable $0$ records zero coordinates and variable $1$ records nonzero coordinates. Its name explicitly identifies the Hamming enumerator, leaving separate stable names available for future complete, Lee, exact, joint, and split weight enumerators. Those later enumerators should be added as new declarations and connected to this one by specialization theorems rather than replacing it.

The standard dual is bilinear, not Hermitian. The code alphabet may be any finite field. The zero code, full code, and empty coordinate type are included; in the empty-coordinate case there is one word of weight zero and the identity reduces to $1=1$. The present mission does not formalize nonlinear codes, complete or other generalized enumerators, orthogonal arrays, or Krawtchouk-polynomial theory. It establishes only the definitions and two character-sum milestones required for the Hamming MacWilliams identity, with a namespace and module boundary intended for reuse by later missions in the textbook series.

Selected references

• F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland, 1977, Chapter 5, pp. 125--154; especially Problem 13 (p. 134), Lemmas 9 and 11 (pp. 143--145), and Theorem 13 (p. 146). Publisher chapter record.
• Violetta Weger, Coding Theory, Technical University of Munich lecture notes, 2025, Theorem 11.2 and Lemma 11.8, pp. 154--159.
• F. J. MacWilliams, “A Theorem on the Distribution of Weights in a Systematic Code”, Bell System Technical Journal 42 (1963), 79--94.

Motivation

Counting the trees on a fixed, labeled vertex set is one of the oldest enumeration problems in graph theory. Cayley stated the count in 1889 while enumerating isomers of saturated hydrocarbons — each tree corresponds to a possible carbon skeleton — and the same number reappears throughout combinatorics as the number of spanning trees of the complete graph $K_n$, a special case of Kirchhoff's Matrix–Tree Theorem, and as the base case against which more refined tree-counting results (trees with a prescribed degree sequence, forests, spanning trees of general graphs) are measured.

Several independent proofs of the count are known — a direct recursive argument, a determinant computation via the Matrix–Tree Theorem, a double-counting argument on increasing trees — and each exposes a different piece of structure. This mission formalizes the proof via Prüfer sequences, due to Prüfer (1918): an explicit, computable bijection between labeled trees and certain finite sequences, presented here following Gross and Yellen, Graph Theory and Its Applications, 3rd ed. (CRC Press, 2018), Section 3.7, pp. 157–162.

Setting

Fix $n \geq 2$ and take the vertex set to be $\{1, \dots, n\}$ (formalized as Fin n). A labeled tree on $n$ vertices is a simple graph $T$ on this vertex set that is connected and acyclic (Mathlib's SimpleGraph.IsTree). Two labeled trees are the same exactly when their edge sets coincide — the two 4-vertex trees in Figure 3.7.1 of the source are both paths but are different labeled trees, since the labels sit on different vertices.

A Prüfer sequence of length $n - 2$ is any sequence $(s_1, \dots, s_{n-2})$ of labels drawn from $\{1, \dots, n\}$, repetitions allowed (so there are $n^{n-2}$ of them, by the rule of product).

The encoding of a tree $T$ (Algorithm 3.7.1, p. 157) builds its Prüfer sequence by repeating, $n-2$ times: find the leaf (degree-one vertex) with the smallest label among those not yet removed, record the label of its neighbor, then delete that leaf. The decoding of a sequence (Algorithm 3.7.3, p. 159) reverses this: it rebuilds the tree edge by edge, at each step joining the smallest label not yet used and not appearing later in the sequence to the next label in the sequence, finishing by joining the two labels left over.

Formalization targets

Goal — Cayley's Tree Formula (Theorem 3.7.5, p. 162)

$$\operatorname{Nat.card}\, \{T : \text{SimpleGraph}(\text{Fin } n) \mid T.\text{IsTree}\} = n^{\,n-2}, \qquad n \geq 2.$$

This is the weakest stable statement: it is exactly the count Cayley identified, phrased without reference to any particular proof method, so it is not tied to properties of Prüfer sequences beyond what is needed to establish the count.

Significance

The identity itself is foundational: it is the base case of Kirchhoff's Matrix–Tree Theorem (which computes the analogous count for spanning trees of an arbitrary graph as a cofactor of its Laplacian) and it appears as an ingredient in random graph theory (counting spanning trees of $K_n$ bounds the number of ways a random graph process can build a tree) and in the analysis of algorithms on trees, where the Prüfer encoding itself is used as a compact serialization of a labeled tree.

The result has been proved by hand for over a century, and its most classical proof (the one formalized here) has not, to this project's knowledge, appeared as a machine-checked Lean proof; Mathlib's Combinatorics.SimpleGraph library has the tree and acyclicity infrastructure this mission builds on, but not the Prüfer bijection or the count itself. Formalizing it here means constructing the encoding and decoding maps explicitly as computable, total recursive functions, and proving they are mutually inverse — the mission's four milestones below are exactly the four supporting results the source uses for this.

Difficulty

The obvious first attempt is to define the encoding by structural recursion, peeling one leaf per step, but this immediately runs into a dependent-typing obstacle: after deleting a vertex, the "remaining graph" naturally lives on a smaller vertex type, so a naive recursive definition changes type at every step and the final sequence's type (length $n-2$) is not visible to the recursion by construction. The formalization here sidesteps this by keeping the ambient vertex type fixed at Fin n throughout and tracking the shrinking set of "active" vertices as an ordinary Finset (Fin n) parameter, so the recursion is on a natural number step-counter rather than on the type itself; the price is that every step's "leaf" and "neighbor" must be picked out by an explicit Finset.filter/Finset.min computation whose well-definedness (there is always a smallest active leaf, and it always has a unique active neighbor) is exactly the content of Propositions 3.7.1 and 3.7.3 below, rather than something the type system gives for free. The inverse direction has the dual issue in reverse: decoding recurses structurally on the sequence while tracking a shrinking label set, and showing the two recursions undo each other (Proposition 3.7.4) requires the same induction run in both directions simultaneously.

Formalization scope

Trees are SimpleGraph (Fin n) satisfying Mathlib's SimpleGraph.IsTree; no alternate, weaker notion of "tree" is used. Prüfer sequences are functions Fin (n - 2) → Fin n (equivalently, by Fintype.card_fun, exactly the $n^{n-2}$ count needed) rather than List or Vector, so that the final counting step is immediate once the bijection is established. The encoding and decoding functions (pruferEncode, pruferDecode) are supplied as noncomputable definitions in Definitions.Def_GYGraphTheory — noncomputable only because Prop-level decidability of a general SimpleGraph.Adj is classical, not because the algorithm is non-constructive; every step is the literal Prüfer procedure, junk-valued (defaulting to label 0) outside its intended domain in exactly the way a hand proof would say "this step is meaningless once fewer than two active vertices remain." The four milestones give the precise faithful statements of the source's Propositions 3.7.1, Corollary 3.7.2, Proposition 3.7.3, and Proposition 3.7.4; the goal theorem is the immediate corollary once all four are in hand, via Fintype.card_congr and Fintype.card_fun. A trivializing formalization is not available here: IsTree is Mathlib's standard, non-vacuous notion, and the milestones pin down pruferEncode and pruferDecode to the source's specific algorithm rather than leaving the bijection's existence as a free black box. Beyond the four milestones, a full development needs: basic Finset/List manipulation lemmas relating pruferPeel's step-indexed recursion to pruferDecodeAux's list-indexed recursion (reusable in any future mission touching Prüfer-style encodings); and the final cardinality argument tying the bijection to n ^ (n - 2). Contributions connecting this formula to Mathlib's general Matrix–Tree machinery (if and when it exists) would be a natural, welcome extension but are out of scope for this mission.

Selected references

• A. Cayley, A theorem on trees, Quart. J. Math. 23 (1889), 376–378.
• H. Prüfer, Neuer Beweis eines Satzes über Permutationen, Archiv der Mathematischen Physik 27 (1918), 742–744.
• J.L. Gross and J. Yellen, Graph Theory and Its Applications, 3rd ed., CRC Press, 2018, Section 3.7 "Counting Labeled Trees: Prüfer Encoding", pp. 157–162.

Assigning distinct resources under compatibility constraints

A finite allocation problem begins with a list of permitted choices. Each recipient may use some resources but not others, and a resource may be assigned at most once. Knowing that every recipient has an available resource is insufficient: several recipients may all depend on the same small pool. A useful theorem must decide whether the compatibility pattern permits all requirements to be met simultaneously.

This mission develops the matching results in the chapter on systems of distinct representatives in D. Yogeshwaran's Discrete Mathematics—Lecture Notes, §6.1. Its endpoint allows different recipients to require different numbers of resources. The classical one-resource problem, the regular-graph case, and the case in which a bounded number of assignments may remain unfilled are retained as separate source-numbered results. The project concerns established theorems, not a new conjecture about the existence of matchings.

Graphs, matchings, and demands

A finite simple graph consists of a finite set of vertices and unordered pairs of distinct vertices called edges. A bipartition is a pair of disjoint sets $L,R$ whose union is the vertex set, such that every edge joins a vertex in $L$ to a vertex in $R$. The left vertices represent recipients and the right vertices represent resources. An edge records that the resource is permitted for that recipient. These graph conventions follow Definition 1.1 of the notes.

For a vertex $x$, the neighbor set $N_G(x)$ contains the vertices joined to $x$. For a set $S$ of vertices, write $N_G(S)=\bigcup_{x\in S}N_G(x)$. A matching is an edge set in which no vertex is used twice. It is complete on $L$ if every left vertex is used, and perfect if every vertex is used. A subgraph may retain selected edges of the original graph. Its degree $\deg_H(x)$ counts the retained neighbors of $x$.

A demand is a natural number $d_x$ attached to each $x\in L$. Unlike a complete ordinary matching, the capstone may assign more than one resource to a recipient. Resources still have capacity one, and a demand may be zero.

Formalization targets

The ordinary matching criterion is Theorem 6.2:

$$\exists\text{ a complete matching on }L \quad\Longleftrightarrow\quad \forall S\subseteq L,\quad |S|\le |N_G(S)|.$$

The development also includes Exercise 6.3, asserting that a $k$-regular bipartite graph has a perfect matching when $k>0$. Proposition 6.4 states the quantitative deficit version:

$$\bigl(\forall S\subseteq L,\ |S|-d\le |N_G(S)|\bigr) \quad\Longrightarrow\quad \exists M\text{ matching},\quad |L|-d\le |E(M)|, \qquad d\ge1.$$

The capstone is the prescribed-degree equivalence of Exercise 6.5:

$$\begin{split} &\exists H\subseteq G: \bigl(\forall x\in L,\ \deg_H(x)=d_x\bigr) \land \bigl(\forall y\in R,\ \deg_H(y)\le1\bigr)\\ &\qquad\Longleftrightarrow\quad \forall S\subseteq L,\quad \sum_{x\in S}d_x\le |N_G(S)|. \end{split}$$

This statement retains the entire demand function and does not fix a uniform demand, restrict demands to positive values, or replace integral selections by real weights.

The set-theoretic interface is Corollary 6.9. A finite family of arbitrary sets $(A_i)_{i\in I}$ has a system of distinct representatives, meaning an injective choice $f(i)\in A_i$, exactly when

$$\forall J\subseteq I,\qquad |J|\le \left|\bigcup_{i\in J}A_i\right|.$$

Only the index family is finite; the sets themselves may be infinite.

What the development provides

The demand criterion characterizes feasibility entirely in terms of the original compatibility graph and the requested multiplicities. Its necessity identifies an obstruction to any assignment, while its sufficiency asserts that no other obstruction exists. The deficit theorem gives a quantitative statement when complete coverage is unavailable. The regular case gives a distinct consequence for graphs described through their degrees, rather than through a separately supplied collection of neighborhood inequalities. These are the respective contents of Exercises 6.3 and 6.5 and Proposition 6.4.

Mathlib already provides finite-family and graph versions of Hall's theorem in its Hall development and graph interface. The source-aligned development therefore reuses established infrastructure. Its additional work consists of connecting exact graph degrees and edge counts to the source statements, retaining the deficit and zero-demand cases, and supplying an arbitrary-set representatives interface. Local proofs of the five theorem statements have been checked in Lean 4.29.0-rc3 with Mathlib 777aaa6.

Where exact formalization is delicate

Independent local choices do not guarantee a matching: different choices can collide at one resource. Replacing distinct selections by nonnegative real allocations would change the conclusion. Counting total demand alone also misses obstructions carried by proper subsets of recipients.

Several representation issues matter even after the mathematics is known. A left-saturating matching need not be perfect. A subgraph's vertex set may omit isolated ambient vertices. Cardinality conventions for infinite sets can turn a superficially plausible formula into a different assertion. Finally, a theorem that assumes all neighborhood inequalities has not established those inequalities merely because a graph is regular. The individual interfaces must distinguish these obligations rather than hide them inside a definition.

Formalization scope

The graph results use finite vertex types and native SimpleGraph and Subgraph objects. Both disjointness and coverage of the bipartition are explicit. Local-finiteness instances supply finite neighbor enumerations; they impose no further restriction on finite graphs. The complete-matching predicate combines the native matching condition with inclusion of the prescribed vertex set.

Degrees in the capstone are cardinalities of finite subgraph neighbor sets. The deficit conclusion counts unordered subgraph edges. Natural subtraction is truncated at zero, an equivalent convention for these nonnegative cardinality lower bounds. Empty graphs, empty index families, and zero demands remain admissible. In the representatives theorem, arbitrary sets are measured by extended cardinality; infinity is never replaced by zero.

The reusable outputs are the source-aligned graph statements, the complete-matching interface, the prescribed-degree equivalence, and the arbitrary-set representatives criterion. Equivalent proofs and clearer reusable interfaces are within scope. Placeholder conclusions, extra assumptions that exclude the difficult cases, and fractional substitutes for the integral capstone are not.

Selected references

• D. Yogeshwaran, Discrete Mathematics—Lecture Notes, Indian Statistical Institute Bangalore, HTML edition generated 2025. Chapter 6.1; graph conventions.
• The mathlib community, Mathlib 4, revision 777aaa6, 2026. Finite-family Hall theorem; native graph Hall theorem.

Motivation

Ramsey theory asks for the smallest number $R(k)$ such that every graph on $R(k)$ vertices contains either a clique of size $k$ or an independent set of size $k$. Beyond being one of the oldest problems in extremal combinatorics, Ramsey numbers sit at the junction of combinatorics, probability, and computer science: the two-coloring of edges they quantify is exactly the distinction between a graph and its complement, and their growth controls constructions used in derandomization and in the theory of Boolean functions.

This mission formalizes the paper that started the probabilistic method as a systematic tool: Erdős's 1947 proof that $R(k) > 2^{k/2}$. It is also the natural companion to the platform's Sipser–Gács–Lautemann mission: the union-bound argument formalized here is the same counting technique that drives the Lautemann lemma used to place $\mathsf{BPP}$ in $\Sigma_2^p$.

Timeline. Ramsey proved in 1928 that $R(k)$ is finite; Erdős and Szekeres gave the first upper bounds in 1935; Erdős's 1947 paper supplied the exponential lower bound $R(k) > 2^{k/2}$ by a one-page counting argument, introducing the probabilistic method. Better constants for specific regimes followed (Lovász local lemma 1975, Spencer 1977), but no general lower bound beyond $2^{(1+o(1))k/2}$ is known today.

Setting

Fix an integer $k \ge 3$ and put $N = 2^{\lfloor k/2 \rfloor}$. A graph is a pair $(V,E)$ with $E$ an irreflexive symmetric relation on $V$; here vertices are labeled $0, \dots, N-1$. A subset $s \subseteq V$ of size $k$ is a clique if every two distinct vertices of $s$ are adjacent, and an independent set if every two distinct vertices of $s$ are non-adjacent. A $k$-set that is either a clique or an independent set is monochromatic: it is monochromatic in the two-coloring of the complete graph on $V$ in which an edge is colored by the graph (present) or its complement (absent).

The ambient probability space is the uniform distribution over all graphs on $N$ labeled vertices — equivalently, each of the $\binom{N}{2}$ possible edges is present independently with probability $1/2$. This space has exactly $2^{\binom{N}{2}}$ elements.

A graph with no monochromatic $k$-set is a graph with neither a $k$-clique nor an independent $k$-set. The mission's goal, "the Ramsey number satisfies $R(k) > 2^{k/2}$", is formalized as the bare existence of such a graph on $N = 2^{\lfloor k/2 \rfloor}$ vertices, without defining the Ramsey number itself.

Formalization targets

Goal: the probabilistic lower bound

$$R(k) > 2^{k/2}, \qquad k \ge 3$$

i.e. there exists a graph on $N = 2^{\lfloor k/2 \rfloor}$ labeled vertices that contains no monochromatic $k$-set.

Stronger: the three steps of the proof, as separate targets

1. Count estimate. For $k \ge 3$ and $N = 2^{\lfloor k/2 \rfloor}$,

$$\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1, \qquad \text{equivalently} \quad \binom{N}{k} \cdot 2 < 2^{\binom{k}{2}}.$$

2. Union-bound principle. In any finite outcome space, if the total number of outcomes ruled out by all bad events together is less than the number of outcomes, some outcome avoids every bad event:

$$\sum_i \left| \{\omega : \mathrm{bad}\ i\ \omega\} \right| < |\Omega| \implies \exists\, \omega, \ \forall i,\ \neg \mathrm{bad}\ i\ \omega.$$

3. Pair-count bound. Over all graphs on $N$ vertices, the total number of pairs $(G, s)$ with $s$ a monochromatic $k$-set in $G$ is at most

$$\binom{N}{k} \cdot 2^{1+\binom{N}{2}-\binom{k}{2}}.$$

The goal follows by combining the three steps: the pair count is the sum over bad events in the union-bound principle, and the count estimate makes that sum smaller than the $2^{\binom{N}{2}}$ graphs.

Significance

The result. The lower bound $R(k) > 2^{k/2}$ is exponential, matching (up to the constant in the exponent) the best known upper bound $R(k) < 4^k$ from Erdős–Szekeres. It shows that the Ramsey function, despite being finite, grows genuinely fast — and the proof's method became more influential than the bound: the probabilistic method now permeates combinatorics, graph theory, and theoretical computer science (random graphs, discrepancy, property testing, derandomization).

Formalizing it. Mathlib currently contains no Ramsey theory at all: no definition of a Ramsey number and no lower bound. This mission closes that gap with the foundational result, in a way that is deliberately elementary — no measure theory, no randomness: the "probabilistic" argument is re-expressed as exact counting, which is why the statements are fully formalizable in Mathlib today. The union-bound principle (target 2) is a reusable lemma for future probabilistic-method formalizations, and the monochromatic-set infrastructure (targets 1 and 3) is the natural base layer for a future definition of the Ramsey number $R(k)$.

Difficulty

The central difficulty is that the bad events — "the $k$-set $s$ is monochromatic" — overlap heavily: a typical graph contains many monochromatic $k$-sets, so the union bound must be crude enough to survive the overlap. Concretely, the estimate $\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1$ holds for $N = 2^{\lfloor k/2 \rfloor}$ but fails for $N = 2^{\lfloor k/2 \rfloor+1}$; the naive "take one vertex more" step is where the argument breaks. A solver who tries to strengthen the bound will find the exponent is tight.

A second difficulty is purely formal: the uniform distribution over graphs has to be eliminated. The mission's statements do this by counting graphs with a fixed monochromatic $k$-set ($2^{1+\binom{N}{2}-\binom{k}{2}}$ of them) and applying the union-bound principle, so no probability theory enters the formalization.

Formalization scope

Representation. Graphs are SimpleGraph (Fin N): a relation on $N$ labeled vertices. A candidate set is a Finset (Fin N) of cardinality $k$; "monochromatic" is IsClique ∨ IsIndepSet on the graph; "no monochromatic $k$-set" is the predicate NoMonoK. All counting is cardinality of finite sets; monoCount N k G is the number of monochromatic $k$-sets of $G$.

Conventions. $N = 2^{\lfloor k/2 \rfloor}$ uses natural-number division, so for odd $k$ the graph lives on $2^{(k-1)/2}$ vertices — the standard reading of $R(k) > 2^{k/2}$. The hypothesis $k \ge 3$ is explicit. The theorem quantifies existence over all graphs; it does not define the Ramsey number $R(k)$ (a definition item for it, with the re-stated bound $R(k) > 2^{k/2}$, is a natural follow-up contribution).

Reusability. The union-bound principle, the monochromatic-$k$-set machinery, and the pair-count bound are all reusable beyond this mission. Welcome contributions: defining ramseyNumber and restating the bound as $R(k) > 2^{\lfloor k/2 \rfloor}$; the Erdős–Szekeres upper bound $R(k) \le 4^k$ as a companion mission; applications of the same principle elsewhere.

Selected references

• Paul Erdős, Some remarks on the theory of graphs, Bulletin of the American Mathematical Society 53(4), 1947, pp. 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-X — the source paper: main construction proving $R(k) > 2^{k/2}$.
• Noga Alon, Joel H. Spencer, The Probabilistic Method, 4th ed., Wiley, 2016 — Chapter 1 (the Erdős lower bound) and Chapter 3 (Lovász local lemma); standard exposition of the technique.
• Stanisław Radziszowski, Small Ramsey Numbers, Electronic Journal of Combinatorics, Dynamic Survey DS1 — survey of Ramsey number bounds and history.

Context: where this sits in the formalization landscape

This mission is not a duplicate of existing platform content, and the choice of target is deliberate:

• Mathlib gap. The pinned environment (mathlib 0df444a) contains no Ramsey-number theory at all — nothing in Combinatorics/SimpleGraph, no ramseyNumber-style definition. This mission seeds that subfield with reusable infrastructure: the monochromatic-set model, the finite union-bound (probabilistic-method) principle, and the double-counting bound are all general-purpose lemmas, not one-off steps.
• Existing Ramsey content is a different quantity. The platform's fully-proved Erdos183 mission concerns multicolour triangle Ramsey numbers $R(3,\dots,3)$ and is driven by recursive palette constructions — a different Ramsey parameter and a different technique. The classical 2-colour diagonal bound formalized here appears nowhere on the platform as a proved statement.
• Directly load-bearing for a live open problem. The public open problem diagonal_ramsey_asymptotics (same environment 0df444a) asks, eventually in $k$, for $2^{\lfloor k/2 \rfloor} \le R(k,k) \le 4^k$; its upper half is already proved as ramsey_theory_upper_bound. The lower half is exactly what this mission's goal supplies: once ramsey_lower_bound is proved, closing that open problem reduces to a translation between the graph formulation used here (SimpleGraph / NoMonoK) and the edge-colouring formulation (ramseyDiag) used there, plus the eventual-quantifier wrapper.
• Formalization convention. The bound is stated on $N = 2^{\lfloor k/2 \rfloor}$ vertices (natural-number division), matching the exponent convention of the existing platform open problem above. For even $k$ this is exactly Erdős's $2^{k/2}$; for odd $k$ it is the standard floor form, equivalent to the classical asymptotic reading $R(k)^{1/k} \ge \sqrt{2}$.

Motivation

Alternating permutations are a classical meeting point of enumerative combinatorics, permutation statistics, and special functions. An up--down permutation alternates between rises and falls, and their ordinary counts are the Euler secant and tangent numbers. Refining this count by the inversion statistic produces the $q$-secant polynomial $E_{2n}(q)$. Its values and congruences retain information that disappears after setting $q=1$: they distinguish how the alternating permutations are distributed by inversion number and reveal cancellation at roots such as $q=-1$. Ji-Cai Liu's article isolates the next nontrivial term in the $(1+q)$-adic expansion of this polynomial, strengthening an earlier Andrews--Foata congruence. The mission formalizes the article's main result, Theorem 1.1, as an exact polynomial-divisibility statement.

Setting

For $n\ge 0$, let $A(2n)$ be the set of permutations $\sigma=(\sigma_1,\ldots,\sigma_{2n})$ of $\{1,\ldots,2n\}$ satisfying

$$\sigma_1<\sigma_2>\sigma_3<\sigma_4>\cdots<\sigma_{2n}.$$

The empty permutation is the unique member of $A(0)$. The inversion number is

$$\operatorname{inv}(\sigma) =\#\{(i,j):1\le i<j\le 2n,\ \sigma_i>\sigma_j\}.$$

The $q$-secant inversion enumerator is the integer polynomial

$$E_{2n}(q)=\sum_{\sigma\in A(2n)}q^{\operatorname{inv}(\sigma)}\in\mathbb Z[q].$$

Congruence modulo $(1+q)^3$ means divisibility in $\mathbb Z[q]$: two polynomials $F$ and $G$ are congruent precisely when $(1+q)^3$ divides $F-G$. This formulation avoids evaluation at a single number and records the first three orders of behavior at $q=-1$.

In Lean, a permutation is represented as an equivalence of Fin (2*n). The alternating inequalities and inversion number are finite predicates and counts on this zero-based type. The polynomial variable is the canonical indeterminate in Polynomial ℤ.

Formalization targets

Cubic congruence

For every integer $n\ge0$, prove

$$E_{2n}(q)\equiv q^{2n(n-1)}-\binom n2(1+q)^2 \pmod{(1+q)^3}.$$

Equivalently,

$$(1+q)^3\mid E_{2n}(q)- \left(q^{2n(n-1)}-\binom n2(1+q)^2\right) \quad\text{in }\mathbb Z[q].$$

The boundary value $n=0$ is included. With the empty-permutation convention and natural-number truncated subtraction in the exponent, both sides reduce correctly, so the formal target does not hide a separate exceptional case.

Significance

The theorem identifies the exact quadratic correction to the highest-inversion monomial near $q=-1$. It therefore explains why the prior congruence modulo $(1+q)^2$ does not generally lift unchanged to the cubic modulus. Specializing at $q=1$ also yields the corresponding refinement modulo $8$ for the ordinary secant numbers. More broadly, the statement is a compact test case for formal reasoning that combines finite permutations, order predicates, inversion statistics, generating polynomials, binomial coefficients, and divisibility in a polynomial ring.

A machine-checked proof would contribute reusable infrastructure for permutation enumerators and polynomial congruences. The published article supplies a human proof; the Prove2me goal is the formal reconstruction of its theorem in Lean. The mission does not encode a proof certificate, an orbit count, or the desired divisibility inside a definition. A successful submission must derive the divisibility from the concrete finite definitions.

The result also gives a useful interface between two styles of formal combinatorics. On one side, alternating permutations are finite objects that can be enumerated, mapped, and partitioned. On the other, their aggregate is an algebraic object in $\mathbb Z[q]$ whose divisibility can be studied without referring to individual permutations. Infrastructure connecting these levels can be reused for other $q$-Euler numbers, descent and major-index enumerators, and congruences obtained from finite weighted actions. The mission keeps that infrastructure general-purpose by making the final target an equality in a quotient of the polynomial ring rather than a specialized computational procedure.

Difficulty

Direct expansion of $E_{2n}(q)$ is factorial in $n$ and gives no uniform explanation of divisibility by a third power. Divisibility by $(1+q)^3$ is stronger than merely checking the value at $q=-1$: it simultaneously constrains the value and the first two formal orders there. A formal solution must control the entire finite family of alternating permutations while preserving exact inversion exponents and polynomial coefficients. Index conventions are also delicate, because the paper numbers positions and values from $1$, whereas Lean uses Fin indices from $0$.

The source argument introduces combinatorial structure beyond the bare statement. Formalizers may contribute reusable lemmas about switching consecutive values, invariance of alternation under permitted switches, inversion-number changes, finite group actions, and divisibility of orbit enumerators. Those are natural milestones, but the present root goal deliberately remains the stable polynomial congruence rather than committing to one decomposition.

Formalization scope

The mission fixes the coefficient ring to $\mathbb Z$ and uses exact polynomial divisibility. It does not replace congruence by coefficientwise arithmetic modulo $8$, evaluation at $q=-1$, or a numerical check for bounded $n$. UpDown is defined directly on permutations of Fin (2*n), invNumber counts ordered index pairs with the required inequality, and qSecant is the finite sum of monomials $q^{\operatorname{inv}(\sigma)}$.

The formal statement quantifies over every natural number. The conventions at $n=0$ and $n=1$ are part of the same theorem and have been audited explicitly. The uploaded definition bundle is transparent and sorry-free; the only admitted declaration is the mission theorem itself. Useful contributions include general lemmas about polynomial divisibility, finite involutions and orbit sums, or bridges between one-based paper notation and Lean's finite types.

Selected references

• Ji-Cai Liu, A Combinatorial Proof of a Cubic Congruence for the $q$-Secant Inversion Enumerator, Electronic Journal of Combinatorics 33(3), P3.10, 2026. DOI

Motivation

A spanning subgraph in which every vertex has degree two may split into several cycles. Barnette’s question asks when planarity, bipartiteness, and connectivity force those vertices onto one cycle. The source is OpenAI's September 2026 manuscript.

Setting

A cubic graph has degree three at every vertex. A bipartite graph has two vertex classes with every edge crossing between them. A Hamiltonian cycle visits all vertices exactly once before returning to its starting point. Planarity is represented by a drawing using injective continuous edge arcs in the real plane.

Formalization targets

$$G\text{ finite, simple, cubic, bipartite, planar, and 3-vertex-connected}\ \Longrightarrow\ G\text{ has a Hamiltonian cycle}.$$

Every finite simple graph with decidable vertex equality and adjacency has a Hamiltonian cycle if each vertex has degree three, the vertices can be partitioned into two classes with every edge joining different classes, the graph is planar, and it is three-vertex-connected. Here planarity means that vertices can be placed at distinct points of the real plane and edges drawn as injective continuous arcs whose interiors contain no vertices and whose interiors are disjoint for distinct undirected edges; reversing an edge reverses its arc. Three-vertex-connectivity means that the graph has at least four vertices and remains connected after deletion of any set of at most two vertices. The conclusion is the existence of one closed cycle visiting every vertex exactly once before returning to its starting vertex.

The goal is OAI.Barnette.main.

Significance

A proof would turn the source’s Hamiltonicity claim into a result available for arbitrary finite graphs satisfying these exact hypotheses. It would also provide a reusable bridge between geometric embeddings and combinatorial walks. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Degree constraints do not guarantee that a spanning cycle cover is connected. The target requires a single cycle and must handle unrestricted face sizes, so verifying local degree conditions is insufficient.

Formalization scope

The published goal unfolds MainStatement. Three-vertex-connectivity requires at least four vertices and connectedness after deletion of any set of at most two vertices. The Hamiltonian object is a closed graph walk satisfying the cycle and vertex-coverage conditions. Stronger edge-avoidance conclusions from the paper are not attached as targets.

The shared definitions are supplied by BarnetteHamiltonian. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Paired states and Hamiltonian cycles in cubic bipartite planar graphs, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Status: complete. This mission records a finished formalization rather than an open call for work. Every statement below, including the goal, was uploaded together with a proof that the platform has verified, so there is nothing left to prove.

Motivation

The Lovász Local Lemma (LLL) is a basic tool of the probabilistic method. It shows that a collection of rare "bad" events can all be avoided simultaneously, even when the events are not independent, provided each event depends on only a few others. Its best-known application is to satisfiability: a $k$-CNF formula in which every variable appears in few clauses has a satisfying assignment.

Quantum satisfiability ($k$-QSAT) is the quantum analogue of $k$-SAT. Clauses are replaced by projectors acting on $k$ qubits, and the question is whether some nonzero state is annihilated by all of them, equivalently whether the corresponding local Hamiltonian is frustration-free. Bravyi showed that $k$-QSAT is $\mathsf{QMA}_1$-complete for $k \ge 4$, so sufficient conditions for satisfiability are of interest in quantum complexity theory and in many-body physics. Ambainis, Kempe and Sattath (arXiv:0911.1696, J. ACM 2012) proved a quantum version of the LLL in which probability is replaced by relative dimension, and derived a sufficient condition for $k$-QSAT instances to be satisfiable.

Timeline

• 1975. Erdős and Lovász introduce the local lemma, in the symmetric form, to colour hypergraphs (Infinite and Finite Sets, 1975).
• 1977. Spencer publishes the general (asymmetric) form, credited to Lovász, and applies it to Ramsey numbers (Discrete Math. 20, 1977).
• 1985. Shearer determines the optimal dependency condition, in terms of the independence polynomial of the dependency graph (Combinatorica 5, 1985).
• 2009 to 2010. Moser gives a constructive proof for $k$-SAT (arXiv:0810.4812, STOC 2009); Moser and Tardos make the general lemma constructive (arXiv:0903.0544, J. ACM 2010).
• 2011. Kolipaka and Szegedy show that the Moser and Tardos algorithm works throughout Shearer's region, giving an algorithmic proof of Shearer's bound (Moser and Tardos meet Lovász, STOC 2011, 235 to 244).
• 2009 to 2012. Ambainis, Kempe and Sattath prove the quantum local lemma and its $k$-QSAT corollaries (arXiv:0911.1696, J. ACM 59(5):24, 2012).
• 2013. Arad and Sattath (arXiv:1310.7766) and, independently, Schwarz, Cubitt and Verstraete (arXiv:1311.6474) give constructive versions for commuting projectors.
• 2016. Sattath, Morampudi, Laumann and Moessner extend Shearer's criterion to the quantum setting and conjecture that it is tight (arXiv:1509.07766, PNAS 2016).
• 2017. He, Li, Liu, Wang and Xia show that the abstract and variable versions of the local lemma differ: Shearer's bound, tight for the abstract version, is not tight for the variable version (the setting of $k$-SAT, where events are determined by independent variables) for instance when the base graph of the event-variable graph has an induced cycle of length at least 4, while there is no gap when it is a tree (arXiv:1709.05143, FOCS 2017).
• 2017. Gilyén and Sattath give an efficient quantum algorithm for the non-commuting case under a spectral gap condition (arXiv:1611.08571, FOCS 2017).
• 2018 to 2019. He, Li, Sun and Zhang prove this conjecture: Shearer's bound is tight for the quantum local lemma, so in this respect the quantum lemma behaves like the abstract version rather than the variable one; they also show that the tight regions of the quantum lemma and of its commuting variant differ in general (arXiv:1804.07055, STOC 2019).

Setting

Let $V$ be a nonzero finite-dimensional vector space. For a subspace $X \subseteq V$, the relative dimension is

$$R(X) = \frac{\dim X}{\dim V}.$$

It plays the role of probability: subspaces replace events, intersection replaces conjunction, and $R(X \mid Y) = \dim(X \cap Y)/\dim Y$ replaces conditional probability.

Subspaces $X_1, \dots, X_n$ have dependency sets $\Gamma(1), \dots, \Gamma(n) \subseteq \{1, \dots, n\}$ when, for every $i$ and every set $S$ of indices with $i \notin S$ and $S \cap \Gamma(i) = \emptyset$,

$$R\Big(X_i \cap \bigcap_{j \in S} X_j\Big) = R(X_i)\, R\Big(\bigcap_{j \in S} X_j\Big).$$

In words, $X_i$ is independent, for relative dimension, of every intersection of subspaces outside its dependency set.

A $k$-QSAT instance on $n$ qubits is a family of projectors $\Pi_1, \dots, \Pi_m$, each acting on a set of $k$ qubits and extended by the identity on the others. It is satisfiable if a nonzero state lies in the kernel of every $\Pi_i$.

The formalization proves the local lemma once, for an abstract valuation: a real function $R$ on a bounded lattice that is nonnegative, monotone and modular, $R(x) + R(y) = R(x \vee y) + R(x \wedge y)$, with $R(\top) = 1$ and $R(\bot) = 0$. Relative dimension on subspaces and the uniform probability on subsets of a finite set are the two instances used.

Formalization targets

Goal: the quantum local lemma (Theorem 14)

Let $X_1, \dots, X_n$ be subspaces with dependency sets $\Gamma(i)$, and let $0 \le y_i < 1$ satisfy $R(X_i) \ge 1 - y_i \prod_{j \in \Gamma(i)} (1 - y_j)$ for every $i$. Then

$$R\Big(\bigcap_{i=1}^{n} X_i\Big) \ \ge\ \prod_{i=1}^{n} (1 - y_i).$$

Other formalized results

All of these are proved on Prove2Me and can be found by name (tag quantum-lll):

1. The same statement for any valuation on a bounded lattice (Theorem 14, abstract form): QLLL.Valuation.lll.
2. The symmetric quantum local lemma: if $R(X_i) \ge 1 - p$, each $X_i$ has at most $d$ dependencies and $p \cdot e \cdot (d + 1) \le 1$, then $R(\bigcap_i X_i) > 0$ (Theorem 4): QLLL.quantum_lll_symmetric.
3. The classical Erdős and Lovász local lemma, asymmetric and symmetric (Theorems 13 and 1), for the uniform probability on a finite set: QLLL.SAT.classical_lll, QLLL.SAT.classical_lll_symmetric.
4. $k$-SAT: a $k$-CNF formula in which every variable appears in at most $2^k/(e k)$ clauses is satisfiable (Corollary 2): QLLL.SAT.sat_of_degree_le.
5. $k$-QSAT: an instance of rank-$\le r$ constraints in which every qubit appears in at most $2^k/(e r k)$ constraints is satisfiable (Corollary 16): QLLL.PiQSAT.inf_ker_extendOp_ne_bot on Mathlib's tensor product, and QLLL.QSAT.satisfiable_of_degree_le for orthogonal projectors.
6. Two results beyond the paper: infinite $k$-SAT (QLLL.SAT.exists_assignment_forall), and the local lemma for infinite index sets under a continuity hypothesis (QLLL.lll_iInf).

Significance

The quantum local lemma gives a sufficient condition for $k$-QSAT satisfiability that depends only on the local structure of the instance: the rank of the projectors and the number of projectors per qubit. It shows that the classical criterion survives the passage from events to subspaces, even though subspaces do not form a distributive lattice. Later work on constructive and tight versions, listed in the timeline, builds on this statement.

All results of this mission are proved and machine-checked. The Lean development was written as a complete formalization of the paper, and every statement here was uploaded together with a proof verified by the platform. What the mission adds is a reusable, Mathlib-based library: the local lemma for abstract valuations, its classical and quantum instances, $k$-QSAT stated on Mathlib's tensor product of qubits, and linear algebra on intersections of tensor products of subspaces that Mathlib does not yet contain. Mathlib currently has no form of the Lovász Local Lemma.

Difficulty

The classical proof uses complements of events and the identity $\Pr(A) + \Pr(A^c) = 1$, together with the distributive law for events. Subspaces satisfy neither in general: the lattice of subspaces is modular but not distributive, and the orthogonal complement does not distribute over intersections. The argument has to be rebuilt from the properties of relative dimension that do hold. For $k$-QSAT, the further difficulty is to show that constraints acting on disjoint sets of qubits are independent for relative dimension, which requires computing intersections and dimensions of tensor products of subspaces.

Formalization scope

Conventions committed to in the Lean statements:

1. The local lemma is stated for $n$ indexed subspaces (or lattice elements) and real weights $0 \le y_i < 1$. An index is never in its own dependency set's complement: independence is required from intersections over sets $S$ that avoid both $\Gamma(i)$ and $i$ itself.
2. Independence is stated in product form, $R(X \cap Y) = R(X) R(Y)$, which agrees with the conditional form of the paper whenever the conditional relative dimension is defined.
3. The quantum lemma holds over any field and requires $V$ to be nonzero and finite-dimensional.
4. The classical lemmas are stated for good events (complements of bad events) under the uniform probability on a finite nonempty set.
5. Qubits: the main $k$-QSAT statement uses Mathlib's tensor product $\bigotimes_{j} \mathbb{C}^2$ and allows arbitrary local operators of rank at most $r$, since only the dimension of their kernels enters. A second form, on functions from bit strings to $\mathbb{C}$, requires the constraints to be orthogonal projectors (idempotent and self-adjoint). Self-adjointness cannot yet be stated on Mathlib's $n$-fold tensor product, which has no inner product in the pinned Mathlib version.
6. Degree conditions are integers: "at most $2^k/(e r k)$ projectors per qubit" is written as at most $D' + 1$ with $\frac{r}{2^k} \cdot e \cdot (k D' + 1) \le 1$, which the paper's hypothesis implies.

An infinite version of $k$-QSAT is deliberately not included. Nonzero subspaces can have all finite intersections nonzero and zero total intersection, so the infinite statement has to be phrased with compatible families of density matrices, and the current Lean formulation does not yet restrict the constraints to positive operators.

The blueprint of the formalization, linking every paper statement to its Lean declaration, is at sattath.github.io/Quantum-Lovasz-Local-Lemma/blueprint. Natural extensions, outside the scope of this mission: the orthogonal-projector form of Corollary 16 on Mathlib's tensor product once inner products on $n$-fold tensor products are available, Shearer-type conditions, and a measure-theoretic classical local lemma on general probability spaces.

A note from the contributor

This is my first contribution to Prove2Me, so the definitions, statements, proofs and descriptions may fall short of what an experienced contributor would produce. Some choices may be unidiomatic, some lemmas may duplicate Mathlib, and the split into entries could be better. Every proof is checked by Lean, so the theorems are correct as stated; the question is whether they are stated in the most useful way.

Selected references

• P. Erdős and L. Lovász, Problems and results on 3-chromatic hypergraphs and some related questions, Infinite and Finite Sets, Colloq. Math. Soc. János Bolyai 10, 1975, 609 to 627.
• J. Spencer, Asymptotic lower bounds for Ramsey functions, Discrete Math. 20, 1977, 69 to 76.
• J. B. Shearer, On a problem of Spencer, Combinatorica 5, 1985, 241 to 245.
• R. A. Moser, A constructive proof of the Lovász local lemma, STOC 2009. arXiv:0810.4812
• R. A. Moser and G. Tardos, A constructive proof of the general Lovász local lemma, J. ACM 57(2), 2010. arXiv:0903.0544
• A. Ambainis, J. Kempe and O. Sattath, A quantum Lovász local lemma, J. ACM 59(5):24, 2012. arXiv:0911.1696
• I. Arad and O. Sattath, A constructive quantum Lovász local lemma for commuting projectors, 2013. arXiv:1310.7766
• M. Schwarz, T. S. Cubitt and F. Verstraete, An information-theoretic proof of the constructive commutative quantum Lovász local lemma, 2013. arXiv:1311.6474
• O. Sattath, S. C. Morampudi, C. R. Laumann and R. Moessner, When a local Hamiltonian must be frustration-free, PNAS 113(23), 2016. arXiv:1509.07766
• A. Gilyén and O. Sattath, On preparing ground states of gapped Hamiltonians: an efficient quantum Lovász local lemma, FOCS 2017. arXiv:1611.08571
• K. He, Q. Li, X. Sun and J. Zhang, Quantum Lovász local lemma: Shearer's bound is tight, STOC 2019. arXiv:1804.07055

All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph.

We strengthen the previously formalized $O(n^{2.99942})$ bound to $O(n^{2.9983})$ for deterministic APSP on directed graphs with polynomially bounded integer weights and no negative cycles, using the same word-RAM model. It formalizes the improvement outlined by Alman and Vassilevska Williams in their conclusion.

References:

1. Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, 2026, Theorems 17 and 19 and conclusion footnote 10.
2. Virginia Vassilevska Williams and Ryan Williams, Finding, Minimizing, and Counting Weighted Subgraphs, 2013, Theorem 3.3 and Proposition 3.4.
3. Virginia Vassilevska Williams and Ryan Williams, Subcubic Equivalences Between Path, Matrix, and Triangle Problems, 2018, Theorem 4.2.

Motivation

A Costas array is a permutation matrix in which the difference vectors between distinct dots are pairwise distinct; such arrays are frequency-hopping patterns for sonar and radar (Costas, 1984). Rubio and Torres ask whether their $m$-dimensional version can stay Costas in every window of its periodic extension, and conjecture that this happens only in the smallest order.

Timeline. 1984: Taylor proves that 2D periodic Costas arrays have order $\le 2$. 2023: Rubio–Torres prove the odd-order and 3D cases, give $2\times2\times4$ examples, and state Conjecture 1.

Setting

Let $[n]=\{1,\dots,n\}$, $X=[a_1]\times\cdots\times[a_k]$, $Y=[b_1]\times\cdots\times[b_l]$ with all sides $\ge2$, and $\varphi:X\to Y$ a bijection; the dots are $(x,\varphi(x))\in\mathbb Z^{k+l}$. The array is Costas if the difference vectors between distinct dots are distinct, and periodic Costas if moreover, after repeating the dots periodically over $\mathbb Z^{k+l}$, the dots inside every translate $t+X\times Y$ have distinct difference vectors.

Formalization target

Conjecture 1: if $k\ge l\ge1$ and $\varphi$ defines a periodic Costas array, then

$$\prod_{i=1}^k a_i=2^k,$$

equivalently every $a_i=2$. The condition $k\ge l$ is a normalization ($\varphi^{-1}$ swaps the boxes).

Significance

A proof would give the multidimensional analogue of Taylor's theorem; a counterexample would give periodic distinct-difference patterns of non-power-of-two order.

Difficulty

The Rubio–Torres counting argument needs a bound that is available only when $Y$ is one-dimensional, which is why it stops at $m=3$. Computational evidence: an exhaustive window check reports that the $2\times3\times2\times3$ array with dots $(1,1,1,1),(1,2,1,2),(1,3,2,1),(2,1,1,3),(2,2,2,3),(2,3,2,2)$ is periodic Costas, which would disprove the conjecture.

Formalization scope

A point of $\mathbb Z^{k+l}$ is a pair $(x,y)$; boxes are 1-based; $\varphi$ is a total function $\mathbb Z^k\to\mathbb Z^l$ whose values off $X$ are unused. Differences are plain integer vectors (not reduced modulo the sides), windows range over all $t\in\mathbb Z^{k+l}$, and $k,l\ge1$ and sides $\ge2$ are part of the definition, so no degenerate case holds vacuously.

Selected references

• I. Rubio, J. Torres, Multidimensional Costas Arrays and Their Periodicity, IEEE Trans. Inf. Theory 69(8), 2023, 5032–5040. arXiv:2208.02378, DOI
• J. P. Costas, A study of a class of detection waveforms having nearly ideal range-Doppler ambiguity properties, Proc. IEEE 72(8), 1984, 996–1009.
• S. W. Golomb, H. Taylor, Constructions and properties of Costas arrays, Proc. IEEE 72(9), 1984, 1143–1163.

Motivation

The Schur number $S(n)$ is the largest $N$ such that $[1, N] = \{1, \dots, N\}$ can be partitioned into $n$ sumfree sets, sets with no $x, y, z$ such that $x + y = z$ ($x = y$ allowed). Schur's argument gives $S(n) \le R_n(3) - 2$, where the triangle Ramsey number $R_n(3)$ is the least $N$ such that every colouring of the edges of $K_N$ with $n$ colours has a monochromatic triangle (Fredricksen–Sweet 2000, inequality (2)). Only $S(1), \dots, S(5) = 1, 4, 13, 44, 160$ are known (Heule 2018). For six colours the published range is $536 \le S(6) \le 1836$; the upper bound is $R_6(3) - 2$ with $R_6(3) \le 1838$ (DS1, rev. 18).

Timeline.

• 1955: Greenwood and Gleason prove $R_3(3) = 17$ and $R_{n+1}(3) \le (n+1)(R_n(3) - 1) + 2$ (Theorem 6) (doi).
• 1961: Baumert finds $S(4) = 44$ by computer, as reported by Fredricksen and Sweet; they and Heule cite Golomb–Baumert 1965 for it.
• 1973: Chung proves $R_4(3) \ge 51$ (doi).
• 1997: Wan bounds $R_n(3)$ and, for even $n \ge 6$, states $S_n < n!\,(e - e^{-1} + 3)/2 - n + 2$ (zbMATH 0882.05095 summary; doi). If his $S_n$ is the least $N$ that forces a monochromatic solution, this is the centred bound below, applied to his own bound on $R_{n-1}(3)$; if it is the largest $N$, it is $1$ above it. His proof was not read.
• 2000: Fredricksen and Sweet prove $S(6) \ge 536$ (doi).
• 2004: Fettes, Kramer and Radziszowski prove $R_4(3) \le 62$ (listed in DS1, which also lists $R_5(3) \le 307$).
• 2018: Heule proves $S(5) = 160$ with a certified SAT computation (AAAI-18; preprint arXiv:1711.08076).
• 2026: a public repository of M. Tatarevic gives a computer-assisted argument for $R_4(3) \le 61$. Its Lean development assumes that a family of 56,830 SAT instances is unsatisfiable, and the repository records solver results for them. The project of this mission's author produced LRAT certificates for all 56,830 instances and checked them; the report is in the repository's issue tracker. This mission does not depend on it.

The first target is a centred-interval bound: if $R_k(3) \le r$, then $S(k+1) \le 2(k+1)\lfloor (r-1)/2 \rfloor + 1$. With $R_4(3) \le 61$ the recursive bound gives $R_5(3) \le 302$, and the centred bound gives $S(6) \le 1801$; with $R_5(3) \le 307$ it gives only $1837$. The mission formalizes what a Schur colouring of $[1, 1801]$ with six colours would have to look like under $R_4(3) \le 61$.

Setting

All numbers are natural numbers, $\mathbb{N} = \{0, 1, 2, \dots\}$, and $[a, b] = \{a, \dots, b\}$.

Schur colourings and covers. A colouring with $n$ colours is a map $c : \mathbb{N} \to \mathrm{Fin}\,n$. It is a Schur colouring of $[1, N]$ (SchurColoring N c) if there are no $x, y \ge 1$ with $x + y \le N$ and $c(x) = c(y) = c(x + y)$, the case $x = y$ included. The cover form uses SumFree S and CoveredBySumFree X n ($X$ lies in the union of $n$ sumfree sets); for $n \ge 1$ the two bridge theorems pass between the two forms in both directions.

Triangle Ramsey property. $\mathrm{TR}(k, r)$ (TriangleRamsey k r): every colouring with at most $k$ colours of the pairs $x < y$ of a finite set of at least $r$ naturals has a monochromatic triangle. For $k \ge 1$ it is the inequality $R_k(3) \le r$.

Neighbourhoods. The difference colouring gives a pair $\{x, y\}$ the colour $c(|x - y|)$. For a Schur colouring of $[1, N]$ it has no monochromatic triangle on $[0, N]$, since $(y - x) + (z - y) = z - x$. Write

• $\Gamma_i(V, v) = \{\, w \in V : w \ne v,\ c(|v - w|) = i \,\}$ (colorNbhd c V v i);
• $V_m = \Gamma_{c(m+1)}([0, 2m+1], m)$, the central neighbourhood (centralNbhd c m), which contains $2m + 1$;
• $P_i = \Gamma_i(V_m, 2m+1)$, the endpoint neighbourhoods (endpointNbhd c m i).

The frontier. The frontier hypotheses are $\mathrm{TR}(k, u + 1)$, $2t = (k+1)u$, $m = (k+2)t$, and $c$ a Schur colouring of $[1, 2m + 1]$ with $k + 2$ colours. From the first two, $\mathrm{TR}(k + 1, 2t + 2)$ holds, and the centred bound excludes Schur colourings of $[1, 2m + 2]$ with $k + 2$ colours; $[1, 2m + 1]$ is the frontier interval. Six colours: $k = 4$, $u = 60$, $t = 150$, $m = 900$, $2m + 1 = 1801$.

Example. For $k = 1$, $u = 2$, $t = 2$, $m = 6$ (and $13 = S(3)$), the classes $\{1, 4, 7, 10, 13\}$, $\{2, 3, 11, 12\}$, $\{5, 6, 8, 9\}$ form a Schur colouring of $[1, 13]$, with $V_6 = \{2, 5, 7, 10, 13\}$ and endpoint neighbourhoods $\{2, 10\}$ and $\{5, 7\}$, both closed under $x \mapsto 12 - x$.

Formalization targets

Goal: six colours under $R_4(3) \le 61$

$$\mathrm{TR}(4, 61) \ \text{ and } \ c \text{ a Schur colouring of } [1, 1801] \text{ with six colours} \implies (1)\text{–}(5),$$

where $q = c(901)$, $V = V_{900}$ and $P_i = \Gamma_i(V, 1801)$:

1. each colour occurs $150$ times in $[1, 900]$;
2. $|V| = 301$;
3. $|\Gamma_i(V, v)| = 60$ for every $v \in V$ and every colour $i \ne q$;
4. $c(901 - d) = c(901 + d)$ for every $d \in [1, 900]$ with $c(d) = q$;
5. for every colour $i \ne q$: $|P_i| = 60$; $x \mapsto 1800 - x$ maps $P_i$ to itself without fixed points; and $c(|x - y|) \notin \{i, q\}$ for distinct $x, y \in P_i$.

The goal is a structure theorem under the hypothesis $R_4(3) \le 61$. It does not prove $S(6) \le 1800$, and it does not assert that a Schur colouring of $[1, 1801]$ with six colours exists; whether such a colouring, or the structure it would force, exists is open. The goal is the six-colour instance of the general theorems below.

Centred-interval bound

$$\mathrm{TR}(k, r) \implies \Bigl[1,\ 2(k+1)\Bigl\lfloor \tfrac{r-1}{2} \Bigr\rfloor + 2\Bigr] \text{ is not covered by } k + 1 \text{ sumfree sets.}$$

Balanced colour classes

$$\mathrm{TR}(k, 2t + 2),\ m = (k+1)t,\ c \text{ a Schur colouring of } [1, 2m+1] \text{ with } k + 1 \text{ colours} \implies \bigl|\{\, d \in [1, m] : c(d) = j \,\}\bigr| = t \ \text{ for every colour } j.$$

Nested saturation

$$\text{frontier hypotheses} \implies |\Gamma_i(V_m, v)| = u \qquad (v \in V_m,\ i \ne c(m+1)).$$

Automorphism extension

For a colouring $\mathrm{col}$ of ordered pairs, a finite set $W$, a point $e \notin W$ and a map $J$ with $J(W) \subseteq W$, $J \circ J = \mathrm{id}$ on $W$ and $\mathrm{col}(J(x), J(y)) = \mathrm{col}(x, y)$ on $W$:

$$v \in W \text{ and } J(v) \text{ have equal colour degrees in } W \cup \{e\} \implies \mathrm{col}(v, e) = \mathrm{col}(J(v), e).$$

Forced reflection

$$\text{frontier hypotheses} \implies c(m + 1 - d) = c(m + 1 + d) \qquad (d \in [1, m],\ c(d) = c(m+1)).$$

The saturation degree is even

$$\text{frontier hypotheses} \implies u \text{ is even}.$$

Significance

The result itself. Under $R_4(3) \le 61$, $S(6) \le 1801$, and the goal constrains a six-colour Schur colouring of $[1, 1801]$ as listed above. In particular, each of its five endpoint neighbourhoods is a set of $30$ pairs $\{900 - d, 900 + d\}$ whose difference colouring uses at most four colours, is invariant under $x \mapsto 1800 - x$ and, like that of every subset of $[0, 1801]$, has no monochromatic triangle. So such a colouring yields five colourings of $K_{60}$ with at most four colours, no monochromatic triangle and a fixed-point-free colour-preserving involution. A proof that this configuration cannot occur would give $S(6) \le 1800$ under the same hypothesis. Whether it can occur, and whether $S(6) \le 1800$, are open.

Formalizing it. All 12 theorems of the tree, the goal included, are proved in Lean 4 with Mathlib over the bundles ClassicalSchurBasic, ClassicalSchurRamsey and ClassicalSchurColoring, with the axioms propext, Classical.choice and Quot.sound only. Independent Claude agents checked the Lean: one rebuilt the frontier theorems, re-ran their axiom audit and checked their statements against the argument; another checked every statement of the tree against the mathematics. The mathematics is in the paper $S(6) \le 1801$ if $R_4(3) \le 61$: a centred Schur bound and the structure at the frontier (A. McKenna, Zenodo, 2026, doi:10.5281/zenodo.23156099), and the Lean code is in its repository; the paper has not been refereed. $R_4(3) \le 61$ is not formalized in the mission.

Difficulty

The centred bound counts, for one colour class, the points $h \pm a$ around the centre of the interval. At the frontier every such count is tight: each colour has $t$ elements in $[1, m]$, and inside $V_m$ each colour other than $c(m+1)$ has degree $u$, the largest value that $R_k(3) \le u + 1$ allows. So no single counting step gives a contradiction, and the theorems describe the tight case instead of excluding it. The first exclusion that the structure gives, parity, works only for odd $u$; at six colours $u = 60$.

The reflection is not a property of Schur colourings in general: the colouring $\{1, 4\}$, $\{2, 3\}$, $\{5\}$ of $[1, 5]$ has $c(2) = c(3)$ but $c(1) \ne c(5)$. At the frontier the theorem asserts it only for the $d$ with $c(d) = c(m+1)$, so an argument that assumes a fully symmetric colouring proves a different statement. A direct search is no substitute: $S(5) = 160$ already needed a large certified SAT computation (Heule 2018), and $[1, 1801]$ with six colours is a much larger instance.

Formalization scope

• Colourings are functions ℕ → Fin n on all of $\mathbb{N}$; SchurColoring N c constrains only $[1, N]$, with $x = y$ allowed. Distances are Nat.dist.
• Neighbourhoods are Finsets. $V_m$ lies in range (2 * m + 2) $= [0, 2m+1]$, so the point $0$ is a candidate member; the centre $m$ never is.
• TriangleRamsey k r takes colours from any Finset of at most $k$ naturals; the pair colouring ℕ → ℕ → ℕ is constrained only on the pairs $x < y$ of the vertex set, which is any finite set of naturals. TriangleRamsey k 0 and TriangleRamsey k 1 are false.
• Covers. CoveredBySumFree X n uses Fin n → Set ℕ; the sets need not be disjoint or lie in $X$.
• Subtraction is truncated. Under the hypotheses, none of $r - 1$, $N - 1$, $m + 1 - d$, $2m - x$ (with $x \in P_i$), $901 - d$ and $1800 - x$ truncates.
• No trivialization. The frontier theorems are vacuous for $u = 0$, and for $k = 0$ (then $[1, 2m + 1] \supseteq [1, 5]$, while $S(2) = 4$). For $k = 1$ they are not: the Schur colourings of $[1, 13]$ meet the hypotheses, and every conclusion can be checked by hand. The goal holds vacuously if $R_4(3) > 61$ or if no six-colour Schur colouring of $[1, 1801]$ exists; it is a structure theorem, not a claim that such a colouring exists.

Bundles: ClassicalSchurBasic (SumFree, CoveredBySumFree) and ClassicalSchurRamsey (TriangleRamsey) are already public; ClassicalSchurColoring holds SchurColoring, colorNbhd, centralNbhd and endpointNbhd. Reusable: the colouring–cover bridges, the pigeonhole step, the centred bound for every $k$, and the automorphism-extension lemma (arbitrary types). Welcome beyond the targets: a formal proof of TriangleRamsey 4 61, and results on whether the configuration of five paired $60$-point sets exists.

Provenance: the centred-interval argument was first written by an AI agent based on ChatGPT (OpenAI) in a project discussion on 2026-09-27, and a Claude (Anthropic) agent audited it. The balance, saturation and reflection argument was proposed by an AI agent based on ChatGPT (OpenAI) in a project discussion; Claude checked each step and restated it with explicit hypotheses. Claude wrote the Lean proofs of both parts; the independent checks are described under Formalizing it.

Selected references

• R. E. Greenwood, A. M. Gleason, Combinatorial relations and chromatic graphs, Canad. J. Math. 7 (1955) 1–7. https://doi.org/10.4153/CJM-1955-001-4
• S. W. Golomb, L. D. Baumert, Backtrack programming, J. ACM 12 (1965) 516–524. https://doi.org/10.1145/321296.321300
• F. R. K. Chung, On the Ramsey numbers $N(3, 3, \dots, 3; 2)$, Discrete Math. 5 (1973) 317–321. https://doi.org/10.1016/0012-365X(73)90125-8
• H. Fredricksen, M. M. Sweet, Symmetric sum-free partitions and lower bounds for Schur numbers, Electron. J. Combin. 7 (2000) #R32. https://doi.org/10.37236/1510
• M. J. H. Heule, Schur number five, Proc. AAAI Conf. Artif. Intell. 32 (2018). https://doi.org/10.1609/aaai.v32i1.12209 ; preprint arXiv:1711.08076 (2017). https://arxiv.org/abs/1711.08076
• S. P. Radziszowski, Small Ramsey numbers, Electron. J. Combin., Dynamic Survey DS1, revision 18, 2026. https://doi.org/10.37236/21
• M. Tatarevic, An improved upper bound for the Ramsey number R(3,3,3,3), GitHub repository, 2026, commit ddd7755. https://github.com/milostatarevic/r3333-upper-bound/commit/ddd7755476db3f0751181db0daec75342576cdd1
• A. McKenna, $S(6) \le 1801$ if $R_4(3) \le 61$: a centred Schur bound and the structure at the frontier, Zenodo, 2026. https://doi.org/10.5281/zenodo.23156099 ; Lean code: https://github.com/mysticflounder/schur-centred-bound (release v1.0.1).

Motivation

A set of integers is sumfree when no two of its elements, equal or distinct, add up to an element of the set. The Schur number $S(n)$ is the largest $N$ such that $\{1, \dots, N\}$ can be partitioned into $n$ sumfree sets; only $S(1), \dots, S(5) = 1, 4, 13, 44, 160$ are known. For $n \ge 4$ the best theoretical upper bound that Eliahou and Revuelta could cite in 2021 was $S(n) \le R_n(3) - 2$, where the Ramsey number $R_n(3)$ is the least $N$ such that every $n$-colouring of the edges of the complete graph $K_N$ has a monochromatic triangle. The Ramsey numbers satisfy $R_n(3) \le n\,(R_{n-1}(3) - 1) + 2$ for $n \ge 2$ (Greenwood–Gleason 1955); for $S(n)$ the paper knows no recursive upper bound.

Eliahou and Revuelta proposed a conjectural one. They defined a number $L(n)$ through the Schur degree of block-sum sets, proved $S(n) \le n\,L(n)$ (Theorem 5.4) and $S(n-1) + 1 \le L(n) \le R_{n-1}(3) - 1$ (Proposition 5.3), and conjectured $L(n) = S(n-1) + 1$ (Conjecture 5.6). This would give $S(n) \le n\,(S(n-1) + 1)$ (Conjecture 5.7) and $S(6) \le 966$ (Conjecture 5.8), against the range $536 \le S(6) \le 1836$ that they give. For $n = 4$ they proved $14 \le L(4) \le 16$, conjectured $L(4) = 14$, and left the value open.

Timeline.

• 1955: Greenwood and Gleason prove $R_3(3) = 17$ and the recursive bound above.
• 1961: Baumert computes $S(4) = 44$ (cited by Eliahou–Revuelta as reference [2]).
• 2000: Fredricksen and Sweet prove $S(6) \ge 536$ (doi).
• 2004: Fettes, Kramer and Radziszowski prove $R_4(3) \le 62$ (listed in DS1, rev. 18).
• 2018: Heule proves $S(5) = 160$ with a certified SAT computation (arXiv:1711.08076).
• 2020–2021: Eliahou and Revuelta, preprint arXiv:2006.01502 and refereed version, with the same numbering of the items used here.
• 2026: McKenna, The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49 (Zenodo, doi:10.5281/zenodo.22987189), proves $L(4) = 16$ and $L(5) \ge 49$; its Lean library ClassicalSchur formalizes both, with $L(5) \le 65$.

Setting

All numbers are natural numbers, except in the group $G$ below.

Sumfree sets. A set $S$ is sumfree when the sum of two of its elements, equal or distinct, is never in $S$. A set $X$ is covered by $n$ sumfree sets when it lies in the union of $n$ sumfree sets.

Schur degree. The Schur degree $\operatorname{sdeg}(X)$ is the least $n \ge 1$ such that $n$ sumfree sets cover $X$. If there is no such $n$, it is $\infty$.

For example, $\operatorname{sdeg}(\{1, \dots, N\}) \le n$ holds for $N \le S(n)$ and fails for $N > S(n)$.

Block sums. Let $A = (a_1, \dots, a_L)$ be a finite sequence of length $|A| = L$. Its block sums are the sums of runs of consecutive entries:

$$a_i + a_{i+1} + \dots + a_j \qquad (1 \le i \le j \le L).$$

The set of these sums is $\hat A$. The average of $A$ is the rational number $\mu(A) = (a_1 + \dots + a_L)/L$.

The number $L(n)$. A length $L$ has the ER property for $n$ when every sequence $A$ of $L$ positive integers with $\mu(A) \le n$ has $\operatorname{sdeg}(\hat A) \ge n$.

For $n \ge 2$, the inequality $\operatorname{sdeg}(\hat A) \ge n$ holds when no $n - 1$ sumfree sets cover $\hat A$. It fails when some $n - 1$ sumfree sets cover $\hat A$.

The number $L(n)$ is the least $L \ge 1$ with the ER property for $n$.

The pigeonhole bound. Let $\rho(0) = 2$ and $\rho(k+1) = (k+1)(\rho(k) - 1) + 2$. The first values are $\rho(1) = 3$, $\rho(2) = 6$, $\rho(3) = 17$ and $\rho(4) = 66$.

For $k \ge 1$, $\rho(k)$ is an upper bound for the Ramsey number: $R_k(3) \le \rho(k)$, with equality for $k \le 3$.

The group $G$. Let $G = \mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2}$. A set $C \subseteq G$ is sumfree in $G$ when the sum in $G$ of two of its elements, equal or distinct, is never in $C$.

The lifted sequence. Take $m_1 \ge 1$ and $M \ge m_1$. Write the $m_1 m_2$ numbers $u + Mj$, with $0 \le u < m_1$ and $0 \le j < m_2$, in increasing order:

$$x_0 < x_1 < \dots < x_{m_1 m_2 - 1}.$$

The lifted sequence is the sequence of the $m_1 m_2 - 1$ gaps between consecutive terms, $x_1 - x_0, \dots, x_{m_1 m_2 - 1} - x_{m_1 m_2 - 2}$. Lemma 4.1 below uses it to turn a cover of $G \setminus \{0\}$ into a sequence in ℕ.

Lean names.

• SumFree S: $S$ is sumfree.
• CoveredBySumFree X n: $X$ is covered by $n$ sumfree sets.
• sdeg X : ℕ∞: the Schur degree, with ⊤ for $\infty$.
• blockSums A and average A, for A : List ℕ: $\hat A$ and $\mu(A)$.
• ERProperty n L: the length $L$ has the ER property for $n$.
• erL n: $L(n)$.
• ramseyBound k: $\rho(k)$.
• GroupSumFree C: $C$ is sumfree in $G$. The Lean definition takes any type with an addition; the targets use it for ZMod m₁ × ZMod m₂.
• liftPrefix m₁ M L: $x_L$, defined for all $m_1$ and $M$ by $x_L = (L \bmod m_1) + M \lfloor L/m_1 \rfloor$.
• liftSeq m₁ m₂ M: the lifted sequence, defined for all $m_1$, $m_2$ and $M$ as the list of the $m_1 m_2 - 1$ differences $x_{k+1} - x_k$.

Formalization targets

Goal

$$\mathrm{erL}\ 4 = 16$$

An exact value, so no later result changes the statement; it is the case Eliahou and Revuelta left open.

Theorem 4.1 of Eliahou–Revuelta, in ℕ, with $\rho(k)$ for $R_k(3)$

$$\rho(k) \le |A| + 1 \implies k + 1 \le \operatorname{sdeg}(\hat A) \qquad (k \in \mathbb{N},\ A \text{ a finite sequence in } \mathbb{N}).$$

Upper bound of Proposition 5.3, with $\rho(k)$ for $R_k(3)$

$$\mathrm{erL}(k+1) \le \rho(k) - 1 \qquad (k \in \mathbb{N}).$$

No length below 16 has the property at $n = 4$

$$\neg\,\mathrm{ERProperty}\ 4\ L \qquad (1 \le L \le 15).$$

Lemma 4.1 (McKenna 2026): lift from a group

For $m_1, m_2, q \ge 1$, $M \ge 3m_1 - 2$ and sets $C_1, \dots, C_q$, sumfree in $G$, that cover $G \setminus \{0\}$, the sequence $A =$ liftSeq m₁ m₂ M satisfies

$$|A| = m_1 m_2 - 1, \quad a_i > 0, \quad \operatorname{sdeg}(\hat A) \le q, \quad a_1 + \dots + a_L = x_L \ \ (L \le m_1 m_2 - 1).$$

Corollary 4.2 (McKenna 2026): group coverings bound $L(n)$ from below

For $n \ge 3$, $m_1, m_2 \ge 1$ and $n - 1$ sets, sumfree in $G$, that cover $G \setminus \{0\}$:

$$m_1 m_2 \le \mathrm{erL}\ n.$$

Theorem 1.2 (McKenna 2026), with the Lean upper bound: bounds for $L(5)$

$$49 \le \mathrm{erL}\ 5 \le 65.$$

Significance

$L(4) = 16$. At $n = 4$, Conjecture 5.6 predicts $L(4) = S(3) + 1 = 14$. So $L(4) = 16$ refutes the conjecture at $n = 4$. Here $L(n)$ equals the upper bound $R_{n-1}(3) - 1$ of Proposition 5.3.

The two bounds of Proposition 5.3 coincide at $n = 2, 3$, where the paper gives $L(2) = 2$ and $L(3) = 5$. So $n = 4$ is the first case in which the conjecture says more than Proposition 5.3.

$L(5) \ge 49$. At $n = 5$, Conjecture 5.6 predicts $L(5) = S(4) + 1 = 45$. So $L(5) \ge 49$ refutes the conjecture at $n = 5$.

What remains open. Conjectures 5.7 and 5.8 remain open.

The paper derives Conjecture 5.7 at each $n$ from Conjecture 5.6 at the same $n$, with Theorem 5.4. At $n = 4, 5$ that derivation is not available. But Conjecture 5.7 holds there by the known values: $44 \le 4 \cdot 14$ and $160 \le 5 \cdot 45$.

Conjecture 5.8 follows from Conjecture 5.6 at $n = 6$ (that is, $L(6) = 161$) with Theorem 5.4. Nothing here decides that case.

With $L(4) = 16$, Theorem 5.4 gives only $S(4) \le 64$. This is weaker than $S(4) \le R_4(3) - 2 \le 60$.

Status. Every target is proved and formalized.

• Theorem 4.1 and Proposition 5.3 are proved in the refereed paper.
• $L(4) = 16$ (Theorem 1.1), Lemma 4.1, Corollary 4.2 and $L(5) \ge 49$ (Theorem 1.2) are proved in McKenna 2026 (doi:10.5281/zenodo.22987189). Before publication, separate agents, with their own code, checked the proofs in two rounds of adversarial audit.

At launch, all 12 theorems of the tree, the goal included, are Proved in Lean over 4 definition bundles. Their only axioms are propext, Classical.choice and Quot.sound.

An independent verifier checked the definitions and the six headline statements against Eliahou–Revuelta and McKenna 2026. The six statements are the goal, Theorem 4.1, Proposition 5.3, Lemma 4.1, Corollary 4.2 and Theorem 1.2.

Literature. The literature search for McKenna 2026 found no result on $L(4)$, $L(5)$ or Conjectures 5.6–5.8. One citing text, in Jungić 2023, was not read. This records the search; it is not a claim of priority.

Open work, not targets.

• The exact $L(5)$: $49 \le L(5) \le 61$ on paper (with $R_4(3) \le 62$), and $49 \le L(5) \le 65$ in Lean.
• The case $n = 6$: $161 \le L(6) \le R_5(3) - 1 \le 306$ (DS1: $R_5(3) \le 307$). Here Conjecture 5.6 is the open step toward $S(6) \le 966$.

Difficulty

Two kinds of bound. The two sides of an exact value of $L(n)$ are statements of different kinds.

An upper bound $L(n) \le m$ needs one length. It follows from $\operatorname{sdeg}(\hat A) \ge n$ for every sequence $A$ of positive integers of one length $L$, with $1 \le L \le m$ and average at most $n$.

A lower bound $L(n) \ge m$ needs every shorter length. For every $L$ with $1 \le L < m$, it needs a sequence of $L$ positive integers, with average at most $n$, whose block sums are covered by $n - 1$ sumfree sets.

One counterexample at length $m - 1$ is not enough. A sequence of length $L + 1$ and average at most $n$ need not contain $L$ consecutive entries of average at most $n$. So monotonicity in $L$ does not follow directly from the definition.

The average bound. The lower bound $S(n-1) + 1$ of Proposition 5.3 comes from the constant sequence $(1, \dots, 1)$, with $\hat A = \{1, \dots, L\}$. Conjecture 5.6 states that at length $S(n-1) + 1$, no sequence of average at most $n$ has $\operatorname{sdeg}(\hat A) \le n - 1$.

Without the bound on the average, this fails. The paper gives a sequence of length 14 with $\operatorname{sdeg}(\hat A) = 3$, found by semi-random search. Its average is 114, and the authors remark that such examples "are hard to come by".

The gap for $L(5)$. The gap from 49 to 61 is open. By McKenna 2026 (§5), the construction of Corollary 4.2 gives nothing above 49 at $n = 5$:

• $S(4) = 44$ excludes the cyclic groups of order at least 46.
• Solver runs exclude the non-cyclic groups of order 50 to 60. Their unsatisfiability proofs (in the DRAT format) were checked.
• $L(5) \le 61$ excludes the orders of 62 or more.

McKenna 2026 knows no sequence of length 49 with average at most 5 and $\operatorname{sdeg}(\hat A) \le 4$; such a sequence would give $L(5) \ge 50$.

Formalization scope

• Ambient ℕ. The paper works in an abelian group; here sets are Set ℕ and sequences List ℕ. For $X \subseteq \mathbb{N}$ the Schur degree is the same in ℕ and in ℤ. Theorem 4.1 is formalized for sequences in ℕ only.
• sdeg is sInf in ℕ∞, so it is ⊤ when no cover exists, and $\operatorname{sdeg}(\emptyset) = 1$. Covers are Fin n → Set ℕ; the sets need not be disjoint or inside $X$. Each lower bound on sdeg must exclude every cover.
• blockSums A uses B <:+: A with B ≠ []; average [] = 0 is never used, since erL requires $L > 0$.
• erL n is sInf {L | 0 < L ∧ ERProperty n L} in ℕ, defined for every $n$ (the paper: $n \ge 2$). As sInf ∅ = 0, an upper bound on erL alone would hold if no length had the property; the Theorem 4.1 target excludes this, giving ERProperty (k+1) at length $\rho(k) - 1 \ge 1$, and 0 satisfies neither the goal nor the lower bounds.
• Ramsey bound. $\rho(k)$ replaces $R_k(3)$. TriangleRamsey k N says every colouring of the pairs $x < y$ of at least $N$ naturals with at most $k$ colours has a monochromatic triangle; the tree proves it for $N = \rho(k)$. As $\rho(4) = 66 > 62 \ge R_4(3)$, the Lean upper bound for $L(5)$ is 65, not 61.
• Lemma 4.1, Corollary 4.2. As in McKenna 2026, the sets need only cover $G \setminus \{0\}$, and Lemma 4.1 requires $q \ge 1$: for $q = 0$, $m_1 = m_2 = 1$ the sequence is empty and $\operatorname{sdeg}(\emptyset) = 1$. The prefix sums are exact: $x_L$.
• Subtraction is truncated; with $m_1, m_2 \ge 1$ and $\rho(k) \ge 2$, none of 3 * m₁ - 2, m₁ * m₂ - 1, ramseyBound k - 1 and n - 1 in Fin (n - 1) ($n \ge 3$) truncates, and the differences in liftSeq do not truncate when $M \ge m_1 \ge 1$.
• Finite checks use kernel decide; no native_decide, no external certificate.

Bundles: ClassicalSchurBasic (the objects of the Setting), ClassicalSchurRamsey (TriangleRamsey, ramseyBound), ClassicalSchurLift (GroupSumFree, liftPrefix, liftSeq), ClassicalSchurValues (the finite data of the two value theorems). As a check, the definitions give the paper's values erL 2 = 2 and erL 3 = 5 (checked in Lean by an independent verifier in a scratch file; not in the tree). Reusable: the definitions of ClassicalSchurBasic (the interface lemmas are inlined in the proofs, not separate nodes), TriangleRamsey k (ramseyBound k), and the lift from group coverings. Welcome beyond the targets: a formal TriangleRamsey 4 62, which with not_coveredBySumFree_blockSums gives $L(5) \le 61$ in Lean; the exact $L(5)$; the case $n = 6$.

Selected references

• S. Eliahou, M. P. Revuelta, The Schur degree of additive sets, Discrete Math. 344 (2021) 112332. https://doi.org/10.1016/j.disc.2021.112332
• S. Eliahou, M. P. Revuelta, The Schur degree of additive sets, preprint, arXiv:2006.01502v1, 2020. https://arxiv.org/abs/2006.01502v1
• R. E. Greenwood, A. M. Gleason, Combinatorial relations and chromatic graphs, Canad. J. Math. 7 (1955) 1–7. https://doi.org/10.4153/CJM-1955-001-4
• H. Fredricksen, M. M. Sweet, Symmetric sum-free partitions and lower bounds for Schur numbers, Electron. J. Combin. 7 (2000) #R32. https://doi.org/10.37236/1510
• M. J. H. Heule, Schur number five, Proc. AAAI-18, 2018; preprint arXiv:1711.08076, 2017. https://arxiv.org/abs/1711.08076
• S. P. Radziszowski, Small Ramsey numbers, Electron. J. Combin., Dynamic Survey DS1, revision 18, 2026. https://doi.org/10.37236/21
• A. McKenna, The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49, Zenodo, 2026. https://doi.org/10.5281/zenodo.22987189 (version 1.0.1: https://doi.org/10.5281/zenodo.22987688). The Lean library ClassicalSchur and the comparator check: https://github.com/mysticflounder/schur-degree-block-sums (tag v1.0.1).