Combinatorics

Motivation

The Ramsey number R(5,5) has remained open since the 1960s. The best known bounds are 43 ≤ R(5,5) ≤ 48, where the lower bound was first established by Exoo (1989) via computational search. This mission formalizes an independent verification using novel GF(p) polynomial seeding.

Setting

The Ramsey number R(s,t) is the smallest n such that every 2-coloring of the complete graph K_n contains either a red K_s or a blue K_t.

Formalization target

Goal: R(5,5) ≥ 43

Established by exhibiting an explicit 2-coloring of K₄₂ with no monochromatic K₅.

Significance

This mission produces a machine-verified certificate of R(5,5) ≥ 43 via the first formalized GF(p) polynomial construction for Ramsey colorings.

Difficulty

The central difficulty is scale: verifying zero violations requires checking all C(42,5) = 850,668 five-element subsets.

Formalization scope

• Graphs as finite types
• 2-colorings as Bool-valued functions
• Violation count via finite enumeration
• GF(43) polynomial witness

Selected references

• Exoo, G. A lower bound for R(5,5). J. Graph Theory, 1989.
• Daugherty, B. et al. R(5,5) ≥ 43: Computational Proof via GF(p) Polynomial Seeding. Zenodo, 2026. DOI: 10.5281/zenodo.19405505

Motivation

A quantum memory stores logical qubits in many physical qubits so that errors can be detected and corrected. The overhead of doing so, measured by how many physical qubits are spent per logical qubit at a given error-correcting power, is one of the main costs of fault-tolerant quantum computation. Bivariate-bicycle (BB) codes are currently the leading low-overhead family: the gross code $[[144,12,12]]$ of Bravyi et al. (Nature, 2024) stores 12 logical qubits at distance 12 using 144 data qubits, roughly a tenth of the overhead of a surface code with the same distance, and it is the basis of a published hardware roadmap. The search for higher-rate members of the family is active, and the claims made in it are claims about the exact distance of explicit finite codes. These are finite but very large computations, and they are rarely checked independently.

Timeline.

• 2004 — MacKay, Mitchison and McFadden introduce bicycle codes: CSS codes built from a pair of circulant matrices.
• 2013 — Kovalev and Pryadko generalize the construction to commuting pairs of group-algebra elements (generalized bicycle codes).
• 2024 — Bravyi, Cross, Gambetta, Maslov, Rall and Yoder define BB codes over $\mathbb Z_l\times\mathbb Z_m$ and give the ladder $[[72,12,6]]$, $[[90,8,10]]$, $[[108,8,10]]$, $[[144,12,12]]$, $[[288,12,18]]$, with $[[360,12,\le 24]]$ left with only an upper bound.
• 2026 — An evolutionary search by Cruz-Benito et al. (arXiv:2606.02418) reports $[[288,16,12]]$ as its best indecomposable weight-6 code at distance 12.
• 2026 — Daugherty, Ryan and Ward give two new $[[336,20,12]]$ codes and a new $[[360,24,12]]$ code. They certify the exact distances of the whole ladder, establish $d=24$ for $[[360,12]]$, and show by enumeration that no connected three-term weight-6 BB code with $n\le 360$ and $k\ge 20$ has distance 13 or more.

Setting

Fix positive integers $l,m$ and let $G=\mathbb Z_l\times\mathbb Z_m$. The monomial $x^iy^j$ of the ring $\mathbb F_2[x,y]/(x^l-1,\,y^m-1)$ is identified with $(i,j)\in G$. A polynomial $P$ with coefficients in $\mathbb F_2$ is identified with its support, the finite set of monomials with coefficient $1$. The circulant of $P$ is the $G\times G$ binary matrix with a $1$ in row $g$, column $h$ exactly when $h-g\in P$.

Given two polynomials $A,B$, the BB code $\mathrm{BB}(A,B)$ acts on $n=2lm$ qubits, arranged in two blocks indexed by $G$. Its check matrices are

$$H_X=[\,A\mid B\,],\qquad H_Z=[\,B^{\mathsf T}\mid A^{\mathsf T}\,],$$

where $A$ and $B$ also denote their circulants. Because $G$ is abelian, $H_XH_Z^{\mathsf T}=AB+BA=0$ over $\mathbb F_2$, so this is a CSS code. Its parameters are:

1. the number of logical qubits $k=n-\operatorname{rank}H_X-\operatorname{rank}H_Z$, with ranks over $\mathbb F_2$;
2. the Z-distance $d_Z$, the least Hamming weight of a vector $v\in\mathbb F_2^n$ with $H_Xv=0$ and $v\notin\operatorname{row}(H_Z)$ (a nontrivial Z-logical);
3. the X-distance $d_X$, defined dually: $H_Zv=0$ and $v\notin\operatorname{row}(H_X)$.

The code is $[[n,k,d]]$ when $d_X=d_Z=d$. Each check of a code built from two three-term polynomials touches six qubits (weight 6). The Tanner graph joins each qubit to the X- and Z-checks acting on it, and the code is connected when this graph is connected.

Formalization targets

Goal: the three new codes

$$\mathrm{BB}_{\mathbb Z_2\times\mathbb Z_{84}}\!\left(1+y+xy^{5},\;1+y^{4}+y^{62}\right)=[[336,20,12]],$$ $$\mathrm{BB}_{\mathbb Z_2\times\mathbb Z_{84}}\!\left(1+y+xy^{5},\;1+y^{20}+y^{46}\right)=[[336,20,12]],$$ $$\mathrm{BB}_{\mathbb Z_6\times\mathbb Z_{30}}\!\left(1+y+xy^{2},\;1+y^{8}+x^{2}y^{16}\right)=[[360,24,12]],$$

