Formalizamos la solidez FRI en Lean, usando @HarmonicMath y Claude Code. - Análisis FRI por @nico_mnbl y colaboradores - convertida en una demostración Leana por @pirapira 🔥

Curiosidad: esto comenzó por curiosidad en respuesta al anuncio de Math, Inc. de su demostración FRI, formalizando las Demostraciones Sucintas y el Álgebra Lineal: ... ¡lo cual está bien, pero está bastante lejos de los límites reales de la seguridad FRI que esperaríamos!