Por 68 anos, matemáticos encaram um problema de uma única frase que se recusava a morrer. Neste mês, uma prova gerada por IA o encerrou — e Terence Tao, após dias de intenso trabalho assistido por IA, transformou a formalização da máquina, de cerca de 90.000 linhas, em um argumento limpo que qualquer um pode acompanhar. No caminho, ele descobriu que a máquina havia, na verdade, provado algo mais forte.
O problema de 68 anos
A conjectura de Sendov, formulada pelo matemático búlgaro Blagovest Sendov em 1958, parece quase simples demais para ser um problema em aberto: tome qualquer polinômio de grau n cujas raízes estejam todas no disco unitário. Para cada raiz a, deve existir um ponto crítico (uma raiz da derivada) a uma distância de no máximo 1 de a.
O teorema de Gauss–Lucas garante que os pontos críticos vivem no envoltório convexo das raízes, então algo próximo sempre existe — mas “a menos de 1 de cada raiz individualmente” é uma exigência muito mais forte. Décadas de trabalho resolveram os casos de grau pequeno (Rubinstein; depois Brown e Xiang estenderam o intervalo) e, em 2020, o próprio Tao provou a conjectura para todos os graus suficientemente grandes. O intervalo intermediário permaneceu intocado.
O que a IA realmente fez
Em 5 de agosto, Lech Mazur usou o ProofAtlas, uma ferramenta de IA para demonstração de teoremas, para produzir uma prova que cobria todos os graus de uma vez — verificada de ponta a ponta no assistente de provas Lean. O problema: a prova da máquina tinha cerca de 90.000 linhas de Lean, praticamente ilegível para humanos, e não estava em forma publicável.
Foi aí que começou a “digestão”. Tao passou vários dias, com forte auxílio de IA (incluindo sessões com o ChatGPT), retrabalhando o argumento: conectando-o à literatura existente, eliminando redundâncias e isolando as ideias principais. O que emergiu é quase constrangedoramente elementar — nada de análise complexa além do teorema fundamental da álgebra, e a desigualdade mais profunda necessária é um caso particular da desigualdade de Maclaurin, derivável da desigualdade AM–HM mais indução.
A digestão produziu duas surpresas. Primeiro, o argumento na verdade prova a versão “interior” da conjectura, que implica tanto a conjectura de Sendov quanto o fortalecimento mais forte de Phelps–Rodriguez — um resultado mais forte que ninguém havia notado estar escondido no trabalho da máquina. Segundo, Tao re-formalizou toda a prova em Lean com um agente de IA em cerca de 15.000 linhas, seis vezes menor que a original da máquina.
Por que a máquina venceu onde os humanos travaram
As quatro “identidades de comunicação” que sustentam a prova (centroide, polar e duas identidades de origem) estavam todas escondidas em pedaços do argumento da IA. A máquina as encontrou por pura busca; os humanos nunca combinaram essas peças porque 68 anos de trabalhos anteriores elegantes criam um campo gravitacional em torno das abordagens esperadas. As máquinas não carregam essa bagagem — elas não precisam que a prova seja bela, apenas que exista.
O que isso significa para a IA e para a matemática
Esta é a demonstração mais limpa até agora do pipeline que Tao vem descrevendo: geração → verificação → exposição → publicação → canonização. A IA agora cuida da geração e da verificação (o Lean confere o trabalho); os humanos cuidam da exposição e da canonização — transformar uma prova verificada, mas ilegível, em algo que uma comunidade possa ensinar, desenvolver e absorver nos livros didáticos. O gargalo mudou de lugar: encontrar provas está se tornando abundante; digeri-las é a habilidade escassa.
Para a indústria de IA, o sinal é maior do que um único teorema. Uma ferramenta de IA resolveu um problema em aberto de 68 anos na matemática pura, e o matemático mais forte vivo passou dias interagindo com o resultado da máquina como um colaborador — não uma calculadora. O padrão espelha o que está acontecendo com agentes de programação: gerar amplamente, verificar rigorosamente, curar com cuidado. Agentes de pesquisa de IA como o Polaris já estão industrializando esse fluxo de trabalho gerar-verificar-digerir para a ciência.
O que você pode fazer a respeito
- Invista em verificação, não apenas em geração. O Lean e ferramentas semelhantes são o que transforma modelos não confiáveis em úteis.
- Trate o resultado da IA como matéria-prima. A prova de 90.000 linhas era inutilizável; a versão de 15.000 linhas de Tao é o artefato de verdade.
- Digerir em público. O relato de Tao e os logs de chat são um modelo para transformar descobertas da máquina em conhecimento da comunidade.
- Observe o pipeline. Equipes que dominarem gerar–verificar–digerir produzirão resultados de pesquisa, não apenas rascunhos.
