Dois projetos inovadores estão empregando programas de computador para tentar resolver um dos debates mais intensos da matemática contemporânea, centrado na Conjectura ABC.
Um desses projetos, mantido em sigilo por mais de dois anos, reflete a esperança de matemáticos de que a controvérsia possa finalmente chegar a uma conclusão.
Esses esforços representam um avanço significativo na busca por clareza sobre uma questão que desafia a comunidade científica há mais de uma década.
A controvérsia teve início em 2012, quando Shinichi Mochizuki, da Universidade de Kyoto, no Japão, anunciou ter provado a Conjectura ABC, uma proposição que explora a relação entre números primos na equação a + b = c.
Mochizuki publicou uma prova de 500 páginas online, introduzindo conceitos inéditos por meio de sua Teoria Inter-universal de Teichmüller (IUT).
Apesar da relevância do trabalho, a complexidade da prova dificultou sua aceitação. Muitos matemáticos, mesmo após meses de análise e diálogos diretos com Mochizuki, não conseguiram validar os resultados, gerando um impasse na comunidade acadêmica.
Em 2018, a situação se agravou quando Peter Scholze, da Universidade de Bonn, e Jakob Stix, da Universidade Goethe de Frankfurt, ambos na Alemanha, apontaram um possível erro na prova.
Enquanto Mochizuki e um grupo restrito de colaboradores, majoritariamente da Universidade de Kyoto, defenderam a validade do trabalho, grande parte da comunidade matemática considerou a prova, no mínimo, incompreensível, ou, no pior cenário, incorreta.
Esse embate paralisou os avanços por anos, até que novos caminhos começaram a surgir.
Em 2025, Mochizuki destacou a importância da formalização matemática, um campo que traduz provas em linguagens computacionais para verificação automática de sua correção.
Ele apontou a linguagem Lean como uma ferramenta crucial, descrevendo-a como a mais promissora para superar barreiras sociais e políticas na validação da verdade matemática.
Esse posicionamento abriu portas para iniciativas que agora tentam formalizar sua prova da Conjectura ABC utilizando essa tecnologia, conforme relatado por fontes especializadas.
Atualmente, dois grupos distintos trabalham nesse desafio. Um deles, liderado por Kato Fumiharu, do Centro de Matemática ZEN, no Japão, deu início ao projeto Lean e Geometria Anabeliana (LANA) no final de 2023.
Fumiharu reuniu matemáticos familiarizados com a obra de Mochizuki e especialistas em Lean, incluindo Adam Topaz, da Universidade de Alberta, no Canadá.
O objetivo central é esclarecer de forma definitiva os pontos controversos da prova. Em uma conferência de imprensa realizada em março de 2026, Fumiharu revelou que sua equipe alcançou uma compreensão aprofundada de aspectos da teoria de Mochizuki, mas enfrenta dificuldades em um ponto específico da IUT — o mesmo identificado por Scholze e Stix em 2018 como potencialmente problemático.
Topaz admitiu que, mesmo após workshops e contatos indiretos com Mochizuki, o progresso nesse aspecto permanece estagnado.
Paralelamente, Mochizuki e sua equipe também iniciaram um projeto de formalização em Lean, mas com um enfoque diferente.
Em um evento acadêmico realizado em janeiro de 2026 na Universidade de Exeter, no Reino Unido, Mochizuki esclareceu que seu interesse não está na validação da prova — que ele considera já correta —, mas na comunicação precisa de sua estrutura lógica.
Ele destacou que a formalização pode evitar interpretações errôneas e facilitar o entendimento por outros matemáticos.
Sua equipe começou a trabalhar na área mais controversa da prova, produzindo inicialmente 70 linhas de código em Lean, embora o material ainda não tenha sido divulgado publicamente.
Kevin Buzzard, do Imperial College London, ponderou que esse volume de código é insuficiente para uma prova de tal magnitude, mas reconheceu o movimento como um dos mais relevantes desde o anúncio original de Mochizuki.
Apesar dos obstáculos, há otimismo entre os envolvidos. Topaz enfatizou que o diálogo estabelecido com o grupo de Mochizuki, mediado pela tecnologia Lean, alimenta esperanças de uma resolução.
A troca de ideias entre os projetos, ainda que independentes, sinaliza um progresso notável em um campo que permaneceu estagnado por anos.
Para a comunidade matemática, esses esforços representam uma oportunidade de superar barreiras históricas e alcançar um consenso sobre a validade da Conjectura ABC.
Com informações de newscientist.com.
Nenhum comentário ainda, seja o primeiro!