Prova de IA redefine o que falta verificar em smart contracts

Cerca de 10 mil agentes de IA trabalharam juntos por 88 horas para provar que as equações de Navier-Stokes podem desenvolver uma singularidade. A OpenAI anunciou na terça-feira, 8 de setembro.

O problema estava aberto há 90 anos e integra os sete Prêmios Milênio do Instituto Clay, cada um com recompensa de US$ 1 milhão. A questão era saber se as equações que governam líquidos e gases poderiam produzir velocidades infinitas a partir de condições iniciais suaves. A OpenAI afirma ter demonstrado que a quebra existe. A prova ainda não foi verificada de forma independente pela comunidade matemática, e a organização não reivindica o prêmio.

O mecanismo da singularidade

O mecanismo descrito é um vórtice que se comprime e se estica ao longo de seu eixo, como espaguete. A região central encolhe e a velocidade cresce sem parar. A energia total permanece finita durante todo o processo, do repouso até a singularidade.

O fluido em repouso recebe uma força externa suave e, em tempo finito, desenvolve velocidade sem limites.

O desafio estava em fazer os termos das equações crescerem e se cancelarem com precisão para que o colapso emergisse do fluido, não de uma força externa infinita. A formalização da prova na linguagem Lean consumiu outras 17 horas usando o modelo GPT-6 Astra, e qualquer matemático pode agora checar cada passo da lógica de forma automatizada. A separação entre geração e verificação é o que permite aceitação pela comunidade.

Lean é um assistente de provas que codifica e verifica teoremas mecanicamente, eliminando a interpretação humana da checagem lógica. No ecossistema crypto, serve para verificação formal de contratos inteligentes. A OpenAI usou o GPT-6 Astra para formalizar a prova em 17 horas, separando a geração da verificação lógica. O anúncio veio com disputa de crédito. Os matemáticos Tristan Buckmaster, da NYU, e Levent Alpöge, da Anthropic, publicaram em 7 de setembro provas de blowup para equações relacionadas. Buckmaster diz que a OpenAI tentou remover Alpöge como autor. A OpenAI nega.

O matemático Terence Tao, da UCLA, havia alertado cinco dias antes sobre o risco de sistemas autônomos de IA resolverem problemas mantendo o processo iterativo privado, longe de outros pesquisadores.

Uma caixa-preta bem-sucedida poderia envenenar o problema em vez de iluminá-lo.

O gargalo se move para a especificação

O mesmo raciocínio se aplica aos contratos inteligentes que controlam bilhões de dólares em valor. A documentação do Ethereum descreve a verificação formal como o processo de confirmar se um programa atende às propriedades definidas antes de ir para produção.

Se essas definições forem imprecisas ou incompletas, falhas de segurança podem permanecer ocultas mesmo quando o verificador indica sucesso.

Quem define como o contrato deve se comportar, quem pode sacar, o que acontece quando o saldo muda, quais funções são restritas a determinados perfis, precisa traduzir regras de negócio em propriedades matemáticas antes que o provador inicie a checagem. Qualquer ambiguidade nessa tradução escapa à verificação.

Quando a construção de provas exige menos esforço, a responsabilidade de definir o que será verificado ganha peso. O esforço humano deixa de se concentrar na prova em si e passa para a descrição precisa do comportamento esperado. Em protocolos de DeFi, pontes entre redes e plataformas de ativos tokenizados, auditorias manuais limitam a adoção da verificação formal. Automatizar essa etapa pode ampliar o uso da técnica, mas o trabalho de definir as condições que não podem falhar permanece com especialistas.

Falta saber se métodos que resolvem problemas teóricos de matemática terão utilidade prática no código de produção e se as provas geradas serão compreensíveis para desenvolvedores e auditores. A distância entre resolver um problema centenário e garantir que um contrato de bridge entre blockchains não perde fundos em uma condição de corrida é maior do que a comunidade de pesquisa costuma admitir.

Empresas que combinem provadores automáticos com especificações rigorosas poderão verificar mais contratos antes do deploy. O conhecimento humano, contudo, permanece na linha de frente, traduzindo regras de negócio em especificações que capturem cada falha que não pode acontecer.