Novo modelo de inferência interno da OpenAI lança dez avanços matemáticos impressionantes de uma só vez.
Incluindo:
- Provou-se pela primeira vez a existência de grupos não soficos (Non-sofic groups);
- Foram apresentados novos limites inferiores de circuito (Circuit lower bounds);
- Superou o limite de dificuldade do Problema do Vetor Mais Próximo (Closest Vector Problem, CVP);
- E o teorema da repetição paralela quântica com decaimento exponencial para jogos quânticos bipartidos.
O que mais importa ao professor associado da Universidade de Columbia, Henry Yuen, é o último—
Em 2016, Yuen fez grandes avanços nessa questão, mas não a resolveu completamente. Durante 10 anos, ele enfrentou repetidas falhas, e até um mês atrás ele ainda usou o ChatGPT 5.5 para uma nova tentativa de prova definitiva, com poucos resultados.
E a IA, em seu ombro, deu um leve chute, enviando a bola para a rede.
A prova está correta, mas os humanos não entenderam
Há alguns dias, Lijie Chen enviou uma versão preliminar do artigo a Henry Yuen e outras pessoas.
Na época, a vida estava corrida, e ele não tinha tempo para estudar a fundo. Agora, o artigo já foi publicado. Ele não consegue mais conter-se; tem coisas para dizer.
O teorema da repetição paralela quântica (Quantum parallel repetition theorem) é o campo em que Henry Yuen dedicou anos de esforço durante seu período de pós-graduação e também o resultado do qual ele mais se orgulha.
Henry Yuen, atualmente professor associado de ciência da computação da família Srivani na Universidade de Columbia
Ele lembrava das tardes passadas em cafés, das noites sentadas no escritório e de inúmeros fins de semana que deveriam ter sido de descanso, reiteradamente desmontando e estudando o teorema clássico de repetição paralela de Ran Raz.
Ele queria resolver a versão quântica desse teorema, e por isso não conseguia dormir, virando e revirando na cama. Ele ingeriu toneladas de ferramentas matemáticas e finalmente conseguiu provar a decaimento polinomial.
https://arxiv.org/pdf/1604.04340
Mais importante ainda, ele construiu confiança a partir disso, finalmente reconhecendo seu próprio potencial e provando que realmente consegue resolver aqueles problemas (pelo menos parte deles) que também importam para os outros.
Ele acredita que a prova da OpenAI deve estar correta, dado que já existe uma prova formalizada em Lean. No entanto, Henry Yuen ainda precisa de algum tempo para assimilar essa nova prova.
Embora a nova prova realmente continue de onde ele havia terminado anteriormente, a IA ultrapassou os limites da estratégia de prova original, utilizando certas técnicas e métodos que talvez já estejam disponíveis para pesquisadores nas áreas da teoria dos operadores e da análise funcional.
Além da empolgação, o primeiro sentimento de Yuen foi decepção, com relação ao estilo de escrita do artigo.
Ele disse que esse certificado parece cheio de sinais de IA: introduções longas e demoradas, mas os pontos essenciais são como um truque de mágica, deixando todos confusos.
A prova da OpenAI é interessante de ler, mas também um pouco frustrante.
Ele primeiro coloca o problema claramente sobre a mesa, e então de repente pula para a direção de "usar a pré-resolução para encontrar a purificação correta", deixando quase nenhum passo lógico entre eles.
Em seguida, vem uma série de cálculos de entropia de matriz bastante incomuns, que se alongam de forma complicada, e no final lhe dizem: este caminho é viável.
Mas o passo mais crucial, essa intuição de onde veio, ele não disse.
E o movimento mais sutil e mais exigente de criatividade — a técnica de expansão do espaço de operadores usando a transformação de Uhlmann — deveria ter sido o clímax mais emocionante de toda a prova, mas foi descartada pelo IA como areia e lama, lançada sem aviso nem explicação na seção quatro.
A prova correta, mas escondeu a ideia mais importante.
Ele gostaria que a OpenAI gastasse mais alguns prompts para organizar bem este roteiro.
Mais doloroso ainda é o segundo nível: a verificação do Lean não equivale à compreensão.
A máquina pode garantir que cada passo da dedução seja impecável, mas não consegue responder a perguntas como: «Por que este método funciona?», «O que ele significa no contexto mais amplo da teoria?» ou «Onde mais pode ser aplicado?» — o Lean não consegue responder a nenhuma delas.
Yuen admitiu que ainda está processando essa prova.
A resposta está diante dele, mas ele precisa, como se lê um artigo de leigo, linha por linha, reconstruir a intuição que a IA não expressou.
Sim, há uma prova Lean lá. Mas é apenas formalização e não significa que eu entendi. Para realmente assimilar, provavelmente só o tempo pode ajudar.
Sim, a IA ampliou os limites da compreensão humana, mas e daí? O que resta da alegria e do significado da pesquisa? Se a IA resolver todos os problemas que ele tanto ansiava, o que lhe restará?
As perguntas se sucedem. Mas um ponto ele ficou cada vez mais certo: os dias seguintes do matemático não serão fáceis; ele precisará domar essas bestas do pensamento e traduzir sua gíria para uma linguagem compreensível.
IA "refuta" conjectura matemática de cem anos é desmascarada! Lean também não é um cofre seguro
Na semana passada, Ramana Kumar refutou a famosa conjectura matemática não resolvida, a Conjectura de Collatz, com 300 linhas de Lean.
A pergunta que ele faz é muito simples: dado um número inteiro positivo, aplique repetidamente duas regras — se for par, divida por 2; se for ímpar, multiplique por 3 e some 1 — será que, independentemente do número inicial, você sempre acabará chegando a 1?
Você pode calcular:
Esta conjectura afirma que, independentemente de qual número inteiro positivo você escolha, acabará caindo nesse ciclo 4→2→1.
Desde que o matemático Lothar Collatz o propôs em 1937, ninguém conseguiu provar sua validade nem encontrar um contraexemplo.
Foi chamado pelo matemático Paul Erdős: “A matemática ainda não está pronta para problemas como este”, e pelo acadêmico da Academia Nacional de Ciências dos Estados Unidos, matemático Jeffrey Lagarias: “É um problema extraordinariamente difícil, totalmente além do alcance da matemática atual”.
Se for refutado, certamente será uma notícia explosiva para a comunidade matemática.
Infelizmente, três dias depois, essa prova formal em Lean foi declarada inválida, pois na verdade explorava uma vulnerabilidade de baixo nível no núcleo do Lean.
Daniel Selsam da OpenAI, com um AI especializado em segurança cibernética, auxiliou o Lean FRO em uma auditoria de kernel.
Como resultado, eles descobriram mais de uma vulnerabilidade no núcleo Lean!
Quase ao mesmo tempo, o professor de matemática da Universidade Rutgers e consultor da organização de pesquisa Lean, Alex Kontorovich, publicou uma mensagem alertando: não vejam o Lean como um verificador universal.
Ele apontou diretamente para o ponto crítico: alinhamento semântico (Semantic Alignment).
Mesmo que o núcleo Lean seja impecável, o Lean cuida apenas da compilação do código. Quem garante que a "definição" que você escreve no código seja a mesma que a "intenção intuitiva" humana expressa em linguagem natural?
O que o Lean pode confirmar é apenas uma coisa: o código compila e a lógica formal está correta. Mas ele não verifica uma questão ainda mais crítica: esta declaração formal realmente corresponde ao teorema que você deseja provar?
A prova está correta, mas o problema foi copiado errado — o Lean ainda assim sinaliza como aprovado.
E esse problema de alinhamento não pode ser resolvido apenas por computador.
Na palestra da ICM 2026, Kontorovich apontou: o maior ponto cego da matemática formalizada não está em "derivar corretamente", mas em "dizer corretamente". O último filtro ainda precisa ser feito por especialistas humanos.
O experimento Liquid Tensor foi considerado lendário justamente porque os pesquisadores realizaram uma revisão manual quase obsessiva de cada definição matemática.
Ao juntar as palavras dos dois professores, aponta-se para o mesmo fato: a IA pode provar, as máquinas podem verificar, mas compreender e supervisionar ainda são tarefas humanas.
Por fim, há um boato sobre modelos de inferência de IA:
Referências:
https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/
https://x.com/AlexKontorovich/status/2083919186825236831
https://x.com/henryquantum/status/2083623700608237956
Este artigo é do número oficial do WeChat "Nova Inteligência", autor: Apocalipse da ASI; editor: David