Formalizando o Último Teorema de Fermat em Lean: Um Projeto de Código Aberto

Um ambicioso projeto de código aberto visa provar formalmente o Último Teorema de Fermat usando o verificador de teoremas Lean. Liderado por Kevin Buzzard e financiado pela EPSRC, sediado no Imperial College London, o projeto emprega uma variante moderna da prova original de Wiles/Taylor-Wiles, planejada em colaboração com Richard Taylor. O site do projeto fornece detalhes sobre o Último Teorema de Fermat, o verificador Lean, os objetivos do projeto e diretrizes de contribuição.