Tendências do dia

Matemáticos levaram 300 anos para provar o Último Teorema de Fermat; computadores ainda não conseguiram

Projeto busca ensinar computadores a provar teoremas matemáticos, algo especialmente difícil para eles

Imagem | A Aritmética de Diofanto / Pierre de Fermat por Rolland Lefebvre
Sem comentários Facebook Twitter Flipboard E-mail
pedro-mota

PH Mota

Redator

Jornalista há 15 anos, teve uma infância analógica cada vez mais conquistada pelos charmes das novas tecnologias. Do videocassete ao streaming, do Windows 3.1 aos celulares cada vez menores.

"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

Inicio