"Encontrei uma demonstração realmente admirável, mas a margem do livro é muito pequena para colocá-la." Foi o que escreveu o matemático francês do século XVII, Pierre de Fermat, ao enunciar seu "último teorema". O último problema de Fermat levou três décadas para ser encontrado entre artigos do matemático e mais três séculos até que essa admirável prova fosse descoberta.
E mesmo assim, o caso não está completamente resolvido, apenas o desafio é diferente.
O novo desafio é fazer com que um computador prove o teorema elusivo. Esse é o objetivo de um novo projeto, Formalizando Fermat, liderado pelo Imperial College London.
O problema de Fermat
O "Último Teorema" de Fermat postula que, se a, b e c são números naturais e não iguais a zero, a equação aˆn+bˆn=cˆn não tem solução se n for maior que dois. Provar algo formalmente não é tão simples quanto prová-lo por tentativa e erro, e essa prova, complexa demais para a "margem estreita" do caderno de Fermat, ficaria perdida por séculos.
O problema foi resolvido em 1994 pelo britânico Andrew Wiles, que começou a resolver esse quebra-cabeça quando tinha apenas 10 anos de idade. Em 2016, Wiles recebeu o Prêmio Abel, considerado o "Nobel da Matemática".
Quase um milhão de libras
Mais 30 anos após a solução do enigma e mais de três séculos após a morte de Fermat, uma equipe de pesquisadores, liderada por Kevin Buzzard, do Imperial College London, começou a trabalhar para dar um passo adiante, ensinando um computador a resolver o problema.
O novo projeto começou no final de 2024 e durará até 2029. Ele conta com um financiamento de pouco mais de £ 934 mil (R$ 7,05 milhões) e já começa a apresentar alguns resultados, na forma de trechos de código que são adicionados a um banco de dados no GitHub.
O que ainda precisa ser resolvido
Pode parecer contraintuitivo, mas esse tipo de raciocínio que nos leva a provar formalmente teoremas matemáticos é difícil de ensinar a computadores.
Recentemente, Buzzard e outros especialistas explicaram a complexidade do assunto ao jornal francês Le Monde. Para começar, devemos ter em mente que a solução desse teorema é complexa; não é por acaso que várias gerações de matemáticos se esforçaram para encontrá-la.
Esses matemáticos também tinham experiência prévia na resolução desse tipo de problema. Como Buzzard explicou ao jornal francês, os matemáticos têm uma base que lhes permite "pular etapas" ao explicar a solução desse problema. Um computador, no entanto, precisa começar do zero para construir sua própria explicação para o problema.
Tudo isso, para quê?
O Último Teorema de Fermat (...) não tem aplicações, nem teóricas nem práticas, no mundo real", disse Buzzard à revista New Scientist há alguns meses. "Então, por que tanto esforço para ensinar um computador a resolver algo que já resolvemos?" A chave aqui não está no passado, mas no futuro.
De acordo com a equipe que lidera o projeto, os computadores hoje podem ser usados para auxiliar matemáticos na resolução de problemas como a demonstração de teoremas, mas há um obstáculo para a materialização de algumas formas de ajuda.
O problema, eles apontam, é que poucos matemáticos se concentraram em trabalhar com esse software, portanto, não existem ferramentas que contenham as "definições" usadas por matemáticos para resolver esses problemas. Trabalhar neste caso deve servir para criar os bancos de dados necessários para a resolução de problemas semelhantes no futuro.
Imagem | A Aritmética de Diofanto / Pierre de Fermat por Rolland Lefebvre
Ver 0 Comentários