A OpenAI publicou uma proposta de solução para o problema de existência e regularidade das equações de Navier-Stokes, um dos Millennium Prize Problems do Clay Mathematics Institute. O trabalho foi gerado por um sistema interno de agentes de IA e formalizado inteiramente em Lean, uma linguagem de verificação formal. A tecnológica declarou de imediato que não tenciona reclamar o prémio de um milhão de dólares associado e remeteu a validação final para o escrutínio da comunidade matemática.
A decisão de codificar a totalidade do argumento em Lean muda o patamar da discussão científica em torno da IA generativa. Até agora, a aplicação destes modelos a investigação de ponta esbarrava na fragilidade das alucinações: um texto matemático plausível pode esconder falhas lógicas graves e difíceis de detetar. Ao recorrer a um assistente de prova formal, a OpenAI substitui a persuasão textual pela verificação algorítmica de cada passo dedutivo.
Renunciar ao prémio monetário é também um movimento estratégico pragmático. Ao retirar o incentivo financeiro do centro da conversa, o laboratório reduz o atrito com o meio académico tradicional e coloca a ênfase no método de trabalho, forçando os pares a avaliarem o código em vez de descartarem o anúncio como mero exercício de relações públicas.
Ainda que a comunidade matemática encontre lacunas na tradução das premissas ou na modelação das equações para o ambiente formal, o precedente fica estabelecido para a investigação científica e de engenharia crítica. A combinação entre geração autónoma de hipóteses e verificação computacional rigorosa aponta para uma redução substancial no tempo necessário para auditar teses complexas, transferindo o esforço humano da conferência manual de contas para o desenho e arbitragem de problemas estruturais.