O alemão Peter Scholze, que ganhou a medalha Fields, prêmio mais importante da matemática, aqui no Rio de Janeiro em 2018, com apenas 31 anos (!), é amplamente considerado um dos mais brilhantes matemáticos de nossos dias. Mas em 2020 ele estava numa situação delicada: um de seus principais teoremas, peça-chave de sua teoria dos espaços vetoriais líquidos, tinha uma prova tão sutil e intrincada que nem os revisores nem o próprio Scholze conseguiam ter certeza de que estivesse certa.
A reação dele foi inusitada: em dezembro daquele ano, Scholze publicou um convite aberto à comunidade científica para que sua prova fosse verificada formalmente por meio de computador. Inclusive, ofereceu um prêmio pela verificação, acrescentando que ficaria aliviadíssimo se ela pudesse ser realizada. Um grupo de especialistas respondeu ao desafio, lançando o que ficou conhecido como o “experimento do tensor líquido”.
A ferramenta mais usada na verificação formal de argumentos matemáticos é a linguagem de programação Lean, criada em 2013 pelo brasileiro Leonardo de Moura, pesquisador da Microsoft Research. Originalmente, foi concebida como um meio para conferir automaticamente programas de computador, ou seja, detectar possíveis “bugs” (erros) diretamente no código sem precisar rodar o programa.
Acontece que um programa de computador e uma prova matemática são essencialmente a mesma coisa. Esse é um princípio da ciência da computação que tem até nome: correspondência de Curry–Howard, em homenagem aos pesquisadores norte-americanos Haskell Curry (1900 – 1982) e William Howard (n. 1926). Assim, Lean se converteu também num meio para detectar, de modo automático, erros em raciocínios matemáticos.
Simplificando um pouco as coisas, a ideia é transcrever os raciocínios para a linguagem Lean e, em seguida, fazer o computador rodar o código obtido dessa forma. Lean atua como um revisor implacável e infalível, que não deixa passar a menor incorreção lógica. Se o código rodar até o final, é porque a prova está formalmente correta.
Foi isso que o grupo do experimento do tensor líquido fez para o teorema de Scholze. Desse modo, em junho de 2021, eles já tinham conseguido validar o passo mais difícil da prova, levando a Quanta Magazine, um dos melhores meios de divulgação científica da atualidade, a proclamar que “os verificadores de provas entraram para a primeira divisão da matemática”. Os trabalhos do grupo foram completados oficialmente um ano depois, com pleno sucesso: os argumentos de Scholze foram totalmente validados.
Foi a primeira vez que um teorema na fronteira do conhecimento teve sua prova validada formalmente desse modo. E o fato de o próprio autor, um matemático do nível de Scholze, ter reconhecido sua insegurança quanto à prova conferiu ao projeto uma dimensão especial, apontando que assistentes computacionais se tornaram importantes ferramentas da pesquisa matemática, mesmo quando realizada por humanos.
Mas transcrever linguagem matemática para Lean é difícil e demorado. Em janeiro de 2024, o não menos brilhante Terence Tao, também ganhador da medalha Fields, lançou outro desafio ainda maior: verificar formalmente a prova do clássico Teorema dos Números Primos. Será a continuação, na semana que vem.
Fonte ==> Folha SP – TEC
