Terence Tao apresenta no Caltech a palestra «Matemática 2.0» sobre provas assistidas por máquina

Terence Tao publicou a gravação da palestra «Math 2.0» («Matemática 2.0»), dada no Instituto de Tecnologia da Califórnia (Caltech). Ele começou a preparar a apresentação há mais de um ano e, na época, a chamava de «Machine Assisted Proof», ou «Prova Assistida por Máquina». A palestra estava prevista para maio, mas foi adiada para outubro. O motivo, segundo Tao, foi uma série de acontecimentos recentes. Quais foram, o trecho disponível do material não diz. O veículo chinês Jiqizhixin colocou no título a ideia central: o tempo em que faltavam provas está chegando ao fim.

O que se sabe sobre a palestra

A própria mudança de título é reveladora. Um ano atrás, o tema soava instrumental: o computador ajuda a verificar e a encontrar provas. No outono de 2026, o autor escolheu a formulação «Matemática 2.0», ou seja, o assunto passou a ser a mudança da própria prática. Tao não explica isso em uma frase; ele remete a uma cadeia de eventos dos últimos meses. O texto completo e os slides é melhor consultar na fonte original, porque o resumo se interrompe justamente onde começa a parte de conteúdo.

Principais dados do trecho disponível:

• formato: palestra pública no Caltech, gravação publicada em 11 de outubro de 2026;
• título de trabalho durante o planejamento: «Machine Assisted Proof»;
• título final: «Math 2.0»;
• prazo: inicialmente maio de 2026, na prática outubro;
• tempo de preparação: mais de um ano.

De onde vem a tese do fim da escassez

A ideia de que provas deixam de ser um bem raro não surgiu do nada. Nos últimos anos, Tao atua publicamente na interseção entre matemática e máquinas. No fim de 2023, ele liderou a formalização, no sistema Lean, da prova da conjectura PFR (conjectura polinomial de Freiman–Ruzsa).

O projeto reuniu uma equipe distribuída e levou algumas semanas. Em 2024, o modelo AlphaProof, do Google DeepMind, resolveu problemas da Olimpíada Internacional de Matemática em nível de medalha de prata. Em 2025, Tao participou dos testes do AlphaEvolve em dezenas de problemas abertos de análise e combinatória.

Esse é o contexto anterior, e não o conteúdo da nova palestra, mas ele mostra a trajetória: primeiro a verificação de provas passa para a máquina, depois parte da busca também passa.

Na matemática clássica, a raridade da prova definia tudo. Um teorema era considerado valioso em parte porque exigia anos de trabalho humano, e a verificação por um revisor também custava tempo. Se gerar e verificar provas fica mais barato, a economia da disciplina muda. O valor se desloca da prova em si para a formulação de perguntas, a escolha de direções e a compreensão de para que serve um resultado.

Onde fica o limite

O título do Jiqizhixin é duro, e Tao costuma fazer mais ressalvas. A formalização em Lean exige um trabalho enorme, e os modelos de linguagem podem errar com toda a confiança. A busca automática funciona bem onde o resultado pode ser verificado de forma mecânica. Por isso, é razoável esperar que «Matemática 2.0» descreva uma nova divisão do trabalho, e não a substituição dos matemáticos. Mas isso é uma suposição, não um resumo da palestra: no texto disponível, essa conclusão não aparece.

Como usar isso na prática

Para pesquisadores e engenheiros que acompanham o tema, três passos são úteis. Primeiro, assistir à gravação completa da palestra e usá-la para conferir qualquer resumo de terceiros, inclusive este. Segundo, aprender Lean e a biblioteca Mathlib: é nessa infraestrutura que se apoiam os projetos mencionados por Tao. Terceiro, para equipes que desenvolvem IA para ciência, a referência é a verificabilidade. Modelos cujas saídas podem ser checadas automaticamente levam vantagem clara sobre os que apenas geram texto plausível.

Por enquanto, a palestra está publicada e sua tese central segue em leitura e debate. Se Tao estiver certo, os próximos anos mostrarão isso por uma mudança no que revistas e conferências consideram um resultado digno de publicação.