Matemáticos tentam provar por computador o desafio de 350 anos, o 'Último Teorema de Fermat'
(dongascience.com)O Último Teorema de Fermat será provado novamente em linguagem de computador
- O professor Kevin Buzzard, do Imperial College London, pretende escrever a partir de outubro de 2024 uma prova formal do Último Teorema de Fermat (FLT) usando o assistente de provas Lean.
- O Engineering and Physical Sciences Research Council [EPSRC], do Reino Unido, decidiu financiar o professor Buzzard por cinco anos a partir desse mês.
- Um plano de projeto criado com o plugin Lean blueprints para plasTeX deve ser divulgado no fim de abril de 2024.
O Último Teorema de Fermat já não foi provado?
Já foi provado. O matemático britânico Andrew Wiles divulgou a prova em 1994, e ela foi publicada oficialmente em 1995. Mas ainda não existe uma prova formal escrita na linguagem de um provador interativo de teoremas [ITP].
Provador interativo de teoremas? Prova formal? O que é isso?
- Provador interativo de teoremas [ITP]: programa de computador que ajuda pessoas a escrever provas formais. Também é chamado de assistente de provas.
- Prova formal: prova que pode ser verificada por um programa de computador chamado verificador de provas. Em geral, assistentes de provas também fazem o papel de verificadores de provas.
Um provador de teoremas é inteligência artificial?
Um provador neural de teoremas [NTP] pode ser considerado assim, mas muitos provadores interativos de teoremas, incluindo o Lean, não são programas baseados em aprendizado de máquina.
Apresente o assistente de provas Lean.
- É ao mesmo tempo um provador interativo de teoremas e uma linguagem de programação funcional pura.
- Baseia-se em teoria dos tipos dependentes.
- Tem recursos como type classes, sintaxe extensível, macros e metaprogramação.
- Em comparação com outros assistentes de provas, a base de usuários do Lean inclui particularmente muitos matemáticos (de áreas fora dos fundamentos da matemática).
Por que querem escrever uma prova formal do Último Teorema de Fermat?
Citando um post no X do professor Kevin Buzzard: “Para fazer o computador entender a teoria moderna dos números e, no fim das contas, conseguir ajudar os teóricos dos números.”
Links
- Mensagem publicada pelo professor Kevin Buzzard no chat Zulip do Lean em 3 de outubro de 2023: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/…
- Biblioteca matemática do Lean: https://github.com/leanprover-community/mathlib4
- Artigo da New Scientist: https://institutions.newscientist.com/article/…
- Artigo da Popular Mechanics: https://popularmechanics.com/science/math/…
1 comentários
Torço por isso. Para quem tem interesse em provas formais, também recomendo assistir à aula Machine Assisted Proofs do professor Terrence Tao (https://www.youtube.com/watch?v=AayZuuDDKP0).