A 1 de agosto de 2026, a OpenAI anunciou que uma versão interna do seu próximo modelo, chamada Astra, apresentava novos resultados sobre dez problemas em aberto de matemática e de informática teórica. Todos estavam por resolver há pelo menos dez anos. Astra é um modelo interno, não publicado: ninguém fora da OpenAI o consegue executar.
A formulação mais simples, e a menos informativa, é dizer que uma inteligência artificial resolveu problemas de matemática. O interesse do caso não está aí. É uma formulação preguiçosa, e o interesse do caso não está aí. Está numa pergunta mais estreita e bastante mais útil: como é que sabemos que aquilo que foi publicado é verdadeiro, e onde é que essa certeza para exatamente? Existe uma resposta técnica precisa a essa pergunta, e ela é mais instrutiva do que o anúncio.
O que foi publicado, exatamente
O material colocado online tem três camadas, e vale a pena separá-las porque não têm o mesmo estatuto epistémico:
- Um manuscrito de 249 páginas. É a exposição matemática, escrita para ser lida por humanos.
- Os traços de raciocínio do modelo. O percurso que conduziu aos enunciados. Interessante para inspeção, sem qualquer valor de prova.
- Certificados de prova em Lean 4. Ficheiros verificáveis por máquina. É esta camada que muda alguma coisa.
O conjunto está no GitHub, sob licença Apache 2.0. Qualquer pessoa pode descarregar os certificados e submetê-los ao verificador.
O que significa um contador “sorry” a zero
O repositório de certificados exibe um contador sorry a zero. Em Lean, sorry é a palavra que permite admitir um passo sem o demonstrar. Escreve-se para tapar provisoriamente um buraco na formalização e continuar a trabalhar no resto: o ficheiro passa, mas o buraco fica assinalado.
Um contador a zero significa, portanto, que nenhuma etapa da formalização ficou por demonstrar. Nenhum lema admitido, nenhum atalho tolerado. É uma métrica banal para quem trabalha com assistentes de prova e é, ao mesmo tempo, a informação mais dura de todo o anúncio, porque é a única que não depende da palavra de ninguém.
Os domínios cobertos e o resultado principal
Os dez resultados repartem-se por teoria dos grupos, álgebras de von Neumann, geometria em dimensão elevada, complexidade quântica, criptografia sobre reticulados euclidianos e combinatória extremal. O resultado apresentado como principal é a primeira construção explícita de um grupo não sófico. A soficidade foi introduzida por Mikhail Gromov em 1999, e desde então a existência de um grupo não sófico era uma questão central e em aberto da teoria dos grupos. Astra terá também resolvido três problemas associados a Paul Erdos.
Thomas Bloom, matemático na Universidade de Manchester e responsável pelo catálogo dos problemas de Erdos, qualificou os resultados de “big news” no X. É a reação de alguém cujo trabalho consiste precisamente em saber que problemas de Erdos continuam em aberto.
Porque é que o Lean muda o estatuto da afirmação
A objeção habitual aos modelos de linguagem em matemática chama-se alucinação. Um texto pode ser fluente, plausível, bem estruturado e falso, e a fluência não é indício nenhum de validade. Uma prova redigida em linguagem natural, mesmo impecável, exige um leitor competente que a arbitre. Em domínios muito especializados esses leitores são poucos e estão ocupados, e até que se pronunciem a afirmação fica em suspenso.
Um certificado Lean desloca o problema. A validade deixa de depender de leitura e passa a depender de execução: o ficheiro compila ou não compila. Não há interpretação, não há benefício da dúvida, não há passo “evidente” que o autor decidiu não escrever. Uma afirmação que passou por um verificador mecânico é de uma ordem diferente de uma afirmação produzida por um modelo de linguagem, e é exatamente isto que responde à crítica das alucinações.
A consequência prática merece ser dita sem rodeios: para a parte formalizada, a pergunta “o modelo inventou?” está encerrada. Não é uma questão de confiar ou não na OpenAI. É uma questão de correr um programa.
Onde essa certeza para: o Lean valida o enunciado, não a pergunta
Chegamos ao ponto exato onde a garantia para, e que corresponde a uma das reservas levantadas por investigadores exteriores.
Uma compilação Lean bem-sucedida confirma que a prova é válida para o teorema tal como está formulado em Lean. Não confirma, por si só, que esse enunciado formal capta o problema em aberto tal como a comunidade matemática o entendia.
Entre as duas coisas está a formalização, que é um ato humano de tradução. Escrever “existe um grupo não sófico” em Lean obriga a fixar definições, quantificadores e hipóteses de fundo. Se a tradução deslizar, ainda que ligeiramente, obtém-se uma prova perfeitamente válida de um teorema que não é aquele que se julgava estar a demonstrar. O verificador não deteta esse deslize, porque só conhece o que lhe foi escrito. Ele verifica a resposta, não a pergunta.
Isto não é uma acusação, é a descrição correta do que um assistente de prova faz. Mas tem uma implicação que convém não perder: a verificação por máquina desloca o ponto de confiança, não o elimina. Deixa de ser preciso confiar na cadeia de raciocínio e passa a ser preciso confiar na fidelidade do enunciado. Esse julgamento cabe a matemáticos humanos, exige tempo, e à data de hoje não está encerrado. Dizer que a comunidade validou os enunciados formais como equivalentes aos problemas em aberto seria afirmar precisamente aquilo que continua em suspenso.
Verificável não quer dizer reproduzível
A segunda reserva é de outra natureza. Investigadores externos assinalaram que pessoal da OpenAI participou na preparação dos artigos e na formalização dos argumentos. E ninguém fora da empresa consegue executar o modelo que fez o trabalho, uma vez que Astra não foi publicado.
Daí uma distinção que raramente é feita com clareza:
- Verificar é pegar no artefacto produzido e confirmar que se sustenta. É possível aqui, e é precisamente o que os certificados Lean permitem.
- Reproduzir é voltar a correr o processo, de forma independente, e obter o mesmo resultado. Não é possível aqui.
Uma disciplina experimental exige normalmente as duas coisas. Neste caso existe apenas a primeira. Está estabelecido que as provas publicadas compilam. Não está estabelecido que um modelo, colocado perante um problema em aberto, produza este tipo de resultado de forma repetível e sem assistência humana pelo caminho.
O viés de seleção
A terceira reserva está ligada à anterior. Foi a OpenAI que escolheu quais os resultados a publicar. Isso tem uma consequência de leitura que convém explicitar: o que vemos é o numerador. O denominador, ou seja o número de tentativas, de becos sem saída e de enunciados abandonados pelo caminho, não foi divulgado. Uma taxa de sucesso não se calcula a partir dos sucessos.
O que os 2 000 dólares querem dizer, e o que não querem dizer
O número que mais circulou é o custo: cerca de 2 000 dólares de computação. À primeira vista é impressionante, e é aqui que a leitura descarrila com mais frequência.
Investigadores apontaram a nuance decisiva: esse valor cobre as execuções bem-sucedidas, não a totalidade das tentativas do modelo. Trata-se, portanto, de um custo de publicação, não de um custo de descoberta.
Por outras palavras, 2 000 dólares é o preço dos caminhos que deram certo, medido depois de já se saber quais eram. O custo real da descoberta inclui tudo o que não deu em nada, e esse número não foi tornado público. Qualquer extrapolação do género “agora resolve-se um problema em aberto por 2 000 dólares” apoia-se num valor que não mede isso.
Gary Marcus fez notar, por seu lado, que por impressionantes que sejam os resultados, não estabelecem nem uma inteligência artificial geral nem a chegada iminente de um resolvedor universal. Registamos a observação e ficamo-nos por aí, porque não é sobre isso que os certificados Lean dizem seja o que for.
O que um dirigente pode retirar daqui, sem extrapolar
A lição transferível não é “a inteligência artificial faz matemática”. É o formato do artefacto.
- Aquilo que uma máquina pode verificar, pode ser mais delegado. Em software isto já existe e chama-se compilação tipada, suite de testes, validação de esquemas, contratos de API. Quando a saída de um sistema passa por um crivo automático, o custo de confiar nela desce de forma real. Quando só um humano a pode julgar, não desce.
- Distinga verificável de reproduzível ao avaliar um fornecedor. Uma demonstração que se consegue conferir uma vez não é um processo que corra todos os dias. São duas garantias diferentes e é útil perguntar qual das duas está a ser oferecida.
- Desconfie dos custos unitários de manchete. O valor anunciado exclui quase sempre os falhanços. A pergunta a fazer é qual foi o denominador.
- A parte difícil continua a ser a especificação. Traduzir o problema real num enunciado exato é o sítio onde as coisas correm mal, e é tão verdade em Lean como num caderno de encargos. Uma aplicação pode passar todos os testes e responder à pergunta errada.
O que não decorre daqui: nada nestes resultados indica que um modelo genérico, acessível hoje, faça este tipo de trabalho. Astra é interno e não foi publicado. Quem estiver a montar processos assistidos por modelos tem mais a ganhar em copiar o método (produzir saídas verificáveis por máquina) do que em esperar pelo modelo. Se quiser discutir o caso concreto da sua empresa, escreva-nos através do formulário de pedido: trabalhamos por escrito e respondemos em 24 horas úteis.
Conclusão
Vale a pena arrumar as duas listas lado a lado.
Está estabelecido que a OpenAI apresentou novos resultados sobre dez problemas em aberto há pelo menos uma década, que o material é público sob licença Apache 2.0, que os certificados Lean 4 compilam sem um único sorry, e que a fatura de computação anunciada para as execuções bem-sucedidas ronda os 2 000 dólares.
Não está estabelecido que os enunciados formais correspondam aos problemas em aberto tal como a comunidade os entendia, que o processo seja reproduzível fora da OpenAI, que se conheça a taxa de sucesso do modelo, nem que 2 000 dólares meçam o custo de descobrir o que quer que seja.
É raro ter uma fronteira tão nítida entre as duas listas. É isso que torna o caso interessante. O Lean não fez desaparecer a incerteza: empurrou-a para um sítio onde se consegue apontá-la com o dedo. Saber exatamente aquilo de que se duvida já é uma forma de progresso, e é bastante mais do que a maioria dos anúncios deste ano permitiu.
