A brave new world. Agora (faz nem 6 meses que tivemos esse salto) que agentes dedicados como esse da Math, Inc ou da Harmonic, ou de propósito geral como o Claude Code etc, são plenamente capazes de gerar de maneira escalável mecanizações em assistentes de demonstração, se torna incontornável pensar como melhor lidar com, e como melhor usar, essas ferramentas.
O Larry Paulson deu uma palestra interessante algumas semanas atrás sobre como vem usando Claude junto com Isabelle na AWS: https://www.youtube.com/watch?v=-Eewz-DJovU Nela ele fala sobre um problema que vem emergindo com o uso de agentes pra mecanizações, que é as demonstrações terem pouca qualidade em termos de coisas que buscamos em demonstrações além de ela só existir, como o seu nível de generalidade, legibilidade etc. Nesse mesmo evento o Kevin Buzzard também falou sobre isso quando descreveu seu projeto de mecanizar Fermat's Last Theorem em Lean, algo que a Math, Inc disse (ameaçou?) que ia tentar fazer também. Não sei se tem vídeo, mas aqui os slides: https://aitpm.github.io/slides/Buzzard.pdf E o Jeremy Avigad comentou nesse ensaio, voltado pra matemáticos, sobre a revolução que está acontecendo e como devemos tentar navegá-la: https://arxiv.org/abs/2603.03684 Abraço, Joao Marcos <[email protected]> writes: > "Lean, novo tira-teima da matemática" > --- por Marcelo Viana > https://www1.folha.uol.com.br/colunas/marceloviana/2026/04/lean-novo-tira-teima-da-matematica.shtml > > O resultado anunciado pela Math Inc. (companhia "dedicated to verified > superintelligence via autoformalization") sobre o "Teorema dos Números > Primos", usando IA, está aqui: > https://math-inc.github.io/strongpnt/ > > (OBS: o termo "veracidade da prova" é tão ruim, tão ruim, que a gente > fica sem saber até o que dizer...) > > JM > > > On Wed, Apr 8, 2026 at 3:08 PM Joao Marcos <[email protected]> wrote: >> >> "Como sabemos se a prova de um teorema está certa?" >> --- por Marcelo Viana >> https://www1.folha.uol.com.br/colunas/marceloviana/2026/04/como-sabemos-se-a-prova-de-um-teorema-esta-certa.shtml >> >> (curiosamente, não há menção a assistentes de demonstração --- ou >> mesmo à Teoria das Demonstrações) -- Haniel Barbosa https://hanielbarbosa.com/ -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <[email protected]> --- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para ver esta conversa, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/877bpznn85.fsf%40gmail.com.
