MDS conjecture settled in even characteristic
Two independent proofs, one checked in Lean with Claude’s help, the other written with ChatGPT
Event confirmedAwaiting review
Importance: major (4 of 5)The takeaway
Two independent claims settle the linear MDS conjecture (from Segre’s 1955 question on arcs) for every finite field of even order: an [n, k] MDS code over F_q, q even, has n ≤ q + 1, except n ≤ q + 2 for k = 3 and k = q − 1.
Status
- Claim
Event confirmedAwaiting review
- Our reporting
- High confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 21 October 2026
Your AI and this story
- GPT-6 Astra173 days after its cutoff
- Claude Opus 5.5112 days after its cutoff
- Gemini 4 Argon203 days after its cutoff
- Grok 4.7142 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 112 days before it.
Key facts
- Statement (Chen–Huang, arXiv 2610.28208): ‘every nontrivial linear [n, k] maximum distance separable (MDS) code over a finite field Fq of characteristic two satisfies n ≤ q + 1, except in dimensions k = 3 and k = q − 1, where n ≤ q + 2. This resolves the linear MDS conjecture in even characteristic.’
- History: Segre’s 1955 problems on arcs in finite projective spaces; Ball (JEMS 2012) proved the conjecture for k ≤ p, settling prime fields; odd characteristic remains open in general
- Chen–Huang AI statement: ‘The authors used ChatGPT to assist with exploring proof strategies, checking intermediate calculations, and editing the exposition. The authors are responsible for all mathematical arguments and for the final exposition.’
- Kumar’s Lean proof: Palomar record PALOMAR-
2026-10-15-000014(registered 15 Oct 2026, trust level ‘high’), theorem EvenOrderMDS.maximum_length_of_MDS_code over Mathlib, standard axioms only, checked by Comparator against Challenge.lean and by the Lean kernel plus the NanoDa and con-ron kernels - Kumar repo authorship note: ‘The mathematical argument was devised by Pranava Kumar … Claude (Anthropic) assisted him in translating the proof into Lean 4’ and ‘The present repository was assembled with the help of an AI agent (Claude Opus 5.5, in Claude Code)’, which wrote Challenge.lean and Solution.lean; ‘No independent human expert has yet reviewed the mathematics.’
- Chen–Huang note the overlap: Kumar’s report ‘also claims to establish Theorem 1.1’; both use a Frobenius obstruction, a ternary colon ideal and Gorenstein Hilbert-function unimodality, with different local constructions
What happened
The MDS conjecture asks how long a maximum distance separable code (one that meets the Singleton bound) can be. Equivalently, it asks for the largest arc in a finite projective space, a question Beniamino Segre posed in 1955. The expected answer is q + 1, with exceptions in even characteristic. Simeon Ball proved it over prime fields in 2012.
On 15 Oct 2026 Pranava Kumar registered a Lean 4 proof of the full even-characteristic case on Palomar, the registry of Lean-verified mathematics. The repository’s README says the argument is Kumar’s: Claude helped him translate it into Lean, and Claude Opus 5.5 in Claude Code later ported it, wrote the Challenge and Solution files, the README and the report. It also says that no independent human expert has yet reviewed the mathematics. Palomar lists the record with trust level “high”.
On 20 Oct Bocong Chen (South China University of Technology) and Jing Huang (Guangzhou University) posted a 33-page proof on arXiv. Their AI statement says ChatGPT helped explore proof strategies, check intermediate calculations and edit the text. They cite Kumar’s report as an independent claim and compare the two arguments.
No expert reaction or press coverage was found on 21 Oct.
Why it matters
If it holds, this is the biggest advance on the conjecture since Ball’s prime-field theorem. It is also an early case of a major classical result arriving with a kernel-checked Lean proof from the start, built with an AI coding agent. Two caveats remain. The Lean statement was written by the AI agent; it was audited against the standard formulations but uses its own definitions of minimum distance and MDS, not Mathlib’s. And neither proof has been refereed yet.
What is disputed or not yet verified
| Verification | Lean 4 proof (Mathlib, Comparator, three kernels) registered on Palomar; the Challenge statement adds two definitions (HasMinimumDistance, IsMDS) and was written by the AI agent; arXiv preprint unrefereed |
|---|
Sources
3 sources from 3 sites. Numbers match the chips in the text.
3 sources: 3 primary
Primary
- arXiv 2610.28208: On the MDS conjecture in even characteristic (Chen, Huang)arxiv.org, paper
- Palomar registry API: PALOMAR-2026-10-15-000014 (Kumar)data.palomar-registry.org, docs
- GitHub: PranavaKCode/EvenOrderMDS (Lean 4 proof)github.com, code
Changes
- Filed (PDF, Palomar record and repository README read)