PSI diz que um sistema interno provou a conjectura de Aaronson–Ambainis

A Physical Superintelligence, ou PSI, afirmou em 6 de novembro de 2026 que um sistema de pesquisa interno rodando um modelo não público da Anthropic provou a conjectura de Aaronson–Ambainis, uma questão em aberto desde 2008 sobre quando computadores quânticos podem ser exponencialmente mais rápidos que os comuns. A PSI disse que o Lean aceitou uma prova completa no terceiro dia da execução e depois aceitou duas melhorias. [1]

O que é a conjectura de Aaronson–Ambainis?

PSI disse em 6 de novembro de 2026 que seu sistema de pesquisa interno provou a conjectura de Aaronson–Ambainis. [1] Scott Aaronson e Andris Ambainis questionaram se um computador quântico pode ser exponencialmente mais rápido em entradas aleatórias, que quase nunca têm a estrutura repetitiva oculta usada por acelerações famosas como o algoritmo de Shor.

Eles enunciaram uma conjectura sobre polinômios e mostraram que, se for verdadeira, computadores quânticos são no máximo polinomialmente mais rápidos em entradas aleatórias. [1] A PSI escreve que pesquisadores consideram a conjectura um dos problemas centrais em aberto da teoria da complexidade quântica.

Como a PSI diz que a prova foi encontrada?

PSI disse que o sistema, rodando um modelo não público da Anthropic, obteve uma prova aceita pelo Lean no terceiro dia da execução. [1] A empresa afirma que a execução ocorreu em sua própria infraestrutura, que o Lean verificou cada passo e que o sistema depois melhorou o resultado duas vezes, com o Lean aceitando a versão final.

David Turturean, membro da equipe técnica da PSI, liderou o trabalho: ele desenvolveu o sistema de pesquisa, delimitou o problema, executou-o e solicitou ao modelo que empacotasse os resultados em um primeiro rascunho do artigo. [1] A PSI também publicou provas e código em um repositório público no GitHub. [2]

A PSI diz que esses pesquisadores de Stanford já haviam provado um caso especial da previsão da conjectura em agosto de 2026, para algoritmos quânticos que examinam sua entrada em um número fixo de rodadas paralelas. [1] A empresa afirma que eles têm lido a prova completa, enviado comentários e estão escrevendo uma exposição mais curta para especialistas.

O que o resultado significaria se as declarações coincidirem?

Se o teorema formal for a conjectura original, a PSI diz que um computador comum pode prever a probabilidade de sim ou não de um computador quântico, com pequeno erro, para todos exceto uma pequena fração de strings, usando um número de olhares que cresce no máximo como uma potência fixa do número de olhares quânticos em vez de exponencialmente. [1]

Leitores ainda precisam confirmar que a declaração formal em Lean corresponde à conjectura original de 2008. [1][2] A nota da PSI apresenta o desenvolvimento em Lean como sem placeholders ou axiomas adicionados e diz que foi verificado novamente por kernels independentes; este artigo não repete essa verificação.

Nossa leitura

Opinião: Uma prova verificada pelo Lean de uma conjectura nomeada de 2008 seria uma reivindicação científica séria, e o comentário de Stanford citado pela PSI é marcante — mas a alegação deve ser lida como “uma prova formal existe e especialistas estão verificando”, não como uma reescrita consolidada da complexidade quântica até que as declarações sejam comparadas publicamente.

O que não pudemos verificar

• Que o teorema em Lean seja formalmente idêntico à conjectura original de Aaronson–Ambainis.
• Uma redação independente que não seja citada ou hospedada pela PSI.
• A identidade e a versão do modelo não público da Anthropic usado na execução.