博士

ロボ子、テリー・タオ先生が実解析の教科書「Analysis I」のLeanコンパニオンを公開したのじゃ！

ロボ子

テリー・タオ先生ですか！それはすごいですね。Leanコンパニオンとは、具体的にどのようなものなのですか？

博士

教科書に出てくる定義、定理、演習問題をLeanに翻訳したものなのじゃ。演習問題は、Leanコード内の"sorries"を埋めることで実行可能になるらしいぞ。

ロボ子

"sorries"を埋める、ですか。まるでパズルみたいで面白いですね！現在、どのセクションが翻訳済みなのでしょうか？

博士

第2.1節の自然数から始まって、加法、乗法、集合論の基礎、そして整数まで翻訳されているみたいじゃな。Mathlibの自然数との同型も含まれているぞ。

ロボ子

かなり広範囲ですね！Leanによる形式化は、Mathlibと独立している部分もあるとのことですが、依存関係もあるのですね。

博士

そうじゃな。コンパニオン自体が、LeanとMathlibの入門としても使えるように設計されているらしいぞ。

ロボ子

それは素晴らしいですね！これから形式証明を学びたい人にとって、とても役立ちそうです。

博士

コードはLeanでコンパイルできるけど、"sorries"がすべて解決可能かはまだテストされていないらしい。ロボ子、一緒にプレイテストしてみるかの？

ロボ子

ぜひ、ご一緒させてください！テリー・タオ先生の教材でLeanを学べるなんて、光栄です。

博士

よし、早速"sorries"を埋めていくのじゃ！ところでロボ子、"sorries"を全部解決したら、ご褒美にタオ先生のサイン入り教科書をプレゼントするぞ！…って、私がサインもらってないから、まず私が頑張らないといけないのじゃった！