Em maio, chegou aos ouvidos do medalhista Fields Timothy Gowers a notícia de que uma IA havia resolvido a conjectura da distância unitária de Erdős — um problema aberto em geometria por quase 80 anos. Sua primeira reação: se fosse verdade, os matemáticos poderiam em breve estar sem emprego. Ele passou a noite recalibrando sua visão de mundo. Na manhã seguinte, chegou um e-mail esclarecedor: a IA não havia provado a conjectura. Ela a havia refutado. Gowers sentiu alívio. Por que uma refutação é mais reconfortante do que uma prova? Em 12 de agosto, seu post no blog respondeu a essa pergunta.
O rumor de maio que quase acabou com a matemática
O contexto: em 1º de agosto, a OpenAI anunciou dez resultados em matemática e ciência da computação teórica, todos produzidos por um modelo interno não lançado chamado Astra. Segundo a narrativa oficial, cada resultado resolve um problema em aberto há muito tempo ou faz progresso substancial em um deles. O desenvolvedor Simon Willison comparou o clima entre os matemáticos online a um “momento Deep Blue” coletivo, e o matemático Kirwin Hampshire já havia publicado um texto intitulado A Noite Escura da Matemática, descrevendo uma genuína crise de confiança. Gowers admitiu que os dez resultados são extraordinários — e então fez uma pergunta mais afiada: se os modelos de grande escala fossem mais fortes que qualquer humano em todos os ramos da matemática, sua vantagem de velocidade deveria fazer os resultados jorrarem como uma enchente. Por que não há enchente?
Dez resultados do Astra — a maioria deles demolições
Olhando para os resultados principais, um padrão aparece. No problema da distância unitária de Erdős, a IA não estendeu o limite de crescimento conhecido há décadas; ela importou ferramentas da teoria algébrica dos números para a geometria discreta, construiu famílias de conjuntos de pontos sobre corpos de números complexos e mostrou que pares a distância unitária podem crescer mais rápido do que a área acreditava possível há muito tempo — um contraexemplo a uma estimativa amplamente aceita. Na conjectura jacobiana, o matemático Levent Alpöge, trabalhando com o Claude, encontrou um contraexemplo a uma questão relacionada. Nos grupos soficos, o avanço foi construir o primeiro grupo não sofico. Nos números de Ramsey multicoloridos, o movimento central foi, novamente, construir objetos combinatórios altamente específicos.
Os quatro problemas se comprimem em uma única pergunta amigável a máquinas: “Existe tal coisa?” Quando a resposta é sim, o repertório do modelo — busca massiva, transferência de ferramentas entre domínios, recombinação de truques conhecidos, tentativas repetidas de construção — assume o comando por completo. E é barato: o gasto total de tokens na caça a contraexemplos em todos os dez resultados ficou na ordem de alguns milhares de dólares a preços de API.
Por que “contraexemplo” e “teorema” não são duas habilidades diferentes
A intuição dos matemáticos trata a busca por contraexemplos como trabalho de sorte — basta um furo e a proposição desaba — e a prova de teoremas como um ofício difícil: nenhuma exceção é permitida, além de um lampejo de inspiração. Gowers argumenta que essa fronteira não se sustenta. Considere dois resultados clássicos: o teorema de Vinogradov de 1937, segundo o qual todo inteiro suficientemente grande é soma de três primos, e o resultado de Gluskin de 1981, segundo o qual em qualquer dimensão existem dois espaços cujas formas estão extremamente distantes entre si. Escritos em linguagem formal, seus esqueletos são quase idênticos — mas ninguém chama o trabalho de Vinogradov de contraexemplo, e ninguém chama o de Gluskin de teorema. A diferença é apenas onde recai o passo difícil.
Há uma camada mais sutil: a palavra “contraexemplo” carrega psicologia. Ela só conta quando derruba uma proposição que as pessoas tinham motivo para acreditar. O grupo não sofico é, portanto, melhor descrito como o primeiro exemplo — poucos especialistas realmente acreditavam que todos os grupos são soficos. E o resultado sobre Ramsey multicolorido, observa Gowers, é para ele pessoalmente um exemplo esperado: ele estudou uma forma equivalente quando era jovem matemático, e a direção que se provou correta foi exatamente aquela em que ele trabalhava. A fronteira acompanha a pessoa, não a matemática.
Oito maneiras de encontrar exemplos; a IA é forte em quatro
Gowers lista oito maneiras padrão pelas quais matemáticos encontram exemplos: percorrer os exemplos padrão em estoque; montar a partir de objetos básicos; deixar lacunas e preencher as condições depois; provar que tal objeto não pode existir; revisar iterativamente um palpite anterior; construir peça por peça sob restrições; escolher um ao acaso; tomar um exemplo suficientemente geral.
Seu julgamento: os modelos serão muito fortes em quatro delas — exemplos de estoque, montagem passo a passo, escolhas aleatórias e exemplos gerais. Elas compartilham três propriedades: rotinas maduras, instâncias densas nos dados de treinamento e baixo custo de falha. As demais abordagens exigem outra coisa: julgar repetidamente, no meio do caminho, se a estrada atual ainda vale a pena. Isso é poda — o ato de cortar a maioria dos ramos de uma árvore de busca assim que ela começa a se bifurcar. Os modelos conhecem quase todos os argumentos padrão e podem falhar milhares de vezes antes de chegar a uma solução, então quanto mais “sorte” exige um problema, mais a IA domina. O terreno que os humanos ainda mantêm é onde a árvore de busca é larga e profunda.
Por que a IA não tem o faro do matemático
Por que os modelos ainda não sabem podar? Três razões. Primeira, os dados de treinamento não contêm tal curso: provas publicadas são produtos finais e limpos — os becos sem saída, os momentos de dúvida, as viradas foram apagados, então os modelos veem conclusões, mas não processos. Segunda, a velocidade é em si o obstáculo: os humanos precisam podar porque uma vida só permite alguns caminhos, enquanto os modelos podem se dar ao luxo de uma busca ineficiente o suficiente para esmagar um humano — e sem escassez, não há pressão para podar. Terceira, a questão é quase impossível de experimentar.
Terence Tao, em sua palestra no ICM 2026, “Matemática na Era da IA”, descreveu o sintoma pelo lado do leitor: provas geradas por IA são dolorosas porque a ênfase está fora de lugar — três páginas sobre um lema óbvio, três linhas sobre o passo genuinamente interessante. Provas humanas deixam o que ele chama de atrito natural nos pontos difíceis; provas polidas por IA o alisam. Seu próprio exemplo: como estudante de doutorado, ele lutou com o artigo de Bourgain de 1991 — nota na margem “eu odeio Jean Bourgain” incluída — e a luta o treinou a acompanhar o raciocínio do autor. Se aquela prova tivesse passado por várias camadas de polimento de IA, ele duvida que teria recebido esse treinamento. “Qual passo é difícil” nunca foi registrado formalmente na tradição matemática, então os modelos não podem aprendê-lo — e suas saídas polidas apagam os últimos vestígios restantes. O resultado é um ciclo errado: os modelos não aprendem julgamento, e suas escritas tornam mais difícil que a próxima geração de modelos aprenda.
A prescrição de Gowers mira a função de recompensa: penalize vagar por becos sem saída demais, e penalize puxar respostas prontas da literatura. Recompense apenas resultados, e você obtém resultados sem processo. Isso vale para o treinamento — e, ele observa, para a própria comunidade matemática.
O teste do cap-set — e o que isso significa para o seu fluxo de trabalho
Gowers oferece a régua mais rigorosa disponível. O avanço do cap-set em 2016: uma nova solução que deixou o limite anterior para trás por uma larga margem, usando uma abordagem que nenhuma das expectativas da área havia previsto — e que, em retrospecto, era obviamente certa. Uma onda de pesquisadores abandonou imediatamente seus próprios trabalhos para explorar o que a nova técnica poderia fazer. Um método genuinamente grande não resolve apenas um problema; ele muda, da noite para o dia, no que uma comunidade trabalha. Somente quando um modelo produzir algo desse peso Gowers considerará o limiar cruzado. Ele espera que os modelos continuem melhorando rápido — possivelmente desenvolvendo um faro mais forte em um ou dois anos. A vantagem humana é alugada, não própria.
Enquanto isso, use os modelos como Gowers faz: como uma máquina barata de contraexemplos. Antes de se comprometer com uma suposição, uma estimativa ou uma restrição de design, deixe um modelo tentar quebrá-la — toda a campanha dos dez resultados custou alguns milhares de dólares em tokens. Mas trate seus esboços de prova confiantes como propostas a serem podadas, não como resultados; e quando um modelo diz “não pude responder à sua pergunta, mas a reduzi a uma mais estreita” cinco vezes seguidas, ele não está convergindo — está descrevendo seu estado de perdido de forma cada vez mais elegante. No mesmo espírito dos artigos do COLM que questionam os padrões dos Transformers, o valor mais profundo da IA na matemática neste momento pode estar menos em novos teoremas e mais em novas perguntas — e em derrubar aquelas em que todos acreditavam.
