A benchmark you cannot argue with

On 20 August the Ethereum Foundation's formal verification team, working with Yukon and zkSecurity, launched better.codes. The task is stated exactly: raise the proven lower bound for koalaIRS12 — a Reed–Solomon proximity problem formalised in Lean — to 128 bits.

Why this particular number

Hash-based SNARKs are what zkrollups, zkVMs and Ethereum's post-quantum roadmap are being built on, and their security rests on Reed–Solomon proximity gaps. The bound is not an abstraction: it is the gap between what these systems are assumed to guarantee and what has actually been proved about them. The challenge problem comes out of work on correlated agreement and connects to the Proximity Prize and to Arnon, Boneh and Fenzi's results on list decoding.

The design is the interesting part

Solvers point AI agents at a shared verified benchmark, and every submission is checked by the Lean kernel. That removes the usual failure mode of an AI-assisted research competition — nobody has to assess whether a claimed proof is a proof. Either the kernel accepts it or it does not.

Promoted results are credited to the solver and to the model that produced them, and new techniques are upstreamed to the public repository so subsequent attempts start from the improved position. The bound therefore moves in one direction only, and the record of who moved it is machine-attested rather than asserted.

What the post does not say

No prize amount and no deadline. The post states that eligibility, evaluation, awards and payments are governed by separate program terms and may be adjusted as the challenge progresses. Anyone planning to spend compute on this should read those terms first — the technical specification is precise in a way the commercial one deliberately is not.