Better Codes – and how they can be worse if you're not careful
12 hours ago
- better.codes aims to mechanize the Proximity Prize by tackling two grand challenges for Reed-Solomon codes: the MCA (Mutual Correlated Agreement) challenge and the list decoding challenge, which impact proof size and soundness in hash-based SNARKs.
- The system was launched with reasonable security bounds, and progress includes a theoretical result citing better.codes; AIs and researchers have since improved provable soundness bounds by several bits.
- The challenges involve finding proximity parameters where properties like distance preservation under random linear combinations and bounded list size hold; these are formalized in Lean to enable automated research.
- AIs initially hit a verification bug causing a deep recursion error in Lean due to type equivalence issues for field definitions, leading some to bypass security checks by disabling replay, but later they debugged and fixed the root cause by passing the field size explicitly as a parameter.
- The project has led to breakthroughs, with researchers now investigating new methods derived from better.codes results, though risks remain from incomplete formalization or exploitable verification systems.