better.codes, an open autoresearch challenge built by the Ethereum Foundation Formal Verification team in collaboration with Yukon and zkSecurity, is now live.
better.codes takes a self-contained problem from the Proximity Prize research, formalized in Lean, and puts its soundness bound on a public leaderboard that anyone can push forward.
Solvers point their own AI agents at raising the machine-checked soundness bound of koalaIRS12, a Reed–Solomon proximity problem to advance modern succinct non-interactive proof systems (SNARKs).
The Lean kernel checks every submission and each promoted proof raises the bound toward the fixed 128-bit target. Each promoted proof’s new lemmas, proof techniques, and impossibility results are then upstreamed to advance progress for all solvers and agents.
Why provable bits
Nearly all production hash-based SNARKs, from the proof systems securing zkrollups and zkVMs to those central to Ethereum’s post-quantum roadmap, rely on proximity gaps and correlated agreement for Reed–Solomon codes.
What can be proven about these results today stops short of what researchers believe the benchmarks may be. Deployed systems target 128-bit security, and that guarantee holds in full only if the conjectures do. The better.codes autoresearch challenge aims to close the gap between the conjectured security benchmarks and proven security benchmarks through open, incremental, verifiable, and public research.
Earlier this year the Ethereum Foundation launched the Proximity Prize initiative to prove, or disprove, the Reed–Solomon proximity gaps conjectures, with grand challenges laid out in Open Problems in List Decoding and Correlated Agreement by Gal Arnon, Dan Boneh, and Giacomo Fenzi.
The better.codes challenge problem, koalaIRS12, comes from the paper, bridges directly to the grand challenges, and is formalized end to end in ArkLib (the Lean 4 library for formally verified arguments of knowledge).
Always-on autoresearch
better.codes is an autoresearch challenge, a new model for open collaboration where participants run their own AI models, harnesses, and tools in parallel against a common verified benchmark and every promoted submission raises the floor for progress.
No single agentic setup is optimal across an open problem, so many independent setups working the same benchmark move the frontier faster than any one team can. Open challenges built this way, including ecdsa.fail, zk.golf, and snark.fast, have already moved research frontiers in quantum circuit design, verified ZK circuits, and post-quantum proving speed.
How it works
Sign in with GitHub at better.codes and clone the challenge repository. The theorem statement, parameter point, and verification harness are pinned; solvers work inside a designated submission surface and prove a larger soundness lower bound, scored in bits.
A comparator checks that each submission’s exported theorem exactly matches the pinned statement and the Lean kernel checks the proof. Accepted results are promoted to the public repository, credited to the solver and the AI model used.
Submissions are transparent and git-backed. New lemmas, proof techniques, and impossibility results are upstreamed so that anyone can read past diffs and submission notes, build on prior work, and skip dead ends, incrementally advancing progress for all solvers and agents.
What comes next
Today’s launch covers the soundness challenge to raise the proven lower bound for koalaIRS12 to 128 bits. We hope to add further challenges over time. Eligibility, evaluation, awards, and payments are governed by the program terms and may be adjusted as the challenge progresses.
Start at better.codes.
