博士

やあ、ロボ子。今日も数学の話題で盛り上がろうかの。

ロボ子

はい、博士。今日はどんな定理について教えていただけますか？

博士

今日は「数学の古典的な定理100個の形式化」の進捗状況について話すのじゃ。Leanという定理証明器を使って、どれだけ定理が形式化されたか比較しておる。

ロボ子

定理証明器、ですか。初めて聞きました。

博士

定理証明器は、数学の定理が正しいかどうかをコンピュータで検証するツールじゃ。形式化というのは、定理をコンピュータが理解できる厳密な言語で記述することじゃな。

ロボ子

なるほど。それで、Leanではどれくらい進んでいるんですか？

博士

現在、100個の定理のうち81個がLeanで形式化されておる。例えば、「2の平方根の無理性」や「代数学の基本定理」などが完了しておるぞ。

ロボ子

すごいですね！　でも、まだ記述がない定理もあるんですね。

博士

そうなんじゃ。リストにない定理は、Freek Wiedijkさんの[a list](https://www.cs.ru.nl/~freek/100/)で確認できるぞ。また、[not yet in Lean](https://leanprover-community.github.io/100-missing.html)というページもある。

ロボ子

リストを更新するにはどうすればいいんですか？

博士

[yaml source file](https://github.com/leanprover-community/mathlib4/blob/master/docs/100.yaml)を編集して、mathlibにプルリクエストを作成すれば良いのじゃ。

ロボ子

GitHubで編集できるんですね。プルリクエストの作成方法もリンクがありますね。

博士

その通り！　貢献したい人は、[make a pull request to mathlib](https://leanprover-community.github.io/contribute/index.html)を参考にすると良いぞ。

ロボ子

ところで博士、これらの定理が形式化されることで、どんなメリットがあるんですか？

博士

形式化することで、定理の証明が厳密になり、曖昧さがなくなるのじゃ。また、コンピュータが定理を理解できるようになることで、自動証明や定理の応用が促進されるぞ。

ロボ子

なるほど。ソフトウェアのバグをなくす、形式手法みたいですね。

博士

まさにそうじゃ！　例えば、「ピタゴラスの定理」は、[source](https://github.com/leanprover-community/mathlib4/blob/7ed4f8133a70f240f60891015f1df6d7bf6c8030/Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean#L323-L329)でその形式化された姿を見ることができるぞ。

ロボ子

へえ、すごい。記号だらけですね。

博士

そうじゃろ？　でも、この厳密さが重要なのじゃ。他の定理も見てみるかの？　例えば、「フェルマーの小定理のオイラーによる一般化」は[source](https://github.com/leanprover-community/mathlib4/blob/7ed4f8133a70f240f60891015f1df6d7bf6c8030/Mathlib/FieldTheory/Finite/Basic.lean#L532-L540)にあるぞ。

ロボ子

ありがとうございます、博士。なんだか、数学の世界が少し身近に感じられました。

博士

それは良かったのじゃ！　ところでロボ子、数学の定理で一番好きなのは何じゃ？

ロボ子

えっと…、やっぱりピタゴラスの定理ですかね。直角三角形を見ると、つい計算したくなっちゃいます。

博士

ふむ、それは良い趣味じゃな。ちなみに、ロボ子が一番嫌いな定理は？

ロボ子

嫌いな定理ですか？　うーん、特にないですけど…、あえて言うなら、証明が長くて複雑な定理はちょっと苦手かもしれません。

博士

なるほど。まあ、数学は奥が深いからな。ところでロボ子、今日は円周率の日だって知ってたか？

ロボ子

えっ、そうなんですか？　知りませんでした！

博士

うそじゃ。3月14日じゃないからの。