Uma prova controversa em matemática – que divide o campo há mais de uma década – poderá finalmente ser resolvida por um juiz improvável: um programa de computador. O cerne do debate gira em torno da tentativa de Shinichi Mochizuki de resolver a conjectura ABC em 2012, um problema de longa data profundamente enraizado na natureza fundamental dos números.
A conjectura ABC centra-se numa equação aparentemente simples envolvendo três números inteiros: a + b = c. Ele postula regras específicas que regem como os números primos que compõem esses números inteiros devem se relacionar. Resolver este problema aparentemente básico poderia desbloquear insights profundos sobre a matemática, impactando potencialmente outras conjecturas famosas como o Último Teorema de Fermat.
Mochizuki, professor da Universidade de Kyoto, no Japão, apresentou sua prova dentro de uma estrutura complexa que ele inventou, chamada teoria interuniversal de Teichmüller (IUT). No entanto, o puro tecnicismo e a obscuridade da teoria do IUT tornaram-na em grande parte incompreensível para a maioria dos matemáticos que tentavam verificar o seu trabalho. O entusiasmo inicial deu lugar à frustração enquanto os especialistas lutavam para decifrar as suas complexidades.
Para colocar lenha na fogueira, em 2018, dois proeminentes matemáticos alemães – Peter Scholze e Jakob Stix – identificaram uma falha potencial na prova de Mochizuki. Mochizuki rebateu o seu argumento e, sem um órgão abrangente para arbitrar disputas matemáticas, o campo dividiu-se em dois campos: aqueles que aceitavam em grande parte a visão dominante (apoiada pela maioria dos matemáticos) e um grupo mais pequeno alinhado com Mochizuki e o seu instituto em Quioto.
Agora, Mochizuki propõe um caminho a seguir através da formalização – convertendo sua prova de notação matemática legível por humanos em Lean, uma linguagem de programação de computador projetada especificamente para verificação matemática rigorosa. Este processo poderia potencialmente permitir que os computadores verificassem automaticamente a consistência dos seus argumentos, oferecendo um nível de objectividade sem precedentes.
Mochizuki acredita que o Lean está equipado de forma única para navegar pelos complexos obstáculos linguísticos e conceituais que paralisaram o progresso na compreensão da teoria IUT. Ele a vê como uma ferramenta para libertar a verdade matemática dos potenciais preconceitos inerentes à interpretação humana.
Embora alguns especialistas como Kevin Buzzard, do Imperial College London, considerem esta uma direção promissora, também reconhecem o desafio monumental que temos pela frente. A formalização da teoria IUT exigiria a tradução de vastas extensões de equações intrincadas para a sintaxe Lean – um empreendimento semelhante a alguns dos maiores projetos de formalização já realizados. Esses esforços geralmente envolvem equipes dedicadas de matemáticos e programadores que duram meses ou até anos.
Johan Commelin, da Universidade de Utrecht, na Holanda, embora cautelosamente optimista, sublinha que o sucesso depende do empenho sustentado de Mochizuki. Ele adverte que se o projecto for abandonado prematuramente, poderá simplesmente tornar-se mais um capítulo numa saga prolongada marcada por disputas não resolvidas.
Mesmo que seja bem-sucedido, Commelin salienta que, mesmo com código verificado por computador, poderão persistir divergências sobre a interpretação. O Lean pode resolver contradições lógicas, mas não necessariamente suprimir todas as diferenças filosóficas ou conceituais que cercam o trabalho de Mochizuki.
Em última análise, embora a formalização ofereça um vislumbre de esperança para resolver este impasse matemático duradouro, resta saber se poderá superar as complexidades profundamente arraigadas e as diferentes perspectivas que caracterizaram o debate sobre a prova da conjectura ABC.