each with $d_X=d_Z=12$ (Table 9 of the source). Each new code is also a milestone on its own.

Milestones

• Lemma 1 (minimality). In any parity system, no nonempty proper subset of a minimum-weight logical is even on every check.
• Table 3, the certified ladder. $[[72,12,6]]$, $[[90,8,10]]$, $[[108,8,10]]$, $[[144,12,12]]$, $[[288,12,18]]$ and $[[360,12,24]]$, all with $d_X=d_Z$, for the polynomials of Bravyi et al.
• Section 6, the weight-6 envelope. Every connected BB code built from two three-term polynomials with $n\le 360$ and $k\ge 20$ has a nontrivial X- or Z-logical of weight at most 12. In words, none has distance 13 or more.

Significance

The result. The new codes encode 25% and 50% more logical qubits at distance 12 than the best weight-6 code reported by evolutionary search, with figures of merit $kd^2/n$ of 8.57 and 9.60. The ladder distances turn published values, several of them previously supported only by heuristic searches or upper bounds, into exact statements. In particular $d([[360,12]])=24$ settles an upper bound left open by Bravyi et al. The envelope statement is a negative result: within this family and size range, distance 12 is the ceiling at $k\ge 20$.

Formalizing it. In the source, each lower bound on a distance is a DRAT refutation or a replayable proof tree, checked by external programs. Only the pruning lemma (Lemma 1) has a machine-checked proof, in Lean 4. A complete formalization would make the code parameters kernel-checked facts about explicit Mathlib objects, independent of every external checker. Upper bounds on distance and the values of $k$ are finite linear-algebra facts. Lower bounds are exhaustive statements over $\binom{n}{w}$-sized spaces and are the core of the work.

Difficulty

The upper bound $d\le 12$ needs one explicit weight-12 logical together with a proof that it lies outside the opposite row space. The lower bound $d\ge 12$ asks that no nontrivial logical of weight at most 11 exist among roughly $\binom{336}{11}\approx 10^{19}$ candidate supports. Direct enumeration is out of reach. A SAT encoding with a cardinality constraint is several orders of magnitude slower than the source's pruned search, and the resulting proof objects are large: hundreds of megabytes for the larger ladder codes. Kernel-checking such certificates, or finding structure that avoids them, is the central difficulty. Computing $k$ also requires an $\mathbb F_2$-rank of matrices with up to 180 rows and 360 columns, and Mathlib's Matrix.rank is not computable by decide. The envelope statement additionally quantifies over 971 group shapes and every pair of three-term polynomials on each.

Formalization scope

All objects are in the definition file BBCode_Setting. $G$ is ZMod l × ZMod m, and a polynomial is a Finset of monomials, which makes it a set of distinct terms. The circulant has entry 1 at $(g,h)$ iff $h-g\in P$. Qubits are G ⊕ G (left and right blocks). $H_X$ is Matrix.fromCols (circulant A) (circulant B) and $H_Z$ is Matrix.fromCols (circulant B)ᵀ (circulant A)ᵀ, over ZMod 2. The row space is the ZMod 2-span of the rows, and the weight counts nonzero coordinates. NumLogical A B k states $\operatorname{rank}H_X+\operatorname{rank}H_Z+k=n$ additively, avoiding truncated subtraction. HasZDistance A B d requires both a nontrivial Z-logical of weight exactly $d$ and the lower bound for every nontrivial Z-logical, so a code without logicals cannot satisfy it vacuously. IsCode A B n k d bundles $n=2lm$, $k$ and both distances.

The envelope quantifies over all $l,m\ge 1$ with $2lm\le 360$. The source enumerates 961 shapes; the 10 it omits ($lm\le 5$) cannot have $k\ge 20$, so the two ranges are equivalent.

Reusable infrastructure includes computable $\mathbb F_2$ rank certificates (explicit row-echelon or basis witnesses), a verified checker for DRAT or proof-tree certificates, and symmetry lemmas for group translations acting on BB codes. Contributions of any of these, of individual sectors ($d_X$ or $d_Z$ separately), or of upper and lower bounds as separate lemmas are welcome.

Selected references

• S. Bravyi, A. W. Cross, J. M. Gambetta, D. Maslov, P. Rall, T. J. Yoder, High-threshold and low-overhead fault-tolerant quantum memory, Nature 627, 778–782, 2024. https://doi.org/10.1038/s41586-024-07107-7 (arXiv: https://arxiv.org/abs/2308.07915)
• B. W. Daugherty, S. Ryan, G. Ward, New distance-12 bivariate-bicycle codes with 20 and 24 logical qubits: an exhaustive classification and checkable distances to 360 qubits, certificate release v1.0.0, Zenodo, 2026. https://doi.org/10.5281/zenodo.23382175
• D. J. C. MacKay, G. Mitchison, P. L. McFadden, Sparse-graph codes for quantum error correction, IEEE Trans. Inf. Theory 50(10), 2315–2330, 2004. https://arxiv.org/abs/quant-ph/0304161
• A. A. Kovalev, L. P. Pryadko, Quantum Kronecker sum-product low-density parity-check codes with finite rate, Phys. Rev. A 88, 012311, 2013. https://arxiv.org/abs/1212.6703
• J. Cruz-Benito et al., evolutionary search for bivariate-bicycle codes, arXiv:2606.02418, 2026. https://arxiv.org/abs/2606.02418