Matemática na era da IA: a leitura de Terence Tao no ICM 2026

A 24 de julho de 2026, Terence Tao, professor na University of California, Los Angeles e medalha Fields, apresentou a conferência “Mathematics in the age of AI” no ICM 2026, em Filadélfia (Pennsylvania Convention Center). Os slides, publicados no seu site oficial, recuperam o contexto histórico da “crise dos fundamentos” (1900‑1930) e propõem uma nova crise — desta vez não sobre os axiomas, mas sobre os valores e as práticas da comunidade matemática. Tao formula uma “Community Response Question” que não é uma questão matemática tradicional, mas metamatemática, política, ética e cultural, mantendo separada a “AI Capability Conjecture” (quão capazes são de facto as ferramentas) da questão dos objetivos e dos valores da disciplina.

Tao observa que os muitos dados invocados a favor ou contra as várias formas da conjetura não foram recolhidos em condições científicas controladas e que a evidência pública arrasta viés de seleção, incentivos não científicos e custos não declarados. A única exceção que cita é o projeto independente First Proof (1stproof.org): o seu segundo lote de dez problemas foi testado em condições controladas a 28 de maio de 2026 contra quatro “harnesses” de IA, com sete dos dez resolvidos com qualidade de publicação por pelo menos uma equipa e com arbitragem de especialistas sobre correção e exposição. Os resultados estão documentados no preprint arXiv 2606.18119 e na página do Center of Mathematical Sciences and Applications de Harvard. Continua a ser uma amostra de dez problemas, não generalizável a toda a investigação matemática; também não está verificado a que sistemas comerciais correspondem os quatro harnesses testados.

Um ponto central da apresentação é a decomposição da produção matemática em cinco etapas: geração, verificação, exposição, publicação e canonização. Segundo Tao, as IA e os assistentes de autoformalização (Rocq, HOL, Lean) já aceleraram as duas primeiras, ao passo que as três últimas continuam dominadas pelo trabalho humano. Tao refere também as provas de IA em erdosproblems.com, onde as soluções não são verificadas por revisores humanos — um sintoma concreto do problema de fiabilidade. Critica ainda a exposição automática, argumentando que o “atrito natural” — as dificuldades com que um autor humano se depara — dá ao leitor sinais úteis, enquanto uma demonstração demasiado polida pela IA pode apagar essas pistas. Nas palavras de Tao, “In short, we will transition from an era of proof scarcity to an era of proof abundance”.

Tao invoca a Leiden Declaration on Artificial Intelligence and Mathematics (2 de junho de 2026) e sugere uma regra prática: se os autores não forem capazes de dar de forma convincente uma exposição clara, de nível especializado, sobre os seus próprios resultados — correta e com as devidas atribuições —, então o resultado não deveria ser publicado. Conclui que a análise da resolução de problemas deveria estender-se ao ensino, à orientação, à contratação e ao financiamento, limitando estritamente o uso da IA na formação. Nota final: o documento público da intervenção são os slides; não existe transcrição oficial do discurso falado.