Skip to content

A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.

License

Notifications You must be signed in to change notification settings

pitmonticone/FLT3

 
 

Repository files navigation

Fermat's Last Theorem for Exponent 3

License: Apache 2.0 CI Documentation: Website Blueprint: Website Blueprint: Dependency Graph Blueprint: Paper

This repository contains a formalised proof of Fermat's Last Theorem for the exponent 3 using the Lean 4 interactive proof assistant. It provides both the proof files and a blueprint for a web-based documentation, along with an accompanying paper.

Build Lean Files

To build the Lean files of this project, you need to have a working version of Lean. For comprehensive guidance on installing Lean, see the installation instructions under the section titled "Regular install".

To build the project, run lake exe cache get and then lake build.

Build Blueprint

To build the web version of the blueprint, you need a working LaTeX installation. Furthermore, you need some packages:

sudo apt install graphviz libgraphviz-dev
pip3 install invoke pandoc
cd .. # go to folder where you are happy clone git repos
git clone git@github.com:plastex/plastex
pip3 install ./plastex
git clone git@github.com:PatrickMassot/leanblueprint
pip3 install ./leanblueprint
cd FLT3

To actually build the blueprint, run

lake exe cache get
lake build
inv all

Languages

  • TeX 53.8%
  • Lean 44.0%
  • Python 1.1%
  • CSS 0.4%
  • Shell 0.4%
  • Dockerfile 0.1%
  • Other 0.2%