Nous avons formalisé la solidité de FRI dans Lean, en utilisant @HarmonicMath et Claude Code. - analyse de FRI par @nico_mnbl et des collaborateurs - transformée en preuve Lean par @pirapira 🔥

Trivia : cela a commencé par curiosité en réponse à l'annonce de Math, Inc concernant leur preuve FRI, formalisant les preuves succinctes et l'algèbre linéaire : ...ce qui est bien, mais assez éloigné des véritables limites de sécurité FRI que nous pourrions attendre !