{"id":"palomar/PALOMAR-2026-10-15-000014","url":"https://github.com/PranavaKCode/EvenOrderMDS/tree/1e7d9f0fc719de64230edd473411b23e2a8ed72b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000014-v1.json","repo":"https://github.com/PranavaKCode/EvenOrderMDS","tags":["math.CO","cs.IT","msc:94B05","msc:94B65","msc:51E21","msc:51E20","msc:13H10","msc:68V20","coding-theory","mds-codes"],"score":0,"title":"The MDS conjecture over finite fields of even order","trust":"high","domain":"math.CO","source":"palomar","authors":["Pranava Kumar"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 proof of the linear MDS conjecture for every finite field of even order. For a finite field K with an even number q of elements and 2 ≤ k ≤ q, the maximum length of a k-dimensional linear maximum distance separable (MDS) code over K is q + 2 when k = 3 or k = q − 1, and q + 1 otherwise; codes are subspaces of K^N and an MDS code is one whose minimum Hamming distance equals N − k + 1. The upper bound is proved through the correspondence between MDS codes and arcs: after puncturing and duality it suffices to exclude arcs of q + 2 vectors in K^r for 4 ≤ r ≤ q/2 + 1. A hypothetical such…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true}