Prova do Último Teorema de Fermat: Computadores Enfrentam um Desafio Matemático
2024-12-12
Uma equipe está tentando provar o Último Teorema de Fermat usando Lean, encontrando desafios inesperados no caminho. Em vez de depender da prova original, eles estão usando uma abordagem moderna mais generalizada. Ao formalizar a cohomologia cristalina, descobriram um erro em um lema-chave, levando a uma reavaliação dos fundamentos da teoria. Eles finalmente encontraram uma solução alternativa usando uma prova diferente. Essa experiência destaca erros potenciais na literatura matemática moderna e sublinha a necessidade de provas formalizadas.