PSI relata prova da conjectura de Aaronson-Ambainis verificada por máquina

A Physical Superintelligence anunciou, em 6 de novembro de 2026, que um sistema interno de pesquisa, executado com instâncias de um modelo não público da Anthropic, havia encontrado uma prova da conjectura de Aaronson-Ambainis, um problema de computação quântica em aberto desde 2008.

O sistema produziu uma prova completa no terceiro dia de uma execução na própria infraestrutura da PSI, e o assistente de provas Lean a aceitou. Em seguida, a PSI atribuiu ao sistema problemas em aberto relacionados, e ele aprimorou o resultado duas vezes antes de o Lean aceitar a versão final. O manuscrito e a formalização em Lean 4 são públicos.

O que a conjectura diz sobre acelerações quânticas

A questão é saber em que situações os computadores quânticos podem ser exponencialmente mais rápidos do que as máquinas clássicas. O algoritmo de fatoração de Shor, de 1994, depende de uma estrutura: sua entrada contém um padrão repetitivo que o algoritmo pode explorar. O resultado da PSI aborda o caso oposto, de entradas aleatórias ou sem estrutura, nas quais geralmente não há esse padrão.

No modelo de consultas, um algoritmo clássico lê um bit por consulta, enquanto uma consulta quântica pode ser distribuída em superposição por muitas posições da entrada. A explicação da PSI relaciona esse modelo a polinômios: após T consultas quânticas, a probabilidade de o algoritmo responder “sim” é um polinômio limitado dos bits da entrada, de grau no máximo 2T. Assim, simular o algoritmo quântico se torna uma questão de estimar esse polinômio sem ler um número exponencial de bits da entrada.

Em seu artigo original, Scott Aaronson e Andris Ambainis conjecturaram que todo polinômio limitado de baixo grau tem uma variável altamente influente. Eles provaram que, supondo válida a conjectura, todo algoritmo quântico de T consultas pode ser simulado, na maioria das entradas, por um algoritmo clássico que faz um número de consultas polinomial em T. A consequência é um crescimento polinomial, e não exponencial, do número de consultas clássicas, para qualquer erro de aproximação e fração de entradas excluídas fixos; isso não descarta vantagens quânticas exponenciais para problemas com uma estrutura adequada.

Formalmente, o repositório considera um polinômio real p de grau no máximo d, cujos valores no cubo discreto estão entre 0 e 1. Se sua variância em relação a uma entrada escolhida uniformemente ao acaso for pelo menos ε, alguma coordenada terá uma influência de pelo menos (8√15 / (125π⁴)) · ε^(5/2) / d⁶ e, consequentemente, de pelo menos (ε/d)⁷. Influência é a variação quadrática esperada de p quando o bit dessa coordenada é invertido.

Como a prova foi construída e verificada

O argumento segue um plano de Shachar Lovett e Jiapeng Zhang, baseado em certificados fracionários e conjuntos de nível, mas substitui por uma nova desigualdade válida para todos os pares uma desigualdade que o plano deixava como conjectura. Um determinante gera um emparelhamento bijetivo entre configurações de entrada. Segundo a PSI, esse emparelhamento vai além do emparelhamento mais fraco do Lema da Borboleta de David Reimer, pois também limita a frequência com que configurações emparelhadas coincidem em cada coordenada, um limite necessário para a nova desigualdade.

O repositório divide a prova elementar em quatro partes: derivar a desigualdade válida para todos os pares a partir do determinante e da bijeção, integrá-la sobre conjuntos de nível, calcular a média sobre as coordenadas e estabelecer um limite para as linhas com um limite pontual de sensibilidade. Juntas, essas etapas produzem o limite explícito para a influência.

De acordo com a auditoria registrada no repositório, o desenvolvimento formal não contém lacunas de prova nem axiomas acrescentados. As declarações foram reexecutadas pelo núcleo do Lean e pelo lean4lean, uma implementação independente do verificador de tipos do Lean. Em uma execução isolada, um comparador que usa os núcleos do nanoda e do Lean aceitou os quatro teoremas finais; em uma segunda máquina, aceitou uma solução pequena correta e rejeitou quatro soluções deliberadamente incorretas.

Essas verificações têm limites explícitos. O leitor ainda precisa confirmar que o enunciado formal corresponde à conjectura publicada. O artigo em linguagem natural não foi, por si só, verificado por máquina, enquanto o núcleo e o compilador do Lean, as definições do Mathlib e as máquinas usadas na verificação continuam fazendo parte da base de confiança.

Papéis humanos e revisão de especialistas

David Turturean, membro da equipe técnica da PSI, desenvolveu e executou o sistema de pesquisa, definiu o escopo do problema, orientou o modelo a preparar uma primeira versão, revisou esse rascunho e é responsável pela correção do artigo. O repositório informa que modelos de IA produziram os enunciados matemáticos, a primeira versão e a formalização em Lean. Jim Halverson auditou a prova, e Phiala Shanahan fez comentários sobre a formalização.

O anúncio vem na sequência de um artigo enviado em 19 de agosto de 2026 por Guy Blanc, Jordan Docter, Carmen Strassle e Li-Yang Tan. Esses autores haviam estabelecido a consequência para a simulação clássica de algoritmos quânticos paralelos, provando que um algoritmo com t consultas e d rodadas pode ser simulado, na maioria das entradas, com t^(O(d²)) consultas clássicas. Segundo a PSI, os quatro autores estão lendo a prova completa, enviaram comentários e estão preparando uma exposição mais curta para especialistas.

Em sua avaliação publicada pela PSI, os pesquisadores escreveram: “Este é um resultado enorme. Ele resolve uma conjectura de décadas, com implicações importantes para a natureza dos problemas que admitem acelerações quânticas. A demonstração se baseia em várias linhas de pesquisa sobre análise de funções booleanas e combinatória probabilística, que também amplia. Tudo é reunido de uma maneira quase mágica.”

O teste imediato é excepcionalmente concreto: kernels independentes podem reproduzir o argumento codificado, enquanto especialistas ainda precisam confirmar que a afirmação codificada corresponde à conjectura de Aaronson e Ambainis e avaliar as partes do artigo que estão fora do Lean. Essa divisão determina o que as verificações da máquina estabelecem e o que ainda requer análise matemática humana.