"Como sabemos se a prova de um teorema está certa?"

[Joao Marcos]

"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)


JM

[Joao Marcos]

"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

[Haniel Barbosa]

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,

--
Haniel Barbosa
https://hanielbarbosa.com/

[Walter Carnielli]

"curiosamente, não há menção a assistentes de demonstração --- ou
mesmo à Teoria das Demonstrações"

Não acho isso nem mesmo muito curioso.

 Marcelo Viana evita dar qualquer protagonismo à lógica,  nem menciona que o LEAN  é construído com teoria dos tipos dependentes, nem que isso  é um assunto basicamente da Lógica.

Não vai se referir à teoria das demonstrações (ou teoria da prova),   e nem reconhecer que um tópico eminentemente lógico poderá ser  muito influente nos fundamentos de toda a  matemática.

( vamos ver o resto das fatias, até agora temos  três. .)

Abs 

Walter 

 ========================
 Walter Carnielli
CLE and Department of Philosophy
University of Campinas –UNICAMP, Brazil

 AI2- Advanced Institute for Artificial Intelligence 

Blog https://waltercarnielli.com/

 

--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@dimap.ufrn.br>
---
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 logica-l+u...@dimap.ufrn.br.
Para ver esta conversa, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjyjqWhum4HEaSU7wSuRjrwkQ3qrV3vfdQJWAxji%2BWh3Q%40mail.gmail.com.