Diego Mirhan
Assinar

Opinião · · 4 min de leitura

A IA já produz provas de matemática em série; o gargalo agora é conferir

A OpenAI publicou 722 manuscritos de matemática gerados por um modelo interno. Produzir prova ficou barato; conferir, não. Minha aposta e o que isso muda para quem programa.

"722" em letras enormes sobre uma onda de luz azul; manuscritos de um modelo da OpenAI, nem todos verificados.

Minha aposta é que o problema da matemática feita por IA deixou de ser achar a prova e passou a ser conferir se ela está certa. O sinal mais forte veio na terça-feira (06/10): a OpenAI publicou 722 manuscritos produzidos por um modelo interno, organizados em 372 famílias de resultados, segundo o repositório no GitHub, e avisou que parte deles ainda não foi verificada.

O que está acontecendo

O anúncio saiu no blog da empresa com o título Sharing AI progress in mathematics. O modelo, que ainda não foi lançado, recebeu cerca de 4 mil problemas, e cada resultado consumiu em média o equivalente a três horas de raciocínio do ChatGPT Pro, de acordo com o README do repositório.

Parte das provas vem formalizada em Lean, uma linguagem de programação em que o computador confere cada passo de uma demonstração. Não todas: o mesmo README diz que muitos manuscritos foram formalizados, mas não todos, e que alguns dos resultados sem formalização "podem ter problemas".

A publicação fecha um mês agitado. Em 8 de setembro, a OpenAI disse ter resolvido o problema de Navier–Stokes, um dos sete Problemas do Milênio, com cerca de 10 mil agentes trabalhando em paralelo por 88 horas, segundo a CNBC.

A MIT Technology Review registrou que esse esforço custou milhões de dólares e que o matemático Tristan Buckmaster, da NYU, acusou a empresa de partir do trabalho dele e de Levent Alpöge sem dar crédito. A OpenAI nega.

Duas semanas depois, a empresa criou um grupo consultivo de matemáticos no Institute for Advanced Study, em Princeton, e afirmou que o mesmo modelo resolveu mais de 100 problemas em aberto, segundo o TechCrunch. No mesmo mês, 25 ganhadores da Medalha Fields assinaram uma carta aberta dizendo que a corrida entre os laboratórios ameaça o trabalho intelectual deles, conforme a mesma reportagem.

Por que acho que o gargalo mudou de lugar

Produzir uma prova ficou barato. Três horas de computação por resultado é pouco perto dos meses que um matemático costuma passar num problema difícil, e acho que nenhum grupo de pesquisa consegue ler 722 manuscritos com cuidado num semestre.

Conferir continua caro. Uma auditoria independente publicada no arXiv revisou os 10 resultados que a OpenAI anunciou em 1º de agosto e precisou cruzar 18 avaliações de especialistas com formalizações em Lean e trabalhos posteriores de outros matemáticos.

O resultado foi bom para a OpenAI, com ressalvas. Os autores não encontraram erro confirmado em nenhum resultado principal, mas um capítulo recebeu pedido de revisão grande, e várias dependências só foram verificadas em parte, segundo a auditoria.

A mesma auditoria traz o alerta que acho mais importante. O Lean garante que a frase formalizada está provada, mas não garante que essa frase diz o que os autores queriam dizer. Esse segundo passo continua sendo trabalho humano, de acordo com os autores.

Minha leitura é que, quando gerar fica quase de graça, o valor vai para quem verifica. Foi assim com a revisão de código gerado por agentes, e acho que a matemática está entrando no mesmo caminho.

A previsão: até outubro de 2027

Aposto que, até outubro de 2027, todo resultado que a OpenAI, a Google DeepMind ou a Anthropic anunciarem como novo em matemática vai sair com a prova principal formalizada em Lean no dia do anúncio. Hoje, na OpenAI, isso vale para muitos manuscritos, mas não para todos, nas palavras do próprio repositório.

Também aposto que a discussão vai mudar de "a prova está certa?" para "o enunciado formalizado é mesmo o problema que dizem ter resolvido?". Acho que é nesse ponto que vão aparecer as primeiras correções públicas.

Dá para conferir. Em outubro de 2027, basta contar quantos anúncios de resultados dos três laboratórios saíram com a formalização completa.

O que me faria mudar de ideia

Dois sinais. O primeiro é a formalização continuar parcial porque formalizar ficou mais caro que provar: se em 2027 os anúncios ainda vierem com só uma parte das provas em Lean, a minha aposta perde.

O segundo é a comunidade criar uma revisão humana que acompanhe o volume, por exemplo, com revistas montando um processo próprio para resultados gerados por IA. Isso tiraria a pressão pela formalização.

Também pesa o que ainda não dá para checar. O modelo que gerou os resultados não foi lançado, e ninguém de fora consegue repetir o processo. A própria OpenAI diz no post do anúncio que trabalha para liberar o modelo.

O que isso muda para quem constrói software

A lição vale para código. Um agente de programação também gera mais do que alguém consegue revisar, e um teste que passa só prova o que o teste verifica, do mesmo jeito que o Lean só prova o enunciado que foi escrito.

Na prática, o esforço vai para a especificação: escrever bem o que o código precisa garantir, com testes que descrevem o comportamento esperado e tipos que impedem estados inválidos. Na revisão, vale mais ler com cuidado o que o teste afirma do que a implementação que o agente gerou.

Minha posição é que gerar ficou barato, na matemática e no código. Quem vai valer mais daqui para frente é quem sabe dizer, com precisão, o que precisa ser verdade.

Fontes

Gostou? Receba o próximo

Um e-mail a cada post novo. Sem spam.

Próximo post Mistral Large 4 tem 1 trilhão de parâmetros, mas os pesos só saem no fim de outubro