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
"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 ...
Matérias relacionadas
Pesquisadores desmontaram as baterias da Tesla e da BYD para saber qual delas tem melhor desempenho