OpenAI resolve 377 problemas matemáticos e desafia cientistas

Inteligência Artificial

Modelos avançados da OpenAI solucionam desafios matemáticos complexos, provocando debates sobre o futuro do raciocínio humano.

Leia também: IA de Stanford cria esboços genéticos de vírus em nova pesquisa

Modelos internos de inteligência artificial da OpenAI resolveram 377 problemas matemáticos complexos, incluindo uma proposta de solução para as equações de Navier-Stokes, mas o avanço que impressiona pela velocidade também acende um alerta: para parte da comunidade científica, a forma como essas máquinas produzem respostas ameaça a própria natureza da matemática como campo de raciocínio humano.

Os sistemas atacam questões em áreas como álgebra, teoria dos números e topologia, usando linguagens de programação e softwares de verificação formal como o Lean. Entregam provas longas, densas e tecnicamente corretas do ponto de vista lógico — a de Navier-Stokes tem 166 páginas —, porém escritas para máquinas, não para pessoas. Matemáticos brasileiros e estrangeiros veem aí um risco real de ruptura na forma como o conhecimento é produzido, compartilhado e ensinado.

Como a inteligência artificial pode impactar o campo da matemática?

Ao resolver 377 problemas complexos em ritmo industrial, a IA muda o foco da matemática do processo para o resultado: ela entrega respostas rápidas, mas quase nada de compreensão humana sobre o caminho até lá.

Na prática, isso pode encurtar décadas de trabalho em certos tópicos, acelerar descobertas e até destravar áreas que estavam paradas. Mas também desloca o centro de gravidade da disciplina. Em vez de artigos escritos para que outros matemáticos entendam, critiquem e reutilizem ideias, surgem códigos e provas formais difíceis de ler, com poucas referências e pouca explicação conceitual.

Para Marcelo Viana, diretor-geral do Instituto de Matemática Pura e Aplicada (IMPA), o perigo não está só na automação, mas em como ela é feita. “O que fez a matemática avançar até hoje é muito mais fazer perguntas do que respondê-las. No processo, você pega ideias anteriores, interpreta e entende em profundidade. Assim, cria pontes para novas ideias. É um processo enriquecedor. A IA não faz nada disso. Ela produz um código que prova a todo custo que você resolveu o problema. Mas o que você pensou?”, questiona.

A crítica toca num ponto central da cultura matemática: provar um teorema não é apenas checar que cada passo está correto, e sim construir uma narrativa conceitual que explique por que aquelas ideias funcionam, de um jeito que outros consigam aprender, adaptar e levar adiante.

Entenda o contexto

O contraste fica claro quando se lembra de dois marcos históricos. Um deles é o Último Teorema de Fermat, que ficou aberto por 357 anos até ser demonstrado por Andrew Wiles, num trabalho que gerou ramos inteiros de pesquisa e influenciou áreas como a criptografia moderna. Ali, o que importa tanto quanto a resposta é a rede de conexões criada ao longo do caminho.

O outro é o Teorema das Quatro Cores, cuja solução, em 1976, foi a primeira a depender fortemente de computador: Kenneth Appel e Wolfgang Haken usaram máquinas para checar milhares de casos. Mesmo naquela ocasião, houve debate sobre o quanto os humanos ainda entendiam de fato a prova. Agora, a escala aumentou: em vez de um único problema checado por computador, são centenas de questões resolvidas por modelos generativos, com passos lógicos certificados por softwares, mas sem uma explicação escrita para humanos.

Ferramentas como o Lean, criado pelo brasileiro Leonardo de Moura em 2013, ganham um papel central. Elas são usadas para garantir que cada linha da prova siga as regras da lógica. Porém, isso não significa que alguém entenda conceitualmente o que está acontecendo. “O material produzido por IAs não segue a lógica de um artigo comum de matemática. No trabalho de Navier-Stokes, a introdução é até bem escrita, mas, quando começa a fazer matemática, é como se ele escrevesse para outra máquina. O problema é que a gente precisa fazer matemática para humanos”, diz Ricardo Martins, professor do Instituto de Matemática, Estatística e Computação Científica da Unicamp (IMECC/Unicamp).

