PSI: uma prova Lean da conjectura Aaronson-Ambainis encontrada por um sistema de IA
A Physical Superintelligence anuncia que um sistema interno de pesquisa, utilizando um modelo não público da Anthropic, encontrou uma prova da conjectura Aaronson-Ambainis (2008), aceita pelo Lean 4. O manuscrito e a formalização são públicos.
A Physical Superintelligence (PSI) anunciou em 6 de novembro de 2026 que um sistema interno de pesquisa, alimentado por instâncias de um modelo não público da Anthropic, encontrou uma prova da conjectura Aaronson-Ambainis, em aberto desde 2008. Segundo o laboratório, o Lean aceitou uma prova completa no terceiro dia de execução, seguida por dois aprimoramentos. O manuscrito e a formalização em Lean 4 são públicos.
O que diz a conjectura
Scott Aaronson e Andris Ambainis questionavam se um computador quântico poderia responder a uma pergunta sim/não sobre uma cadeia aleatória com exponencialmente menos consultas do que um computador clássico. A maior parte das acelerações espetaculares conhecidas (como o algoritmo de Shor) depende de uma estrutura rara na entrada. A conjectura de matemática pura deles, se verdadeira, implica que, na ausência dessa estrutura, a sobrecarga clássica permanece no máximo polinomial em relação ao número de consultas quânticas.
Na prática, após T consultas, a probabilidade de um algoritmo quântico responder “sim” é um polinômio de grau no máximo 2T com valores em [0, 1]. A conjectura afirma que tal polinômio, se variar o suficiente, sempre possui uma variável de influência suficientemente grande — o que permite a um computador clássico imitar a previsão observando apenas poucos bits.
O que a PSI publica
A página de pesquisa e o repositório no GitHub descrevem uma prova que segue um plano de Lovett e Zhang, substituindo uma desigualdade que haviam deixado em aberto. O README afirma quatro teoremas em Lean sem placeholders nem axiomas adicionados, reverificados por duas implementações do núcleo do Lean (versões 4.33.0 / Mathlib v4.33.0, licença Apache 2.0). David Turturean liderou o trabalho; Jim Halverson auditou a prova; Phiala Shanahan comentou a formalização.
Em agosto de 2026, quatro pesquisadores de Stanford (Blanc, Docter, Strassle, Tan) já haviam resolvido um caso particular. A PSI afirma que eles agora estão lendo a prova completa e preparando uma exposição mais curta; o laboratório cita um comentário elogioso da parte deles.
Limites para manter em mente
O repositório deixa a cargo do leitor a verificação de que o enunciado em Lean PrintedConjecture realmente corresponde à conjectura impressa. Um teorema aprimorado baseia-se em uma hipótese de Agarwal e Ben-David não formalizada aqui. O artigo em prosa não é verificado por máquina. O modelo da Anthropic não foi nomeado nem é público: é possível inspecionar o resultado, mas não reproduzir a descoberta. Nenhuma reação pública de Aaronson ou Ambainis havia sido encontrada até o momento da nossa redação.
Nossa leitura
O sinal aqui não é “um modelo inventou a teoria dos números”, mas que um sistema de pesquisa acoplado a um verificador formal hoje consegue produzir um artefato inspecionável sobre um problema em aberto há dezoito anos. A máquina propõe, o Lean resolve parte do trabalho, e o ser humano continua responsável pela correspondência entre o enunciado formalizado e a conjectura original. Enquanto essa fidelidade e a revisão por pares não estiverem resolvidas, a atitude adequada é tratar o repositório como uma candidata a prova verificada por máquina, e não como um teorema já consolidado no cânone.
Fontes
- PSI — A proof of the Aaronson-Ambainis conjecture (6 de novembro de 2026) Fonte primária
- GitHub — physical-superintelligence/aaronson-ambainis (artigo + Lean 4) Fonte primária
- Aaronson & Ambainis — The Need for Structure in Quantum Speedups (arXiv:0911.0996) Fonte primária — Enunciado original da conjectura
Uma fonte primária vem diretamente da empresa, do laboratório ou da organização envolvida. Uma fonte secundária relata a informação sem ser a sua autora: nós a sinalizamos como tal. Encontrou um erro? Consulte nossa política de correções.
