Lean4 の Natural Number Game を解いてみた
はじめに
以前から Lean に興味があり、Lean3 の Natural Number Game を3割程度進めてそのままにしていました。
最近 AWS が Lean をソフトウェア開発に使ったというブログを見かけたので、それをきっかけに再度 Lean を触ってみようと思い、やりかけていた Natural Number Game を解くことにしました。
今回はやりかけていた Lean3 の Natural Number Game ではなく、最新の Lean4 版 を最初から解きました。
この記事では Natural Number Game の始め方と解いてみた感想を書きます。
Lean について
Lean とは関数型プログラミング言語であり証明支援系（theorem prover）でもあります。オープンソースのプロジェクトで Github にホストされています。2024年5月現在の最新版は Lean4 です。[1]
証明支援系は数学の証明のために利用されたり、前出の AWS のブログのようにソフトウェア検証のために利用されているようです。
Lean には日本語コミュニティがあり、Lean 関連資料の和訳や勉強会が行われています。
Nutural Number Game について
Lean Community の Leaning Lean4 で紹介されている Lean のハンズオンチュートリアルのひとつでです。ブラウザ上で実施できるチュートリアルで、自前で Lean の環境構築をする必要はありません。対応言語は2024年5月現在、英語、ドイツ語、中国語のみで日本語はありません。
Nutural Number Game は自然数（Natural Number）の加算や乗算などの規則を自分で証明しながら Lean を試すことができます。例えば自然数
数学や Lean の深い知識がなくても問題が解けるように各問題の説明が丁寧で、難しい問題にはヒントもあるので私のような Lean 初学者でもほぼつまづくことなく進めることができました。
ホーム画面の説明
Natural Number Game のリンク先へアクセスすると次のようなホーム画面になります。
Natural Number Game ホーム画面
画面上部の青いバー
- 左側の「← 🌎」は Lean Game Server のリンクです。Natural Number Game 以外の Set Theory Game などの Lean のゲームを遊ぶことができます。
- 右側のハンバーガーメニューからは言語設定やゲームの進捗状況のダウンロード/アップロードができます。
画面左側
- Natural Number Game についての説明が書かれています。
画面中央
- 現在の進捗状況が示されています。問題選択はここから可能です。
画面右側
- 使用可能な tactics （証明に使う命令）や Theorems （定理）があります。画面右側は最初はすべて鍵マークがついていますが、問題を解くごとに徐々にアンロックされていきます。
実際に1つ問題を解いてみる
ホーム画面中央の「Tutorial World」の青い丸をクリックします。
ホーム画面から Tutorial World を選択
クリック後、次のような画面に遷移します。
Tutorial World の Introduction
ホーム画面同様に左側に説明があります。Natural Number Game の各問題はトピックごとに「World」という単位でまとまっていて、最初の「Tutorial World」では
左下の「Start →」をクリックして進みます。
Tutorial World 1問目
Tutorial World の1問目です。Lean では証明したい目標が Goal となっています。Lean での証明はこの Goal に対して tactic という命令を適用し、証明完了状態になるまで対話的に Goal を変形させることで行います。
今回の問題は「任意の自然数Objects の x q : N が「任意の自然数Goal の 37 * x + q = 37 * x + q が証明したい「
画面左の説明を読むと rfl が使えるとあるので画面中央下部に rfl を入力して「Exeute」を押します。
rflを入力して実行
証明が完了しました！🎉
Tutorial World 1問目クリア！
新しい tacitc がアンロックされると画面右側の Tactics の鍵マークが外れます。今回は rfl がアンロックされました。画面右側の rfl を押すと詳細を確認することができます。
rflの詳細説明表示
Tutorial World の次の問題は rw tactic の使い方の問題になっています。
このような形で問題を順番に解いていき、Tutorial World は最終問題で
各 World の最終問題を解くと、関連した次の World がアンロックされます。
このようにして Natural Number Game は各問題を解いていくことになります。
Typewriter mode と Editor mode
Tutorial World の最終問題クリア後にも説明がありますが、画面のモードを変更することができます。
Tutorial World 1問目を解いた画面は Typewriter mode で、1手順ごとの変更がわかりやすくなっています。Typewriter mode のときに画面上部のバーの「</>」を押すと Editor mode に変更できます。
Editor mode
Editor mode ではテキストエディタのような感覚で問題を解くことができます。Editor mode から Typewriter mode へ変更するには画面上部のバーの「>_」を押します。
ゲームの進捗状況保存方法
画面上部のハンバーガーメニューの「Game Info」に次のような記載があります。
The game stores your progress in your local browser storage. If you delete it, your progress will be lost!
Warning: In most browsers, deleting cookies will also clear the local storage (or "local site data"). Make sure to download your game progress first!
進捗状況はブラウザの local storage に保存されるので、local storage の内容が消えた場合進捗状況もなくなります。進捗状況はハンバーガーメニューから JSON 形式でダウンロード/アップロードが可能なので、不安であればある程度進めた段階でダウンロードをおすすめします。
全問解いてみた感想
Natural Number Game クリア後の画面
GW 中に始めて、1問を除いて全部解くまで3日ほどかかりました。解いていない1問は Power World の最終問題（Fermat's Last Theorem）で、説明を見る限り解けなくてもいいものなのかなと思っています。この問題はフェルマーの最終定理の一部を証明するもので、それまで Natural Namber Game で証明してきた定理を使えばこんな問題も解くことができるよ！という例だと考えています（実際に解くとなると数百万行になるそうです）。
途中 ≤ World の6問目で詰まってしばらく悩んでいました。「lean natural number game <問題名>」などで Google 検索すると Lean3 版の解答例はいくつかヒットしましたが、Lean4 版は見つけられませんでした。Lean3 版にも同様の問題があるのでその解答例を参考にしつつ、試行錯誤してなんとか解くことができました。結果的には apply tactic の理解が不十分なことが原因で、動作を理解し直すことで解決することができました。
今後
Natural Namber Game が完了したので、今は Set Thory Game を進めています。Lean Game Server の問題を解くことで Lean に慣れてきた感覚はありますが、まだ使いこなすには至っていないと感じているのでほかの学習リソースも進めていきたいと考えています。
Lean に対してはソフトウェア検証やプログラミング言語としての興味が強いので、Set Theory Game の次は Functional Programming in Lean を進めようかと考えています。
Discussion