Theorem Proving in Lean 4

by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the Lean Community

このテキストは読者がLean 4を使うことを前提にしています。Lean 4をインストールするには、Lean 4 Manualの節Quickstartをご覧ください。このテキストの最初のバージョンはLean 2用に書かれました。Lean 3用のバージョンはこちらで入手可能です。

この翻訳について

translated by aconite(2章～12章), Haruhisa Enomoto(1章)

この翻訳は有志による非公式翻訳です。翻訳に際して、表現を大きく変えた箇所や、分かりやすさを期すため記述やコード例を追加した箇所があります。また、用語の訳が一般的でない可能性があります。誤りを含む可能性もあります。必要に応じて原文Theorem Proving in Lean 4 (GitHub)もご覧ください。

原文のライセンスはApache License 2.0であり、それに基づいて原文を翻訳・公開しています。

この翻訳のソースはGitHubリポジトリから入手可能です。また、ページ右上端のGitHubマークを押してGitHubリポジトリに移動することもできます。この翻訳の全ページとソースはApache License 2.0の下で公開されています。

誤字脱字、内容の誤りの指摘、フォークからのPull Request、フォークによる翻訳の改変等は歓迎いたします。基本的に、ご指摘はGitHubリポジトリのIssuesで受け付けます。

翻訳に際して、機械翻訳サービスDeepL翻訳を参考にしました。

バージョン情報

この翻訳は原文のcommit 81b028359684646f2db48e3909ee81b4fad51dfb (Date: Fri Mar 1 14:54:59 2024 -0600)に基づいています。