Quando uma IA propõe uma demonstração, a questão não é apenas saber se o texto parece convincente. É preciso poder verificar o raciocínio, compreender exatamente o que foi demonstrado e determinar o que muda com o resultado. O Lean intervém neste processo com uma força particular: as suas verificações incidem sobre uma prova formalizada. Isso não transforma, contudo, todos os anúncios acompanhados da palavra «verificado» em descobertas definitivamente compreendidas.
A 26 de outubro de 2026, a OpenAI reivindicou três resultados em matemática, informática teórica e física. A empresa anuncia uma prova da conjectura do alisamento local em todas as dimensões, com consequências para Kakeya, uma refutação da hipótese do tempo exponencial e um resultado de existência em teoria quântica de campos. Descreve uma divulgação diferenciada: materiais públicos para as duas primeiras áreas, ficando a publicação dos documentos de física a cargo do grupo de investigadores incumbido de os estudar.
Estas reivindicações voltam a colocar em primeiro plano uma distinção: produzir uma prova, verificá-la e estabelecer o seu alcance são três trabalhos relacionados, mas diferentes.
O que o Lean recebe realmente
A documentação do projeto Lean explica que os scripts e as táticas de prova produzem um objeto explícito, chamado termo de prova. Um componente restrito, o núcleo, verifica depois a sua construção lógica. A tática é o meio utilizado para procurar ou construir a prova; não é, por si só, aquilo que lhe confere validade.
Esta separação é importante para a IA. Um sistema pode propor uma pista errada, tentar uma estratégia ineficaz ou gerar uma explicação muito confiante: nenhum destes comportamentos substitui o objeto que o verificador tem de aceitar. A verificação não se reduz, portanto, a perguntar a um segundo modelo se considera a resposta plausível.
O Lean é também uma linguagem de programação, não apenas um corretor de trabalhos de matemática. Entre as suas utilizações estão a verificação de software e de protocolos. Em todos estes casos, o benefício depende de um trabalho prévio: expressar com precisão as propriedades que se pretende estabelecer. Uma propriedade mal escolhida pode ser demonstrada na perfeição e continuar a ser insuficiente para a utilização prevista.
A prova certa tem de responder à pergunta certa
Consideremos um exemplo deliberadamente simples, sem relação com os trabalhos anunciados. Provar que todos os números pares de um conjunto são divisíveis por dois não prova que todos os números desse conjunto são pares. A diferença está no enunciado, não na virtuosidade da demonstração. Ainda assim, um leitor apressado pode reter uma conclusão mais abrangente do que aquela que foi realmente estabelecida.
Na investigação, as diferenças são menos evidentes: o domínio de validade, as condições iniciais, as definições ou as dependências podem alterar o alcance de um teorema. O trabalho humano não consiste, portanto, apenas em admirar a extensão de um ficheiro. É preciso aproximar o enunciado formal da pergunta inicial e verificar se não se introduziu entre ambos nenhuma restrição decisiva.
O manual do Lean dedicado à validação distingue explicitamente a validade de uma prova do significado do seu enunciado. As marcas de validação no editor dizem respeito a uma conclusão obtida a partir das definições, teoremas e axiomas do projeto. Não são um certificado autónomo da novidade científica do resultado.
As hipóteses fazem parte do resultado
Um axioma é um ponto de partida aceite no quadro lógico utilizado. Acrescentar um axioma não equivale a demonstrá-lo. É por isso que o manual recomenda inspecionar as dependências com o comando «#print axioms». A presença de «sorryAx», por exemplo, indica que se recorreu a uma prova deixada incompleta no teorema ou nas suas dependências. Os axiomas padrão do Lean não devem ser confundidos com uma hipótese adicional introduzida para um caso específico.
Para contextos mais exigentes, a documentação descreve também a reverificação das provas e a sua comparação com um enunciado estabelecido num ambiente de confiança. O objetivo é concreto: verificar o objeto certo, com as hipóteses certas, nas condições certas. A fórmula «compila» não conta, por si só, todo este percurso.
Isto não diminui o interesse da formalização. Pelo contrário, tornar estes elementos examináveis dá matéria para a crítica. Uma discussão científica pode então incidir sobre uma definição precisa, uma dependência identificada ou uma discrepância reproduzível, em vez de se centrar na confiança com que um sistema apresenta a sua resposta.
AlphaProof: um exemplo documentado, não uma confirmação da OpenAI
O estudo «Olympiad-level formal mathematical reasoning with reinforcement learning», publicado na Nature, descreve outro sistema: o AlphaProof. Este aprende a procurar provas num ambiente formal, com base em tentativas e feedback verificável. Uma tática altera o estado do problema; os objetivos por resolver indicam o que falta solucionar. O resultado pode ser verificado no Lean.
Os autores relatam que foram resolvidos três dos cinco problemas da Olimpíada Internacional de Matemática de 2024 que não eram de geometria. A pontuação equivalente a uma medalha de prata combina o AlphaProof e o AlphaGeometry 2, com vários dias de cálculo. Estas condições fazem parte do desempenho: impedem que este seja apresentado como o resultado instantâneo de um assistente generalista colocado nas mesmas condições que um candidato humano.
Este estudo mostra como a investigação e a verificação se podem articular. Não valida os resultados da OpenAI, que dizem respeito a outros sistemas e a outras questões. Passar de um êxito numa competição para um avanço na investigação exige elementos específicos de cada caso.
Como ler o próximo anúncio
A OpenAI apresenta os seus manuscritos como materiais em bruto que exigem trabalho de compreensão. No domínio da informática, a empresa anuncia um grupo liderado por Russell Impagliazzo, Ramamohan Paturi e Ryan Williams. A função de uma análise deste tipo não se limita a dar um aval: deve tornar os resultados suscetíveis de discussão, explicáveis e situáveis no conhecimento existente.
Para o leitor, quatro perguntas ajudam a manter o rumo: o enunciado exato está acessível? As hipóteses são explícitas? A verificação é descrita de forma reproduzível? As conclusões científicas ou práticas vão além do que foi realmente estabelecido? Uma resposta positiva a uma delas não dispensa as outras três.
Uma demonstração formal pode ser um resultado considerável. A sua existência, contudo, ainda não diz quanto custará um cálculo útil, que áreas beneficiarão de um método ou se uma descoberta anunciada se traduzirá numa aplicação. A promessa mais sólida é mais precisa: tornar uma parte do raciocínio verificável, para que a discussão comece com algo mais do que um texto persuasivo.
Fotografia ilustrativa: um quadro com fórmulas científicas, sem relação com as provas mencionadas. Vitaly Gariev / Pexels, licença Pexels.
