Density of binary LINEAR covering codes: does $f(r)\to\infty$? Is $f(2)=1$? (Ben Green Problem 40)
Statement
Fix $r\ge1$ and let $H(r)\subseteq\mathbb{F}_2^n$ be the Hamming ball of radius $r$ about the origin. Let $f(r)$ be the smallest constant for which there is an infinite sequence of $n$ with LINEAR subspaces $V_n\le\mathbb{F}_2^n$ satisfying $V_n+H(r)=\mathbb{F}_2^n$ (a linear covering code of radius $r$) and $|V_n|=(f(r)+o(1))\,2^n/|H(r)|$ (covering density $\to f(r)$). Does $f(r)\to\infty$ as $r\to\infty$? In particular, is $f(2)=1$?
Acceptance. ADVANCES (the expected product): an explicit family of binary LINEAR radius-2 covering codes with asymptotic density below the current record — a reproducible upper-bound certificate on $f(2)$ (the generator/parity-check family plus a proof that $V_n+H(2)=\mathbb{F}_2^n$) — or a lower bound $f(2)>1$ / $f(r)\to\infty$ with a checkable LP dual. FULLY RESOLVES: determine $f(2)$ exactly (in particular decide $f(2)=1$), or decide whether $f(r)\to\infty$, with proof. Provide the code constructions and a verification script that checks the covering property $V_n+H(r)=\mathbb{F}_2^n$.
Background
Problem 40 of Ben Green's 'Open Problems' manuscript (Dec 2025) — the linear-covering-code density question from the Cohen-Honkala-Litsyn-Lobstein covering-codes monograph. Best-known: $f(1)=1$ (Hamming codes are perfect, density $\to 1$); for radius 2, $1\le f(2)\le 1.4238$ classically, improved to roughly $1.3203$ for the relevant families, with new upper bounds in 2025 (Davydov et al., arXiv:2511.02542); the general upper bound $f(r)\le r^r/r!\sim e^r$; and the NON-linear analogue satisfies $\tilde f(2)=1$. Both 'is $f(2)=1$?' and 'does $f(r)\to\infty$?' are open — a positive answer to the latter would separate linear from non-linear covering density. An attacker needs: (i) explicit algebraic constructions (BCH / Hamming-product parity-check matrices) plus SAT/heuristic search over generator matrices to drive down the achievable radius-2 density — each construction is a checkable upper-bound record on $f(2)$; (ii) an LP / Delsarte-type lower-bound argument to prove $f(2)>1$ (or $f(r)\to\infty$). Formal tooling now exists for certifying $q$-ary covering codes in Lean 4 (arXiv:2606.09600).
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Ben Green, 100 Open Problems (Problem 40) | paper |
| REF-02 | New upper bounds for binary linear covering codes (Davydov et al., 2025) | arxiv |
| REF-03 | Proof-Carrying Certificates for q-ary Covering Codes in Lean 4 (2026) | arxiv |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.