Uma equipa de investigadores quer criar uma prova verificada por computador do Último Teorema de Fermat, um problema que tem intrigado e confundido a comunidade matemática desde a sua formulação, no século XVII, por Pierre de Fermat.
Esta iniciativa tem como objetivo não só solidificar a exatidão da prova sem margem para dúvidas, mas também ser pioneira de uma nova era em que as provas matemáticas são examinadas e validadas pela lógica infalível dos computadores.
O Último Teorema de Fermat, uma afirmação de que três inteiros positivos a, b e c não podem satisfazer a equação an + bn = cn para qualquer valor inteiro de n superior a 2, permaneceu um enigma durante mais de 350 anos.
Foi apenas em 1993 que Andrew Wiles apresentou uma prova que cativou o mundo da matemática.
A prova de Wiles, com mais de cem páginas, levou mais de dois anos de revisão por pares para ser verificada devido à sua complexidade e aos conceitos matemáticos avançados que empregava.
O projeto atual, liderado por Kevin Buzzard, do Imperial College de Londres, não é apenas uma tentativa de digitalizar a prova histórica de Wiles. Representa um passo fundamental para o futuro da matemática, em que as provas são codificadas num formato legível por computador usando uma linguagem de programação conhecida como Lean.
Esta metodologia, explica a revista New Scientist, permite a deteção instantânea de erros lógicos e pode potencialmente permitir que os computadores utilizem estes teoremas como base para outras provas.
No entanto, a jornada para formalizar uma prova tão importante está repleta de desafios. Grande parte da matemática contemporânea que está na base da prova de Wiles ainda não foi traduzida numa forma que os computadores possam interpretar. Apesar destes obstáculos, Buzzard e a sua equipa estão motivados.
Para além de provar o Último Teorema de Fermat, o seu esforço pode tornar uma vasta gama de conceitos matemáticos mais acessíveis à análise computacional, acelerando assim o ritmo da investigação e descoberta matemática.
A equipa planeia seguir de perto a estrutura da prova de Wiles, com pequenos ajustes, e pretende fazer do projeto um esforço de colaboração, envolvendo a comunidade Lean.
Apesar da natureza ambiciosa do projeto e do grande dispêndio de tempo – com Buzzard a dedicar cinco anos a este empreendimento, suspendendo as suas funções de professor – a comunidade matemática assiste com expetativa.
