Independent research · Lean 4
Proximity Prize
How much error can Reed–Solomon codes tolerate?
We study this question with formal proofs and exact computations. The prize conjecture remains open.
The problem, in plain terms
A Reed–Solomon code turns a short message into a longer sequence of symbols. The extra symbols let us recover the message when some values are wrong. With more errors, several messages may fit. List decodingasks how many candidates can remain.
1. Add redundancyFour message symbols become eight encoded symbols.
× marks a changed symbol. Move the slider to add or remove errors.
3. Find the possible messagesKeep every valid codeword at most 2 symbol changes away.
1 possible message
Here the original message is the only candidate.
Exact enumeration of all 17⁴ messages for this eight-symbol code, using arithmetic modulo 17. This illustrates ordinary list decoding; the prize adds interleaving, smooth-domain, and much smaller failure-budget requirements.
What the prize asks
Find the exact error threshold, δ*, for the codes used in these cryptographic checks. One challenge bounds the list of possible interleaved messages. The other, mutual correlated agreement (MCA), asks when agreement in mixtures of words must have a common explanation in the original words.
The target failure budget can be as small as 2⁻¹²⁸. A useful threshold must work for the specified codes and all required inputs, with a proof of its limit.
Rate 1/2: half the encoded symbols carry message information. These are list-decoding benchmarks, not a claimed solution to the prize’s extra conditions.
What we have established
Research snapshot: 6 September 2026
Exact thresholds for two finite codes Lean proofs
We proved both sides of the MCA threshold for two small Reed–Solomon codes: δ* = 1/4. These give exact reference cases for checking general arguments, rather than only upper or lower estimates.
| Code | Failure budget ε* | Exact δ* |
|---|---|---|
| 4 symbols over F₅ · degree < 2 | 2/5 | 1/4 |
| 8 symbols over F₁₇ · degree < 4 | 2/17 ≤ ε* < 7/17 | 1/4 |
These pins use the repository’s supremum definition: the boundary itself is not an allowed radius at these budgets. They are finite results, not a pin at the prize’s 2⁻¹²⁸ budget.
F₅ proofF₁₇ proof and budget range
Stronger bounds on additive collisions Lean proof
We extended a stronger lower bound on equal-sum tuple pairs to every depth r ≥ 3. It strictly improves the earlier adjacent-swap bound for sets with at least two elements, over any finite field. These collision counts are ingredients in character-sum analysis.
The bound and its scope
For a set of N elements, Eᵣ counts pairs of r-tuples with the same sum. We proved Eᵣ ≥ 3Nʳ − 2Nʳ⁻², improving 2Nʳ − Nʳ⁻¹. This is a lower bound on collisions; the production argument still needs an upper bound controlling cancellation.
All-depth theorem and comparison
Interpolation certificates beyond Johnson Exact computation + Lean core
The new approach uses derivatives inside an auxiliary polynomial to constrain possible messages. Our contribution formalizes and quantifies this part of the Brakensiek–Chen–Putterman–Zhang–Zheng approach. The repository contains Lean proofs of the interpolation core at every derivative order, plus exact integer certificates for selected parameters. At rate 1/2, the best registered certificate reaches about 35.50% errors, compared with the 29.29% Johnson benchmark.
| Code rate | Johnson radius | Interpolation radius |
|---|---|---|
| 1/2 | 0.29289 | 0.35498 |
| 1/4 | 0.50000 | 0.57140 |
| 1/8 | 0.64645 | 0.72004 |
| 1/16 | 0.75000 | 0.84377 |
These certificates support the interpolation step. They do not meet the prize’s list-size budget or prove its MCA claim. The rate-1/16 entry is feasible; its exact threshold is not asserted. A full list-decoding conclusion also uses an external theorem and is not yet an end-to-end Lean proof.
Integer certificatesLean coreResearch note
A correction to the strip approach
A Lean refutation shows that the master hypothesis used by the SYZ46 conditional lower bound is false. That lower bound needs a new, satisfiable hypothesis. The separately proved upper bound is unaffected.
What remains open
Have we beaten di Benedetto? Conditional comparison
Not unconditionally. Di Benedetto and coauthors proved a character-sum estimate with leading exponent 2849/2880 ≈ 0.98924. Our proposed recalibration targets 23/24 ≈ 0.95833. Smaller is better, but this still assumes stronger energy bounds and a specialized analytic estimate that we have not proved for the prize fields.
Compare the same quantities
Here H is the subgroup size and p the prime field size. Their Theorem 3.1, for p^(1/4) < H < p^(1/2), gives a bound with powers H^(2689/2880) p^(1/72). The proposed energy substitution targets H^(65/72) p^(1/72). Near the p ≈ H⁴ boundary these correspond to the two leading exponents above. Constants and subpower losses are suppressed; these are not finite numerical guarantees.
The current Lean consumer assumes the specialized analytic estimate, and the finite-field energy transfer remains open. The arithmetic comparison is formalized; a stronger unconditional character-sum theorem is not. Interpolation radii measure something different and do not establish a win over this result.
Di Benedetto et al., Theorem 3.1Our conditional comparison
The production proof
The current production proof needs both a worst-case character-sum bound (the BGK input) and an incidence bound. A character-sum estimate alone is not enough.
The final argument must also reconcile the maximum and supremum definitions of the threshold, prove matching bounds at the sponsor’s parameters, and pass an independent audit with no unproved assumptions.
Contribute
Start with the current research and open pull requests. Choose one precise claim, check it, and report the result with its assumptions and reproduction steps. A verified counterexample is useful too.
To work with a coding agent, give it this instruction: