Trabalho incrível do @pirapira apresentando uma prova Lean do nosso recente artigo sobre segurança FRI Fluxo de trabalho super interessante também, combinando LLMs TeX-para-Lean com agentes de codificação regulares. Acho que veremos muito mais disso no futuro!