Uma IA resolveu um problema em aberto há décadas, dos que valem um milhão de dólares. A semana seguinte foi mais interessante do que a resolução: matemáticos acusaram a empresa de ter beneficiado de trabalho que não era dela, mais de mil pessoas assinaram uma declaração contra a forma como os laboratórios usam a matemática, e o instituto que atribui o prémio limitou-se a dizer que o processo é lento de propósito. A parte mais sólida da história é, provavelmente, a que quase ninguém está a discutir.

O anúncio, a 8 de setembro

A OpenAI publicou a resolução do problema de existência e suavidade das equações de Navier-Stokes, um dos sete problemas do milénio do Clay Mathematics Institute, com um prémio de um milhão de dólares desde 2000. Quem o resolveu foi um modelo que a empresa não lançou. Segundo a análise publicada hoje pelo forgeeks.net, o resultado foi produzido com cerca de dez mil agentes autónomos e um custo de inferência na ordem dos quinze milhões de dólares, e vem acompanhado de uma formalização em Lean 4 — a linguagem em que uma máquina verifica a prova.

A resolução não está verificada de forma independente, e é isso que o prémio exige. Só no dia 11 de setembro é que o Clay se pronunciou, e fê-lo em duas frases: as regras descrevem o processo de avaliar o que foi alcançado e de atribuir o crédito; «o processo é deliberadamente sem pressa, mas daremos atualizações». Traduzido: o problema continua formalmente aberto.

A acusação que ficou sem resposta

Uma semana antes, Tristan Buckmaster, professor de matemática na Universidade de Nova Iorque, trabalhava no mesmo problema há quase um ano com Levent Alpöge — matemático que trabalha na Anthropic. Usaram Claude e Codex, sobretudo o GPT-5.6 Sol. A 15 de agosto tiveram o avanço. Depois ouviram dizer que a OpenAI tinha resolvido «um problema aberto importante», procuraram perceber o que se passava e descobriram uma equipa a trabalhar num problema relacionado, com uma abordagem parecida. O relato é do próprio Buckmaster, num documento publicado à pressa, e é resumido pelo programador Simon Willison.

Buckmaster perguntou quando tinha sido enviado o primeiro pedido àquele modelo. Não obteve resposta direta durante algum tempo; acabou por lhe ser dito que fora nos dias anteriores, depois de a informação sobre o seu trabalho chegar à empresa. Perguntou se o modelo tinha sido treinado com as sessões do Codex onde ele e Alpöge guardavam todos os rascunhos do projeto. Foi-lhe dito que «o modelo não consulta dados de utilizadores». Voltou a perguntar, agora sobre treino, e não teve resposta. A empresa ofereceu-se para esperar pela publicação dele, ou para o deixar assinar um artigo sobre o resultado — mas disse que Alpöge não seria convidado como coautor, por causa da relação de concorrência com a sua entidade patronal.

A 10 de setembro chegou uma segunda acusação, esta do matemático Andreas Thom, que falou em comportamento não ético e «desonesto» e em falta de transparência sobre a origem dos dados de treino, noticia o The Verge.

Porque importa: disputas de prioridade são antigas na matemática, e há quem as resolva em revistas durante anos. O que é novo é a pergunta que ninguém conseguiu responder com clareza: um modelo terá sido treinado com o rascunho de alguém que estava a resolver o mesmo problema?

A parte de que ninguém fala

Enquanto a polémica corria, o matemático e programador John D. Cook reparou no que faltava na conversa: a OpenAI publicou, ao mesmo tempo que a prova legível por humanos, uma prova formal em Lean 4 — e a verificação do artigo de 166 páginas levou 17 horas.

Para medir o que isso significa, Cook vai buscar uma estimativa de 2005, de Henk Barendregt e Freek Wiedijk: formalizar uma página de um manual de licenciatura levava cerca de uma semana de trabalho humano, quarenta horas. Contando que um artigo de investigação é vinte vezes mais denso, as 166 páginas da OpenAI dariam cerca de 132.800 horas de trabalho. Cook hesita em usar a palavra «revolucionário», mas baixar o custo de uma coisa em quatro ordens de grandeza, diz ele, é isso mesmo.

Porque importa: a verificação formal não é o mesmo que aceitação matemática — uma prova pode compilar e continuar a ser discutida. Mas muda radicalmente o que passa a ser barato verificar, e isso aplica-se a muito mais do que à matemática.

Mil pessoas assinam uma declaração

A 11 de setembro apareceu uma declaração intitulada «Um desalinhamento severo da IA na matemática», aberta a assinaturas. O argumento não é contra a IA. É este: as capacidades matemáticas dos modelos melhoraram de forma acentuada, ao ponto de resolverem problemas em aberto, mas usar problemas famosos como benchmark é prejudicial para a ciência e para a comunidade. Os objetivos das empresas e os da comunidade matemática, dizem os signatários, estão severamente desalinhados — e veem nisso uma versão particular de um problema mais vasto, que atinge outras ciências, profissões criativas e a sociedade em geral.

O texto descreve como a matemática funciona por dentro: problemas famosos servem de faróis para medir a compreensão de uma área, mas o que transforma um resultado em conhecimento é o processo longo e difícil que vem depois — palestras, discussões, simplificações — até haver uma apresentação que qualquer estudante consiga ler. Um resultado que salta esse processo não é conhecimento partilhado; é um ficheiro. No Hacker News, o debate foi o mais intenso do dia: mais de mil pontos e quase mil comentários.

E, na mesma semana, os laboratórios a falar de abrandar

Na quinta-feira, a Bloomberg noticiou que Sam Altman disse aos funcionários da OpenAI que a empresa está aberta a abrandar o desenvolvimento de IA de ponta; a Reuters reproduziu a notícia no dia seguinte. É uma frase curiosa numa semana em que o debate público foi sobre uma empresa a correr mais depressa do que a comunidade científica que avalia o que ela produz. No mesmo dia, o The New York Times publicou dois artigos sobre o outro lado da mesma questão: as discussões internas nos laboratórios sobre um cenário catastrófico, e a dificuldade de as empresas controlarem sistemas que se desenvolvem mais depressa do que os mecanismos criados para os vigiar.

Fontes

• OpenAI, «On the Navier–Stokes Millennium Prize Problem» (8 de setembro de 2026) — openai.com
• Simon Willison, «Some thoughts on the Navier–Stokes Millennium Prize Problem» (8 de setembro) — simonwillison.net
• Clay Mathematics Institute, «Navier-Stokes Announcement» (11 de setembro) — claymath.org
• Declaração «A Severe Misalignment of AI in Mathematics» (11 de setembro) — mathandai.org
• The Verge, «Mathematicians want proof OpenAI didn’t use their work» (10 de setembro) — theverge.com
• John D. Cook, «The part of Navier-Stokes no one is talking about» (9 de setembro) — johndcook.com
• for(geeks), «OpenAI’s Navier-Stokes claim splits the math community» (12 de setembro) — forgeeks.net
• Reuters, «Altman tells staff OpenAI is open to slowing AI development» (11 de setembro), a partir da Bloomberg — reuters.com
• The New York Times, «Inside the Discussions at AI Companies Over a Superintelligence Doomsday» e «Why It’s Difficult for Tech Companies to Rein In A.I.» (12 de setembro) — nytimes.com
• Discussão no Hacker News (1033 pontos, 986 comentários) — news.ycombinator.com

Nota de método: as datas acima foram confirmadas pela submissão original de cada ligação ao Hacker News. Quando uma afirmação depende de uma única fonte, isso está dito no texto. A resolução continua, à data de hoje, por verificar de forma independente.