Uma disputa de uma década em matemática sobre a prova da conjectura ABC de Shinichi Mochizuki pode ser resolvida usando formalização computacional. Mochizuki sugeriu traduzir seu trabalho de 500 páginas para a linguagem de programação Lean para verificação automatizada. Essa abordagem poderia unir divisões entre campos conflitantes na comunidade matemática.
A controvérsia remonta a 2012, quando Shinichi Mochizuki, professor da Universidade de Kyoto no Japão, publicou uma prova extensa de 500 páginas para a conjectura ABC. Esse problema de 40 anos diz respeito à equação a + b = c para inteiros completos e às relações entre seus fatores primos, com implicações para teoremas como o Último Teorema de Fermat. A prova de Mochizuki depende de sua intrincada teoria de Teichmüller inter-universal (IUT), que muitos especialistas acharam difícil de penetrar.
O entusiasmo inicial diminuiu à medida que os esforços de verificação pararam. Em 2018, Peter Scholze da Universidade de Bonn e Jakob Stix da Universidade Goethe de Frankfurt identificaram uma falha potencial, que Mochizuki contestou. Sem uma autoridade central, o mundo da matemática se dividiu: a maioria dos matemáticos de um lado, e um grupo menor afiliado a Mochizuki e ao Instituto de Pesquisa em Ciências Matemáticas de Kyoto do outro.
Para romper o impasse, Mochizuki agora defende a formalização da prova em Lean, uma linguagem para matemática verificada por computador. Inspirado por uma conferência em julho em Tóquio, ele argumenta em um relatório recente que o Lean poderia libertar a verdade matemática das "dinâmicas sociais e políticas." Como ele escreve, “[Lean] é a melhor e talvez a única tecnologia… para alcançar progresso significativo em relação ao objetivo fundamental de libertar a verdade matemática do jugo das dinâmicas sociais e políticas.”
Especialistas veem promessa, mas com cautela. Kevin Buzzard do Imperial College London observa: “Se estiver escrito em Lean, então não é loucura, certo? Muita coisa nos artigos é escrita em uma linguagem muito estranha, mas se você puder escrevê-la em Lean, isso significa que pelo menos essa linguagem estranha se tornou algo completamente bem definido.” Johan Commelin da Universidade de Utrecht adiciona: “Queremos entender o porquê [da IUT], e temos esperado por isso há mais de 10 anos. O Lean poderia nos ajudar a entender essas respostas.”
No entanto, a tarefa é imensa, exigindo equipes de especialistas e possivelmente anos de trabalho. Mesmo o sucesso pode não encerrar debates sobre interpretação, pois Mochizuki reconhece que o Lean não oferece uma "cura mágica" para questões sociais. Buzzard permanece otimista: “Você não pode discutir com o software.”