Sistema de pesquisa da PSI com modelo da Anthropic prova a conjectura de Aaronson-Ambainis

A conjectura de Aaronson-Ambainis está aberta desde 2008 e trata de quando computadores quânticos podem ser exponencialmente mais rápidos que os clássicos. Os dois autores mostraram que, se a conjectura for verdadeira, o ganho quântico em entradas aleatórias é no máximo polinomial. A PSI (Physical Superintelligence) diz que um sistema de pesquisa desenvolvido internamente, rodando um modelo não público da Anthropic em infraestrutura própria, produziu a prova. Segundo a PSI, o sistema tinha uma prova completa no terceiro dia da execução, e o Lean, assistente de provas que checa cada passo, a aceitou. Depois o sistema trabalhou em problemas relacionados e melhorou o resultado duas vezes, com o Lean aceitando a versão final.

O enunciado técnico é sobre polinômios limitados de baixo grau. Se o valor de um polinômio f não é constante, algum bit tem influência mínima dada por uma constante c, cerca de 0,0025, segundo o texto. A prova segue o plano de Lovett e Zhang, mas troca uma desigualdade que eles deixaram como conjectura por uma nova, demonstrada no manuscrito. Um grupo de Stanford já havia resolvido em agosto de 2026 o caso especial de rodadas paralelas fixas e agora lê a prova completa. A PSI afirma que David Turturean liderou o trabalho e é responsável pela correção do artigo, e que Jim Halverson auditou a prova.

A cobertura anterior do CEVIU mostra uma sequência de resultados matemáticos atribuídos a IA. Em 8 de setembro de 2026, o CEVIU noticiou "IA da Anthropic Gera Prova do Último Teorema de Fermat, Mas Desafia Adoção Ampla", com prova validada em Lean, mas de 13 milhões de linhas. Em 27 de outubro de 2026, veio "OpenAI afirma que seus modelos refutaram a Exponential Time Hypothesis", também com prova verificada em Lean. A novidade agora é que o resultado atinge um problema central da complexidade quântica e vem de um sistema de pesquisa de terceiros usando modelo da Anthropic. Os itens de 9 de setembro e 20 de outubro de 2026, sobre a OpenAI, são anúncios de outro tipo e não entram na comparação.

Para quem acompanha IA aplicada à pesquisa, o dado relevante é o arranjo: um sistema em torno de um modelo, execução de dias e verificação formal em Lean. Isso é a leitura editorial, não uma conclusão da fonte. O modelo é não público, então ninguém de fora reproduz o experimento. O que dá para checar é a prova e o certificado.