話題の証明支援システム LEANについての本やサイトの紹介です。
望月先生のABC予想の証明の正しさをチェックするプロジェクトが使っているLEANについての本が評判になっています。The Proof in the Codeという本です。
https://www.quantabooks.org/books/the-proof-in-the-code/
もともとLEANはMicrosoftのLeo de Mouraによって開発されたプログラムです。Microsoft WordやWindowsなどのプログラムのコードにバグがないか、セキュリティ脆弱性がないか、そして設計どおりに動作するかをチェックするプログラムとして開発されました。LEANはあまり使われていなかったようですが、数学者がこれが数学の証明のチェックに使えるのに気付き、現在の証明支援システムに育て上げたのだそうです。ものすごく面白い本のようで多くの人の賛辞が上のサイトにのっています。
このLEANの公式サイトはこちらです。https://lean-lang.org/
無料のエディタであるVS Codeの機能拡張としてインストールしてセットアップして使うようです。
日本語で参考になるサイトがありました。
https://aconite-ac.github.io/
こちらはLEAN関連の、日本語の情報を中心にまとめてくださっているサイトです。ご自身の哲学探究サイト『束跡』をホストしているサイトでもあるのでとても興味のもてる内容のようです。LEAN関係の部分を以下に引用しておきます。
・Theorem Proving in Lean 4 日本語訳 : Leanのチュートリアルドキュメント「Theorem Proving in Lean 4」の非公式日本語訳です。
・Leanのインストール方法・elanとLakeの使い方 : Leanのインストール方法・elanとLakeの使い方をまとめた非公式資料です。
外部リンク
日本語情報
LEAN JA : Lean言語の日本語コミュニティです。豊富なリンク集が掲載されています。Discordサーバーもあります。
Lean by Example : LEAN JA管理者の北窓氏による、Lean言語とその主要なライブラリの使い方を豊富なコード例とともに解説した日本語資料です。
英語情報もまとまっているので役立ちます。是非参考になさってください。