Outro problema é a pobreza de referências. Enquanto artigos tradicionais chegam a trazer 60 citações detalhadas, as provas geradas pela IA listam algo como dez. Isso dificulta mapear de onde vêm as ideias, verificar interpretações e inserir o novo resultado numa tradição de conhecimento coletivo.

Existe risco da inteligência artificial substituir ou destruir a matemática tradicional?

O risco apontado por especialistas não é de a IA “acertar demais”, mas de esvaziar o papel do pensamento humano ao transformar a matemática em um jogo de verdadeiro ou falso rodado em data centers, com pouco espaço para criatividade, interpretação e debate.

Depois do anúncio sobre Navier-Stokes e dos 377 problemas solucionados, um grupo de grandes nomes do campo — incluindo ganhadores da Medalha Fields — divulgou uma carta alertando para a “produção em massa” de resultados binários como ameaça ao terreno fértil de novas ideias. A avaliação é que, se o objetivo vira apenas acumular provas mecânicas, sem clareza conceitual, a matemática deixa de ser um empreendimento intelectual compartilhado.

No Brasil, a preocupação tem camadas adicionais. Por um lado, o país conquistou relevância internacional em áreas como equações diferenciais parciais, justamente o campo que abriga Navier-Stokes, com investimento modesto e uma característica vista como virtude: fazer matemática é relativamente barato, basta gente bem formada, quadro e giz. Se a pesquisa de ponta passar a depender de treinar modelos que custam dezenas de milhões de dólares, abre-se uma nova fronteira de exclusão científica, concentrando avanços em poucos laboratórios ricos.

Por outro lado, há o impacto sobre a formação de novos pesquisadores. Teses de mestrado e doutorado, que giram em torno da solução de um único problema ao longo de anos, tendem a perder espaço diante de sistemas capazes de esgotar questões similares em horas. A expectativa entre professores universitários é de que os trabalhos acadêmicos tenham de se tornar mais conceituais, comparativos e ambiciosos, indo além de provar um enunciado específico.

Isso não significa que a matemática tradicional esteja condenada a desaparecer, mas aponta para uma mudança de papel do matemático. Em vez de ser apenas o autor direto de provas, o pesquisador pode passar a funcionar como curador e intérprete: alguém que escolhe quais perguntas fazer às máquinas, traduz resultados opacos em ideias compreensíveis e decide quais caminhos valem ser explorados em profundidade.

Como pesquisadores estão reagindo ao avanço da IA na área da matemática?

A reação da comunidade mistura fascínio com inquietação. Ninguém ignora a façanha técnica de atacar problemas em aberto há 90 anos, como Navier-Stokes, com provas verificadas formalmente. Ao mesmo tempo, cresce a pressão para que empresas de IA mudem a forma de divulgar esses resultados e abram espaço real para escrutínio acadêmico.

Frente às críticas, a OpenAI criou grupos de trabalho com matemáticos para discutir a relevância das soluções e a melhor maneira de comunicá-las. A verificação independente de tudo o que foi apresentado deve levar anos, justamente porque as provas são longas, altamente técnicas e escritas em linguagem formal.

Em instituições brasileiras como o IMPA, a USP e a Unicamp, a discussão já entra em reuniões de departamento e seminários. Há quem veja uma oportunidade de usar esses modelos como assistentes poderosos, automatizando partes repetitivas da pesquisa. Mas também há quem enxergue, nas palavras de Viana, um “desalinhamento de interesses”: a matemática estaria sendo usada como vitrine para valorizar empresas de tecnologia e suas ofertas de ações, sem que a humanidade aprenda de fato com o processo.

Enquanto isso, softwares de verificação como o Lean ganham protagonismo como árbitros de correção lógica, mas não substituem o que falta: provas que conversem com pessoas, e não apenas com outras máquinas.

Fonte: matéria original