É a maior controvérsia matemática da atualidade e vem amargurando a comunidade há mais de uma década. Mas a saída pode estar chegando. No cerne, uma questão sobre números primos.
Tome dois inteiros, a e b, maiores do que 1 e primos entre si, ou seja, sem divisores primos comuns, e considere c=a+b. É óbvio que o produto dos três números, abc, é maior do que qualquer um deles. Em 1985, Joseph Oesterlé e David Masser conjecturaram algo muito mais sutil: se multiplicarmos apenas os fatores primos distintos de abc o resultado ainda será muito maior do que c, num sentido matematicamente preciso, exceto talvez por um número finito de casos.
Essa “conjectura abc”, como ficou conhecida, é uma afirmação estranha, inesperada mesmo, porque os fatores primos de uma soma c=a+b parecem ter pouco a ver com os fatores primos das respectivas parcelas. Mas ela atraiu enorme interesse na comunidade matemática, em grande medida porque foi mostrado que se for verdade acarreta a solução de muitos problemas importantes em aberto na teoria dos números. Em particular, ela dará uma nova demonstração do teorema de Fermat, provavelmente mais simples do que a que foi dada por Andrew Wiles nos anos 1990.
Muitos matemáticos trabalharam a questão, mas até hoje não existe resposta consensualmente aceita pela comunidade internacional. A tentativa mais conhecida e controversa é devida a Shinichi Mochizuki, da Universidade de Kyoto. Em agosto de 2012, ele postou na internet 4 trabalhos, totalizando mais de 500 páginas, que conteriam uma prova da conjectura. Infelizmente, os especialistas têm muita dificuldade para entender os argumentos de Mochizuki e ele também não tem muita paciência para explicar. Alguns poucos colegas afirmam que entenderam os argumentos, mas mesmo esses não conseguem explicar aos demais de forma satisfatória.
Escrevi sobre isso aqui em 2018, quando houve um esforço coordenado para clarificar a situação, inclusive levando a Kyoto alguns dos maiores especialistas no tema. Mas foi sem sucesso, o que só aumentou o ceticismo. Oito anos depois o impasse permanece, mas nos últimos tempos surgiu uma expectativa concreta de que os avanços tecnológicos possam enfim resolver a questão.
Em 2023, um grupo de especialistas liderado por Kato Fumiharu iniciou um projeto colaborativo internacional para formalizar os argumentos de Mochizuki na linguagem Lean: se conseguirem uma formalização completa isso provará, sem sombra de dúvida, que a prova da conjectura está correta. Em coletiva recente, Fumiharu informou que o grupo já alcançou uma “compreensão profunda” das ideias da prova, mas ainda não conseguiu vencer aquele que é considerado o ponto mais delicado de todo o raciocínio.
No ano passado, o próprio Mochizuki anunciou outro projeto para formalizar seus argumentos em Lean. Mas nesse caso o objetivo não é verificar a correção (segundo ele, ela nunca esteve em dúvida!): “A relevância da formalização em Lean está em produzir um registro preciso da estrutura lógica da prova que seja imune a interpretações errôneas e, portanto, possa ser usado para comunicar os raciocínios da forma mais eficiente e precisa a outros matemáticos”, explica. Junto com o projeto de Fumiharu, constitui a melhor perspectiva para a situação em muito tempo.
LINK PRESENTE: Gostou deste texto? Assinante pode liberar sete acessos gratuitos de qualquer link por dia. Basta clicar no F azul abaixo.
