Provas matemáticas geradas por IA acabam de sair do laboratório e cair direto no colo de quem pesquisa. A OpenAI publicou 372 resultados que supostamente resolvem ou avançam problemas em aberto, de melhorias em algoritmos centrais da computação até progresso ligado à hipótese de Riemann. Cada um saiu, em média, de um único prompt para um único agente, com cerca de três horas de computação do modo Thinking do ChatGPT Pro. Se isso estiver correto na escala que parece, o problema agora não é gerar matemática. É conseguir revisar, entender e confiar no que foi gerado antes que a próxima leva chegue.

O fato

A OpenAI colocou no GitHub uma coleção com 372 resultados matemáticos produzidos por um modelo interno de fronteira. Não foi em revista científica, foi em repositório com log de revisão, citações e arquivos de formalização. Segundo a empresa, quase todos os resultados vieram de uma única chamada a um único agente, com algumas tentativas extras em parte dos casos. O pacote inclui avanços em algoritmos importantes e passos relevantes em conjecturas clássicas. O mesmo modelo, diz a empresa, já teria produzido uma solução para um problema de Navier-Stokes que está há semanas em revisão formal.

PublicidadeAnuncie aqui336x280 / responsivo

O contraste de escala é o que chama atenção para quem opera sistema. Essa leva de 372 resultados teria custado, em média, três horas de computação pesada por item. Já a solução de Navier-Stokes exigiu um enxame de 10 mil agentes e milhões de dólares em computação. Ou seja, estamos falando de dois regimes diferentes. Um é pesquisa concentrada, cara e dirigida, com paralelismo massivo. O outro é geração distribuída e quase rotineira, onde um prompt bem construído já cospe um candidato a teorema novo. Para laboratório universitário, isso muda a conta de recursos. Para empresa que roda inferência, muda a previsão de custo e latência por descoberta.

Como funciona na visão de operador

Na prática, o pipeline parece ter três camadas. Primeiro, o agente gera a prova em linguagem natural a partir de um prompt único, provavelmente com acesso a ferramentas de busca, execução de código e tentativa de prova assistida. Depois, parte desse material é traduzida para Lean, uma linguagem de provas verificáveis por máquina. Por fim, tudo é publicado com resumo do raciocínio, estatísticas de tentativa e estimativa média de custo. Não temos o prompt exato nem o custo por problema, apenas médias. Isso limita a reprodutibilidade, mas já dá para inferir bastante sobre arquitetura e operação.

Pense em latência e custo. Três horas de Thinking do ChatGPT Pro por resultado não é inferência barata. É raciocínio longo, com muitas chamadas internas, autorrevisão e provavelmente uso de ferramentas. Se cada hora nesse nível custar algo na ordem de dezenas de dólares em infraestrutura equivalente, cada teorema candidato sai por uma fração pequena de uma bolsa de pesquisa, mas ainda longe de ser grátis em escala. Multiplique 372 por três horas e você tem mais de mil horas de GPU de alta performance concentradas em raciocínio simbólico. É plausível para um laboratório de fronteira, impossível de ignorar para uma universidade sem orçamento de computação.

A parte de Lean é o que torna tudo operacionalmente interessante. Revisão humana de 372 provas densas levaria meses e travaria qualquer departamento. Com formalização, você troca parte da revisão lógica por verificação automática. O Lean não diz se o resultado é importante, original ou elegante. Ele só diz se a lógica fecha dentro dos axiomas. Isso resolve o gargalo de correção, mas cria outro gargalo, o de relevância. É como ter um CI que passa no teste unitário mas não diz se a feature deveria existir. Útil, mas insuficiente para decidir o que entra na base principal do conhecimento.

Onde o GitHub entra na jogada

Publicar no GitHub em vez de revista não é detalhe. Revista tradicional foi feita para poucas descobertas por ano, com revisão lenta, anônima e limitada a dois ou três pareceristas. GitHub foi feito para iteração rápida, histórico público e correção contínua. A OpenAI consultou o grupo consultivo de matemática e IA do Institute for Advanced Study, que inclui nomes como Timothy Gowers, e seguiu de forma solta as recomendações públicas deles sobre comunicação. Só que impôs um limite claro. Os matemáticos poderiam opinar sobre como comunicar, não sobre se ou em que ritmo produzir. Isso diz tudo sobre a tensão atual entre velocidade de geração e governança científica.

O que isso muda na prática

Quem ganha no curto prazo é quem já opera na interseção de IA e prova formal. Grupos com pipeline em Lean, Coq ou Isabelle conseguem ingerir esse material, rodar o verificador, filtrar o que compila e priorizar leitura humana só no que passou. Quem perde é o fluxo tradicional de seminário, preprint isolado e revisão de seis meses. Nenhum departamento tem gente suficiente para ler 372 provas de fronteira de uma vez. Sem automação na triagem, a maioria desses resultados vai ficar sem avaliação séria, mesmo que alguns sejam realmente bons. O conhecimento existe, mas não circula.

  • Para universidades: a prioridade passa a ser infraestrutura de verificação, não só contratação de gênios individuais.
  • Para builders: surge um nicho real de ferramentas para ranquear, explicar e conectar provas geradas por IA ao corpo existente da matemática.
  • Para empresas: melhorias em algoritmos vindas desse processo podem virar ganho direto em compressão, otimização e roteamento se forem validadas.

A ação prática mais imediata é simples. Se você pesquisa ou constrói com matemática pesada, monte hoje um ambiente mínimo para ler esse repositório. Instale o Lean, clone os arquivos formalizados, rode a verificação local e crie um script que extraia hipóteses, conclusões e dependências de cada prova. Depois, cruze com sua base de problemas reais. Não tente ler tudo na ordem. Filtre pelo que compila, pelo que toca no seu domínio e pelo que tem citação verificável. Em uma semana dá para separar cinco por cento que merece atenção humana de noventa e cinco por cento que pode esperar. Sem esse filtro, você será soterrado.

A tensão que ninguém quer admitir

Aqui entra a dúvida real. Isso escala ou só move o gargalo de lugar. Gerar 372 candidatos é impressionante, mas quantos são de fato novos, não triviais e bem apresentados. A própria OpenAI admite que precisa melhorar citações e apresentação. E 25 vencedores da Medalha Fields já assinaram uma carta aberta falando em desalinhamento profundo entre a indústria e a matemática, com o argumento de que resolver problema é só um proxy para o objetivo real, que é entendimento conceitual. Eles têm um ponto. Uma máquina pode cuspir afirmações verdadeiras em volume industrial sem gerar insight que ajude o próximo humano a pensar melhor.

Tem também o problema de custo e transparência. Sem prompt publicado e sem custo por problema, fica difícil saber taxa real de sucesso, quantas tentativas falharam e quanto lixo foi descartado antes dos 372 finalistas. Se a taxa for de uma em cem, o custo efetivo por resultado útil explode. Se for de uma em três, a história muda completamente. Operador experiente já viu esse filme em geração de código. No começo todo demo parece mágica, depois você descobre que o custo de curadoria, teste e manutenção come a margem. Com matemática não deve ser diferente, só que o teste é o Lean e a manutenção é a integração conceitual com décadas de literatura.

Conclusão

No fim, a OpenAI não publicou só teoremas, publicou um ultimato operacional para a academia. Ou a matemática cria um pipeline novo para ingerir, verificar e julgar prova feita por máquina, ou vai viver afogada em resultados que ninguém consegue avaliar. A pergunta que fica é direta. Quantos desses 372 vão sobreviver a um ano de escrutínio sério e virar ferramenta usada por gente de verdade.