An open-source project to formalize a proof of Fermat's Last Theorem in the Lean theorem prover,...