O que foi realmente demonstrado
Levent Alpöge e Tristan Buckmaster publicaram três pré-publicações que estabelecem explosão em tempo finito com um termo de forçamento suave para a equação do meio poroso incompressível, o sistema de Boussinesq bidimensional e as equações de Euler incompressíveis a três dimensões.
Terence Tao escreveu sobre os resultados na segunda-feira, notando que os argumentos são “fortemente assistidos por IA” e que o trabalho também foi formalizado em Lean. Atribui o programa subjacente a Diego Córdoba e Luis Martínez-Zoroa, que trataram primeiro o caso do meio poroso.
Explosão significa que as equações produzem uma solução cuja velocidade se torna infinita em tempo finito: uma rutura matemática, não física. Estabelecê-la para Euler com forçamento é um passo rumo à mesma pergunta para Navier-Stokes, que tem associado um Prémio do Milénio do instituto Clay.
A parte da IA
Buckmaster está na Universidade de Nova Iorque. Alpöge é investigador na Anthropic. Segundo a Unite.AI, a dupla revelou ter usado o Claude, da Anthropic, e o Codex, da OpenAI, para a contabilidade de ordens indutivas e constantes, e para refinar iterativamente a redação.
Foram diretos quanto à qualidade da prosa produzida pelos modelos. Buckmaster descreveu o texto inicial gerado por IA como “o mais horrendo que já li”, e os autores classificaram o primeiro rascunho como a pior redação que tinham visto. É a formalização em Lean que traz a certeza: um assistente de prova aceita um argumento ou não aceita.
A disputa
Num comunicado publicado com as pré-publicações, Buckmaster diz que a OpenAI lhe contou que um modelo interno tinha produzido uma prova de cerca de 100 páginas de explosão em tempo finito para as equações de Navier-Stokes forçadas. Descreve duas conversas a 6 de setembro com investigadores da OpenAI, entre eles Sébastien Bubeck.
Buckmaster afirma que a OpenAI propôs ou que os dois grupos publicassem em dias consecutivos, com o resultado de Navier-Stokes da OpenAI a seguir ao seu artigo sobre Euler, ou que ele redigisse sozinho o resultado de Navier-Stokes creditando um modelo interno não identificado da OpenAI, com Alpöge retirado da autoria — ponto que Buckmaster liga ao emprego de Alpöge na Anthropic. Relata que, depois de recusar, lhe perguntaram por que arruinaria a sua carreira. Acrescenta que perguntou se as sessões de Codex da sua equipa tinham sido usadas em treino e que, nas suas palavras, não obteve resposta.
Buckmaster é cauteloso no comunicado: não viu a prova da OpenAI e escreve que não está a acusar ninguém de nada.
Bubeck rejeitou o relato. A OfficeChai noticiou que classificou as afirmações de falsas e inflamatórias, disse que a OpenAI não usou os prompts nem as provas da dupla para instruir os seus próprios modelos, e afirmou ter entrado na conversa seguindo normas académicas. Disse que a OpenAI chegou a Euler de forma independente por métodos diferentes, e que o seu trabalho sobre Navier-Stokes usou uma abordagem semelhante, desenvolvida durante um fim de semana.
O que está e não está resolvido
Os resultados de Alpöge e Buckmaster são públicos e verificados em Lean. A alegação da OpenAI sobre Navier-Stokes não está: até segunda-feira a empresa não tinha publicado o resultado na sua própria página de notícias, e nenhum terceiro inspecionou a prova.
Mesmo que se confirme, a questão do Prémio do Milénio não fica obviamente respondida. A Scientific American noticiou a ressalva do próprio Buckmaster de que parte da comunidade pode dizer que o problema não foi realmente resolvido, porque a versão forçada assenta num termo que a formulação clássica exclui.
O que há a vigiar é estreito e verificável: se a OpenAI divulga a prova e o respetivo certificado Lean para outros verificarem, e se o instituto Clay diz alguma coisa sobre termos de forçamento. Até que o primeiro aconteça, um dos lados desta história publicou o seu trabalho e o outro descreveu-o.
