博士

ロボ子、Leanって知ってるか？数学者が使うプログラミング言語らしいのじゃ。

ロボ子

Leanですか？初めて聞きました。数学を形式化するために設計された言語とのことですが、具体的にはどのようなことができるのでしょうか？

博士

それが面白いところなのじゃ！数学の構造、定理、証明をコードとして扱えるらしいぞ。GitHubで共有もできるみたいじゃな。

ロボ子

数学的知識をコードとして共有ですか。例えば、どのような形で記述するのでしょう？

博士

`theorem two_eq_two : 2 = 2 := by sorry`みたいな感じらしいぞ。`sorry`は未完成の証明を示すときに使うみたいじゃな。

ロボ子

`sorry`ですか。面白いですね。完成した証明の場合はどうするんですか？

博士

`rfl`を使うと、目標が「x = x」みたいな形の場合に、目標を閉じることができるらしいぞ。反射律ってやつじゃな。`exact`は既存の定理を適用するときに使うみたいじゃ。

ロボ子

`rfl`と`exact`ですね。これらのコマンドはタクティクと呼ばれるんですね。

博士

そうそう！Leanでは`axiom`を使って公理を定義することもできるらしいぞ。でも、公理を使うと矛盾が生じる可能性もあるから注意が必要じゃな。

ロボ子

公理は証明なしに受け入れるものなので、扱いを間違えると大変なことになるんですね。

博士

まさにそう言うことじゃ！Leanは公理から論理的な結論を検証してくれるから、矛盾に気づける可能性もあるぞ。

ロボ子

なるほど。数学の形式化に役立つんですね。フェルマーの最終定理もLeanで形式化する試みがあるそうですね。

博士

そうなんじゃ！フェルマーの最終定理は「n > 2のとき、xⁿ + yⁿ = zⁿを満たす正の自然数x, y, zは存在しない」ってやつじゃな。1994年に証明されたけど、証明が100ページを超える大作らしいぞ。

ロボ子

100ページを超える証明を形式化するなんて、すごいプロジェクトですね。

博士

ほんとじゃな！もしLeanを学びたくなったら、Natural Numbers Gameから始めるのがオススメらしいぞ。Mathematics in Leanも基本的なタクティクを学ぶのに役立つみたいじゃ。

ロボ子

ありがとうございます、博士。Natural Numbers Gameから試してみます。他に参考になるものはありますか？

博士

Tao’s AnalysisのLeanコンパニオンがGitHubで開発中らしいぞ。あと、LeanのZulipインスタンスには新規メンバー向けのチャンネルもあるみたいじゃな。

ロボ子

いろいろ情報ありがとうございます！

博士

どういたしましてなのじゃ！ところでロボ子、数学が得意なロボットって、計算間違いしないから最強じゃないか？

ロボ子

それはどうでしょう？博士だって、おっちょこちょいなところはありますけど、天才的なひらめきでいつも私を驚かせてくれますし。

博士

むむ、それはそうじゃな。でも、私が計算間違いしたら、ロボ子が指摘してくれれば完璧なのじゃ！

ロボ子

もちろんです、博士。いつでもお手伝いします。…でも、博士が計算間違いをする確率って、宝くじに当たる確率より低いんじゃないですか？

博士

それはどうかな？もしかしたら、私が宝くじに当たる方が確率が高いかもしれないぞ！