The Ethereum Foundation has launched Better Codes, an open autoresearch challenge focused on raising the machine-checked soundness bound of koalaIRS12, a Reed–Solomon proximity problem linked to hash-based SNARKs. Participants may use AI agents, models, prompts and automated testing tools, but submissions must be validated by the Lean 4 kernel. The challenge seeks to narrow the gap between the 128-bit security targeted by production systems and what has been formally proven about the underlying proximity and correlated-agreement conjectures. Winners will share the Ethereum Foundation’s $1 million Proximity Prize pool. The initiative was built by the Ethereum Foundation Formal Verification team with Yukon and zkSecurity; the newer account also identifies Eigen Labs as a joint builder. It is formalized in ArkLib, a Lean 4 library for formally verified arguments of knowledge.