OpenAI reacende debate sobre provas matemáticas feitas por IA

A OpenAI anunciou que um de seus modelos internos resolveu 377 problemas matemáticos complexos, em áreas como álgebra, teoria dos números e topologia, e afirmou anteriormente ter solucionado as equações de Navier-Stokes, um problema em aberto há cerca de 90 anos. Os anúncios reacenderam o debate entre matemáticos sobre a confiabilidade das provas produzidas por inteligência artificial (IA) e os efeitos da automação sobre a pesquisa.

As equações de Navier-Stokes descrevem o movimento de fluidos, como líquidos e gases. Uma de suas questões centrais integra os Problemas do Milênio, uma lista de desafios matemáticos cuja solução exige uma prova aceita pela comunidade científica. A demonstração atribuída à OpenAI tem 166 páginas e ainda passa por análise de pesquisadores; portanto, o anúncio da empresa não equivale a uma validação definitiva do resultado.

A matemática não dispõe de um órgão central que certifique provas. A aceitação depende da avaliação de especialistas, que verificam se o raciocínio é válido e se a demonstração sustenta a conclusão. Marcelo Finger, professor do Instituto de Matemática e Estatística da Universidade de São Paulo (USP), disse que ninguém verificou ainda todos os resultados apresentados pela OpenAI e que o processo pode levar anos.

Parte da discussão não se limita a saber se uma resposta está correta. Matemáticos também questionam se as ferramentas conseguem apresentar um caminho compreensível, que possa ser conferido e aproveitado para desenvolver novas ideias. Marcelo Viana, diretor-geral do Instituto Nacional de Matemática Pura e Aplicada (IMPA), afirmou que o avanço da área depende tanto de formular perguntas e conectar conceitos quanto de resolver problemas.

Segundo Viana, os sistemas podem produzir códigos que demonstram formalmente uma solução sem tornar claro o raciocínio que levou a ela. Ricardo Martins, professor do Instituto de Matemática, Estatística e Computação Científica da Universidade Estadual de Campinas (Unicamp), avaliou que o trabalho sobre Navier-Stokes começa com uma introdução acessível, mas se torna difícil de acompanhar quando entra nas demonstrações matemáticas.

Esses sistemas podem usar ferramentas de verificação formal, programas que checam se uma prova segue regras lógicas definidas. Um exemplo é o Lean, criado em 2013 pelo brasileiro Leonardo de Moura. Mesmo quando a lógica é verificada por software, a apresentação pode continuar densa e pouco acessível a leitores humanos, o que não elimina a necessidade de examinar o conteúdo e explicar os passos da demonstração.

Pesquisadores também apontam que os documentos gerados por IA costumam trazer menos referências bibliográficas e de forma mais genérica do que artigos matemáticos escritos por pessoas. Isso pode dificultar a identificação das ideias anteriores usadas na prova e a avaliação de como o resultado se relaciona com o conhecimento existente. No caso das demonstrações atribuídas à OpenAI, a comparação apresentada pelos matemáticos é de cerca de dez referências, ante aproximadamente 60 em provas humanas.

O uso de computadores em demonstrações matemáticas não começou com a IA. Em 1976, Kenneth Appel e Wolfgang Haken recorreram a um computador para solucionar o Teorema das Quatro Cores, proposto em 1852. A diferença agora, segundo os pesquisadores ouvidos, está na escala das respostas e na possibilidade de que partes essenciais do raciocínio fiquem opacas para quem não consegue interpretar o código ou os sistemas usados.

Outro caso histórico é o Último Teorema de Fermat, proposto em 1637 e demonstrado por Andrew Wiles em 1994, após sete anos de trabalho. A busca pela solução contribuiu para o desenvolvimento de áreas da matemática. Esse exemplo é usado para ilustrar por que pesquisadores valorizam não apenas a resposta final, mas também os métodos e as conexões criados durante a investigação.

A preocupação levou 25 ganhadores da Medalha Fields, prêmio internacional da matemática, a publicar uma carta depois do anúncio sobre Navier-Stokes. O documento alerta que a produção acelerada de afirmações classificadas como verdadeiras ou falsas pode prejudicar o ambiente de pesquisa que permite o surgimento de novas ideias. Após a divulgação dos resultados, a OpenAI formou um grupo de trabalho com matemáticos para ajudar a comunicar e avaliar a relevância das descobertas.

Viana disse que empresas podem usar problemas matemáticos como referência para comparar o desempenho de modelos de IA e promover seus produtos, sem que isso necessariamente resulte em avanço científico compartilhado. Ele também apontou o risco de a pesquisa de ponta depender de modelos caros, concentrados em grandes laboratórios. A OpenAI teria gasto US$ 20 milhões para resolver Navier-Stokes, segundo o relato do custo associado ao trabalho.

Para pesquisadores brasileiros, a dependência de sistemas de alto custo poderia ampliar a desigualdade no acesso à pesquisa. Martins observou que o país conquistou destaque internacional em matemática com investimento relativamente baixo em ciência e ressaltou que a área é, em parte, acessível porque depende de bibliografia e trabalho intelectual. Se os avanços passarem a exigir grandes modelos, universidades com menos recursos podem ter dificuldade para acompanhar.

A formação acadêmica também pode mudar. Finger afirmou que teses de mestrado e doutorado talvez precisem ir além da solução de um problema pontual, com pesquisas mais amplas e conceituais. Com a IA assumindo tarefas de resolução, os matemáticos terão de discutir como preservar a compreensão, a verificação e a criação de conhecimento que dão sentido aos resultados.