フェルマーの最終定理の証明は関数

では ∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0 の証明とはどのようなものでしょうか？この命題には矢印が含まれているので，フェルマーの最終定理のステートメントは $\mathrm{Hom}(A,B)$ という形の集合の一種です．Lean では，フェルマーの最終定理の証明は実際に関数です！その関数が何をするかは次の通りです．それは４つの入力を持ちます．最初の３つの入力は自然数 x, y, z です．４番目の入力は証明で，命題 n > 2 ∧ x^n + y^n = z^n の証明です．そして出力は命題 x*y=0 の証明です．これは「フェルマーの最終定理の証明とは何か」という問いについてのきわめて型破りな考え方であり，証明を実際に理解しようとする際には全く役に立たないことを強調しておきましょう． ―― しかし，これは数学がどのように機能するかについての完全に一貫したメンタルモデルです．数と証明の概念を統一することで，―― つまり両方を項として考えることで，―― 証明を関数として考えることができます．Lean は関数型プログラミング言語であり，特に関数を中心に設計されています．現在 Lean や Coq や Isabelle/HOL といった型理論を使用する証明支援系が，Metamath や Mizar のような集合論を使用する証明支援系より進んでいるのは，このためだと私は確信しています．

定理を証明しましょう！関数を書きましょう！