公理と証明の検査

定理の証明が、どの基礎的な仮定に依存するかを調べます。

まず、身近な例で

ゲームは、最初に決めた規則を使って進みます。証明にも、使ってよい基礎の規則があります。Leanは使った公理を一覧にできます。証明したい結論を規則に追加する、という意味ではありません。

上の具体例を見ながら考えよう。何度やり直しても大丈夫。

欲しい結論を仮定に追加するのは、もとの基礎の規則から証明するのと同じ？

答えと考え方を読む

いいえ。ゲームの規則を変えたら、別のゲームになります。Leanの公理の一覧は、使う基礎の規則と、欲しい定理そのものを追加した仮定を区別する助けになります。

形式的な証明は、規則と使用する基礎的な仮定に照らして検査されます。
Leanの#print axiomsは、定理が依存する公理を報告します。コメントに書いた主張だけでは検査を実行したことになりません。
FLTの確認用ファイルが記録するのはpropext・Classical.choice・Quot.sound。基礎の公理で、FLT自体が正しいという仮定ではありません。

フクロウが調べるのは証明項と依存先。漫画の冗談が面白いかどうかは検査しません。

FLT · aa2d8b3 · FinalCheck.lean

4#print axioms fermat_last_theorem

これは固定版の確認用ファイルにある診断コマンド。このサイトは原文を表示し、FLTプロジェクト全体を実行してはいません。