O Brasil ajudou a IA a revolucionar a matemática

Na semana passada visitei meu colega de Folha, Marcelo Viana, diretor-geral do IMPA (Instituto de Matemática Pura e Aplicada). Falamos da revolução que a inteligência artificial está gerando na matemática.

Sobre o tema, leia o ótimo artigo que Marcelo escreveu com Artur Avila (brasileiro vencedor da medalha Fields) aqui na Folha.

Neste momento a matemática está em polvorosa. A razão é que um dos seus "problemas do milênio" foi resolvido com inteligência artificial, as equações Navier-Stokes que modelam o comportamento de fluidos.

O resultado está em um impressionante estudo de 166 páginas.

Duas coisas chamam atenção nele. O estudo não é assinado por ninguém. No topo consta apenas "OpenAI". E, mesmo não sendo assinado, o estudo usa o pronome "nós" para descrever os achados.

Quem seria esse "nós"? O coletivo do conhecimento humano? Um "nós" real, ou luciferiano.

O fato é que entramos em um território em que a IA está sendo usada na fronteira da matemática. O que permitiu chegarmos a este momento é o trabalho de um brasileiro: o cientista da computação e matemático Leonardo de Moura.

Doutor pela PUC do Rio, Leonardo desenvolveu em 2013 a linguagem de programação Lean, que permite a descrição e a prova de problemas matemáticos por computadores.

O impacto da criação do Lean só será compreendido com o passar dos anos. Por causa dele foi possível a criação de bibliotecas de resoluções matemáticas, traduzidas para linguagem computacional.

O Mathlib, a maior dessas bibliotecas, tem mais 400 mil "declarações.

Só foi possível para a inteligência artificial atuar na fronteira da matemática por causa do Lean. Sem ele, provar a resolução do problema Navier-Stokes não teria sido possível.

O Lean deveria estar incluído no "nós" do estudo.

O curioso é que a chegada da IA na matemática está produzindo maravilhamento e terror. Por exemplo, 25 ganhadores da medalha Fields assinaram uma carta com o título "Desalinhamento Severo da IA na Matemática.

A carta abre dizendo que "a resolução de problemas matemáticos como métrica por empresas de IA ocorre em detrimento da matemática e sua comunidade". Artur Avila está na lista das assinaturas.

De fato, um dos aspectos mais nobres da matemática é que ela pode ser feita apenas com lápis e papel. Ou melhor, podia. Agora, a fronteira da matemática passa a exigir poder computacional.

E o mais radical: torna a matemática incompreensível para nós, humanos.

Sobre isso, o jovem matemático Logan Graves escreveu: "O que sobra para essa comunidade? Converter-se em monges. Passar o resto de suas vidas tentando entender o incompreensível.

Mesmo gênios serão incapazes de entender uma única descoberta.

O pandemônio que tomou conta da matemática irá se repetir em basicamente todas as áreas de atuação humana. Quem diz isso não sou eu. São os próprios matemáticos que assinaram a carta.

Já era – fronteira da matemática feita por pessoas.

Já vem – fronteira de outras disciplinas ocupada pela IA.

LINK PRESENTE: Gostou deste texto? Assinante pode liberar sete acessos gratuitos de qualquer link por dia. Basta clicar no F azul abaixo.

Em números

• O Mathlib, a maior dessas bibliotecas, tem mais 400 mil "declarações