Em 6 de novembro de 2026, a Physical Superintelligence (PSI) afirmou que seu sistema interno, executado com um modelo não público da Anthropic, produziu uma prova da conjectura de Aaronson–Ambainis aceita pelo Lean. O repositório público descreve o enunciado formal e suas cotas, mas atribui aos leitores a tarefa de confirmar se a formalização corresponde à conjectura pretendida. A PSI apresentou a afirmação e o contexto, e seu repositório detalha a formalização.
A conjectura, proposta por Scott Aaronson e Andris Ambainis, trata de complexidade de consultas quânticas e da influência de variáveis em polinômios limitados. A PSI a descreve como uma questão em aberto desde 2008.
O que a formalização afirma
O repositório enuncia um resultado para um polinômio real de grau no máximo d, cujos valores ficam entre 0 e 1 em {0,1}^N, o conjunto de todas as sequências de N zeros e uns. A variância do polinômio sobre entradas uniformemente escolhidas precisa ser de pelo menos ε, com ε > 0.
Nessas condições, alguma variável precisa ter influência mínima. Em termos simples, a influência de um bit mede quanto o valor do polinômio tende a mudar quando esse bit é invertido, mantendo os demais iguais. O repositório apresenta a cota explícita (8√15/(125π⁴))·ε^(5/2)/d⁶ e também expressa a versão da conjectura formalizada como (ε/d)^7.
Essas expressões especificam o limite inferior para a influência ao quadrado associada à inversão de um bit. O resultado depende das condições do polinômio, da variância e do grau; não é uma afirmação sobre qualquer função ou entrada.
O que o Lean verifica
Lean é um assistente de provas: verifica se uma demonstração formal segue das proposições escritas em sua linguagem e das definições e fundamentos usados. O repositório lista quatro declarações finais de teoremas e afirma que a formalização não tem lacunas nem axiomas adicionais. Também relata verificações pelo kernel do Lean e pelo lean4lean, outra implementação de verificação de Lean.
Essa checagem se aplica ao enunciado formal. O próprio repositório diz que ela não confirma, por si só, que a proposição chamada PrintedConjecture representa a conjectura original. Essa correspondência exige uma leitura matemática. O artigo escrito para leitores também não foi verificado integralmente por máquina; o repositório inclui o kernel e o compilador do Lean, as definições do Mathlib e as máquinas de verificação entre os elementos de confiança.
Uma prova formal pode ser conferida em relação ao enunciado que foi escrito; identificar esse enunciado com a conjectura original também exige uma interpretação matemática.
O alcance da consequência para consultas quânticas
A implicação descrita pela PSI está no modelo de complexidade de consultas. Segundo a empresa, depois de T consultas quânticas, a probabilidade de um algoritmo responder “sim” pode ser representada por um polinômio limitado de grau no máximo 2T.
A consequência que a PSI atribui à conjectura é que uma quantidade polinomial de leituras clássicas da entrada pode aproximar essa probabilidade para a maioria das entradas aleatórias, com a margem de erro e a fração de entradas fixadas. Isso trata da quantidade de consultas nesse modelo, não do tempo total de execução de qualquer tarefa quântica. Em 6 de novembro, a PSI informou que quatro pesquisadores de Stanford estavam lendo a prova, haviam enviado comentários e preparavam uma exposição mais curta para especialistas.
