Les deux versions sont alignées bloc par bloc, dans l’ordre du texte : titre, l’essentiel, puis paragraphe par paragraphe. Quand la traduction a fusionné ou scindé un paragraphe, la case correspondante reste vide — on ne rapproche jamais deux passages au jugé.
At better.codes, a solver signs in with GitHub, clones the challenge repository and works on koalaIRS12, a Reed–Solomon proximity problem. The new Ethereum Foundation challenge asks the solver’s own AI agents to raise its machine-checked soundness bound toward 128 bits.
Sur better.codes, un participant se connecte avec GitHub, clone le dépôt du défi et travaille sur koalaIRS12, un problème de proximité pour les codes de Reed-Solomon. Le nouveau défi de la Fondation Ethereum demande à ses propres agents IA de relever sa borne de solidité vérifiée par machine vers 128 bits.
The problem sits beneath hash-based SNARKs — succinct non-interactive proof systems — used in systems securing zkrollups and zero-knowledge virtual machines, as well as in Ethereum’s post-quantum roadmap. These systems rely on proximity gaps and correlated agreement for Reed–Solomon codes. The foundation says deployed systems target 128-bit security, while the full guarantee still depends on conjectures that researchers are working to prove or disprove.
Le problème se situe sous les SNARK fondés sur le hachage — des systèmes de preuve succincts et non interactifs — utilisés par les systèmes qui sécurisent les zkrollups et les machines virtuelles à connaissance nulle, ainsi que dans la feuille de route post-quantique d’Ethereum. Ces systèmes reposent sur des écarts de proximité et des accords corrélés pour les codes de Reed-Solomon. La fondation indique que les systèmes déployés visent une sécurité de 128 bits, tandis que la garantie complète dépend encore de conjectures que les chercheurs tentent de démontrer ou de réfuter.
The mechanism is deliberately strict. The theorem statement, parameter point and verification harness are pinned; a comparator checks that the exported theorem matches exactly, then the Lean kernel — the formal proof checker — validates the proof. A promoted result is credited to its solver and the AI model used, and its lemmas, techniques or impossibility results are added to the public repository so later participants can build on them rather than repeat the same dead ends.
Le mécanisme est volontairement strict. L’énoncé du théorème, le point de paramètres et le dispositif de vérification sont figés ; un comparateur vérifie que le théorème exporté correspond exactement, puis le noyau Lean — le vérificateur formel de preuves — valide la preuve. Un résultat promu est attribué à son participant et au modèle d’IA utilisé ; ses lemmes, techniques ou résultats d’impossibilité sont ajoutés au dépôt public afin que les participants suivants puissent s’appuyer dessus plutôt que de refaire face aux mêmes impasses.
And concretely? The immediate users are researchers and developers with an AI setup capable of formal mathematics, not people installing a new product. They get a shared benchmark, a public score in bits and a trail of machine-checked work. The intended benefit is cumulative evidence for the security assumptions behind existing proof systems, but the launch covers only koalaIRS12 and does not say that the 128-bit target has been reached.
Et concrètement ? Les utilisateurs concernés sont des chercheurs et des développeurs disposant d’une configuration IA capable de mathématiques formelles, et non des personnes installant un nouveau produit. Ils bénéficient d’une référence commune, d’un score public en bits et d’une trace de travaux vérifiés par machine. Le bénéfice attendu est de fournir des éléments cumulatifs en faveur des hypothèses de sécurité des systèmes de preuve existants, mais le lancement ne couvre que koalaIRS12 et n’affirme pas que l’objectif de 128 bits a été atteint.
The challenge is part of the Ethereum Foundation’s Proximity Prize initiative, developed with Yukon and zkSecurity. The foundation says similar open autoresearch challenges have already advanced work in quantum circuit design, verified zero-knowledge circuits and post-quantum proving speed. Eligibility, evaluation, awards and payments are governed by program terms that may change as the challenge progresses.
Le défi s’inscrit dans l’initiative Proximity Prize de la Fondation Ethereum, développée avec Yukon et zkSecurity. La fondation affirme que des défis similaires de recherche ouverte automatisée ont déjà fait progresser les travaux sur la conception de circuits quantiques, les circuits vérifiés à connaissance nulle et la vitesse de preuve post-quantique. L’éligibilité, l’évaluation, les récompenses et les paiements sont régis par les conditions du programme, qui peuvent évoluer au fil du défi.