公開2025.09.03更新2026.10.13 107 人が閲覧（直近 30 日）プログラミング言語

Lean4とは？入門・インストールからMathlib4・VSCode設定、最初の証明まで

Lean4は、数学の定理やプログラムの性質を形式的に書き、その証明が正しいかをコンピュータに検査させる定理証明支援系です。同時に、ネイティブコードへコンパイルできる関数型プログラミング言語でもあります。最新安定版は2026年10月12日公開のLean 4.35.0です。

この記事では、ブラウザで試す方法、VS Code拡張とelanによるインストール、lakeでのプロジェクト作成、Mathlib4の導入、基本文法、タクティクで書く最初の証明までを順に扱います。掲載したLeanのコードとmacOS向けのコマンドは、2026年10月13日にmacOS（Intel）上で実行して出力を確かめたものです（Lean本体だけの例は4.35.0、Mathlibを使う例はMathlibが指定した4.35.0-rc4）。Windowsの手順は公式ドキュメントからの引用です。

まとめ

Lean4は「型が命題、プログラムが証明」という考え方で動く言語です。theoremで書いた主張に証明が通ると、カーネルと呼ばれる小さな検査器が「その命題がその証明から導ける」ことを確かめます。保証されるのは書いた命題の証明までで、命題が意図した仕様を正しく表しているかは人間が確かめます。証明の途中経過はVS Code拡張のInfoviewに「残りのゴール」として表示されるので、対話しながら証明を組み立てられます。

まず試す：インストール不要のLean 4 Webで書いてみる
入れる：VS Codeに拡張「Lean 4」（leanprover.lean4）を入れ、セットアップガイドの「Install Lean」でelanを導入する
作る：lake new helloでプロジェクトを作り、lake buildでビルドする
数学をやる：Mathlib入りのプロジェクトはlake +leanprover-community/mathlib4:lean-toolchain new 名前 mathで作り、lake exe cache getでビルド済みファイルを取得する
証明する：rfl・decide・rw・induction・simp・omega・grindから覚える

Lean本体の公開直後はMathlibの対応タグがまだ無く、手元のLeanの版でlake new … mathを実行すると失敗します（後述の実測）。以下、概要から順に見ていきます。

Lean4とは：定理証明支援系と関数型言語を兼ねる理由

定理証明支援系としてのLean

Leanでは、命題を型として書き、その型を持つ値を作ることが証明になります（Curry-Howard対応）。たとえば2 + 2 = 4は型であり、rflはその型の値です。人間が書いた証明はカーネルが1ステップずつ検査するので、推論の途中に飛躍や見落としがあれば受理されません。ただしsorryや追加の公理に頼った宣言も警告付きで通るため、何に依存しているかは後述の#print axiomsで確かめます。

theorem two_plus_two : 2 + 2 = 4 := rfl

theorem bad : 2 + 2 = 5 := by decide
-- error: Tactic `decide` proved that the proposition
--   2 + 2 = 5
-- is false

誤った主張は、このように検査の段階で拒否されます。紙の証明では読み手が行間を補いますが、Leanでは省略した推論ステップがあれば検査を通りません。

プログラミング言語としてのLean

Leanは証明専用の道具ではなく、IOを扱う実行ファイルも作れる純粋関数型言語です。Lean自身のコンパイラやビルドツールLakeの大部分もLeanで書かれています。下はlake new helloが生成するMain.leanそのもので、ビルドするとHello, world!を出力します。

import Hello

def main : IO Unit :=
  IO.println s!"Hello, {hello}!"

「新世代の純粋関数型言語になれるか」という問いには、条件付きで「なれる」と答えられます。型クラス、do記法、ネイティブコンパイル、強力なマクロがそろっている一方、Webフレームワークやデータベースドライバなどのライブラリ群はHaskellの得意分野と比べてもまだ薄いのが現状です。業務アプリの主言語にするより、「仕様を証明しておきたい中核ロジック」をLeanで書く使い方が現実的です。

開発体制とLean 3からの移行

Leanは2013年にLeonardo de Moura氏がMicrosoft Researchで開発を始めた言語です。現在の開発は、2023年7月にde Moura氏とSebastian Ullrich氏が設立したLean FRO（Convergent Research内の非営利組織）が主導しています。de Moura氏自身は2023年にAWSへ移っており、「Microsoftのプロジェクト」という説明は現在は当てはまりません。ライセンスはApache-2.0です。

Lean 3とLean 4のコードには互換性がありません。構文もライブラリも作り直されており、Lean 3向けのmathlib3は2024年7月24日にアーカイブされました。検索で見つかる解説がimport data.nat.basicのような小文字・ドット区切りのimportを使っていたら、それはLean 3時代の資料です。

Leanの利用分野：数学の形式化・ソフトウェア検証・AI研究

主要な用途の1つが数学の形式化です。コミュニティが育てる数学ライブラリMathlibは、公式の統計ページで定義137,943件・定理289,925件・貢献者772人（2026年10月13日取得）を数えます。ソフトウェア検証では、AWSの認可ポリシー言語Cedarの検証などが公式サイトで事例として挙がっています。AIに数学の証明を書かせる研究でも、出力の正しさを判定する「答案用紙」としてLeanが使われています（DeepSeekMathの自己検証の仕組みも参照）。

Lean 4 Webでのブラウザ実行（インストール不要）

インストール前に雰囲気をつかむなら、公式のオンラインエディタLean 4 Web（live.lean-lang.org）が最短です。lean4webのREADMEによると、Leanはブラウザ内ではなくWebサーバー側で動いており、最新のMathlibもインストール済みです。import Mathlibを書いた例もそのまま試せます。

ただしREADME自身が、本格的な開発や大きなプロジェクトは対象外と明記しています。数十行の練習や、勉強会でコードを見せる用途に留め、複数ファイルに分けて継続的に書くなら、ローカルに入れて使います。

Lean4のインストール手順：VS Code拡張とelan

推奨手順：VS Code拡張「Lean 4」のセットアップガイド

公式のインストールページが推奨するのは、VS Codeと拡張機能「Lean 4」を使う方法です。

VS Codeをインストールする
拡張機能で「lean4」を検索し、提供元leanproverの「Lean 4」（ID：leanprover.lean4）を入れる
自動で開くセットアップガイドに従い、「Install Lean」ボタンでelan（Leanのバージョン管理ツール）を導入する

ガイドが開かない場合は、エディタ右上の∀アイコンから「Documentation」→「Docs: Show Setup Guide」で呼び出せます。elanはRustのrustupにあたる道具で、プロジェクトごとに必要なLeanの版を自動で取得・切り替えます。Lean本体を直接入れるのではなく、elan経由で入れるのが前提です。

手動インストール：elan-initのコマンド

ターミナルで入れる場合は、手動インストールの公式手順にあるelan-initを使います。macOSとLinuxは次の2行です。

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
source $HOME/.elan/env

WindowsはPowerShellスクリプト版を取得して実行します。

curl -O --location https://elan.lean-lang.org/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1

VS Code拡張はcode --install-extension leanprover.lean4でも入ります。公式は手動よりもセットアップガイドを強く勧めているので、PATHの設定などでつまずいたら推奨手順に戻るのが早道です。

インストール後の確認とディスク容量

$ elan --version
elan 4.2.4 (227caca13 2026-08-25)
$ lean --version
Lean (version 4.35.0, x86_64-apple-darwin24.6.0, commit eb6cafb7290e, Release)
$ lake --version
Lake version 5.0.0-src+eb6cafb (Lean version 4.35.0)

elanは初回にLeanを呼び出したタイミングでツールチェーンをダウンロードします。手元ではLean 4.35.0を1つ入れた時点で~/.elanが2.8GBになりました。Mathlibを使うと、Mathlibが指定する別の版のツールチェーンも同じ場所に増えていきます。入っている版はelan toolchain listで確認でき、使われていないと判定された版はelan toolchain gcで一覧でき、elan toolchain gc --deleteで削除できます。判定はelanを実行したことのあるディレクトリのlean-toolchainをもとにするので、削除前に一覧を確認してください。

LakeによるLean4プロジェクトの作成とビルド

lake newの5種類のテンプレート

Lakeは、Leanに同梱されているビルドツール兼パッケージマネージャです。lake new 名前テンプレートで雛形を作ります。Lake 5.0.0のlake new --helpが示すテンプレートは5種類です。

テンプレート	中身	使う場面
`std`（既定）	ライブラリ＋実行ファイル	言語として学ぶ
`exe`	実行ファイルのみ	CLIツール
`lib`	ライブラリのみ	他から使う部品
`math-lax`	ライブラリ＋Mathlib依存	数学を気軽に
`math`	Mathlib依存＋Mathlib流のlint設定	Mathlib準拠で書く

設定ファイルは既定でTOML形式のlakefile.tomlです。lake new hello std.leanのように.leanを付けると、Leanで書くlakefile.leanになります。

lake buildとlake exeによるビルドと実行

$ lake new hello
$ cd hello
$ lake build
✔ [8/8] Built hello:exe (2.0s)
Build completed successfully (8 jobs).
$ lake exe hello
Hello, world!

生成されるのはlakefile.toml、lean-toolchain、Main.lean、Hello.lean、Hello/Basic.leanなどです。初回のlake buildは手元で約13秒でした。ビルド成果物は.lake/に出力され、.gitignoreにも最初から入っています。

lean-toolchainによるLeanのバージョン固定

プロジェクト直下のlean-toolchainにはleanprover/lean4:v4.35.0のように使う版が1行で書かれています。elanはこのファイルを読み、そのディレクトリでは指定の版を自動で使います。チームでLean本体の版をそろえるには、このファイルを共有すれば足ります。ただし版を上げるときは、Mathlibなどの依存も対応する版へlake updateで更新し、破壊的変更に合わせてコードを直してから再ビルドします。

Mathlib4の導入と依存管理

Mathlibの収録分野と数学向けタクティク

Mathlib（Lean 4版を指してMathlib4とも呼ばれます）は、集合・群・環・位相・測度・解析までをカバーするコミュニティの数学ライブラリです。自然数の足し算程度ならLean本体だけで証明できますが、実数・行列・素数などを扱う証明は事実上Mathlibが前提になります。ring・linarith・norm_numといった数学向けのタクティクも、Lean本体ではなくMathlib側にあります。

新規プロジェクトへのMathlib導入とキャッシュ取得の実測

公式手順は、MathlibのリポジトリにあるLeanの版を指定してプロジェクトを作る方法です。

lake +leanprover-community/mathlib4:lean-toolchain new my_math math
cd my_math
lake exe cache get

lake exe cache getは、Mathlibのビルド済みファイル（.olean）を一括でダウンロードするコマンドです。キャッシュを取得していない状態でlake buildすると、依存するMathlibのモジュールを手元でコンパイルし始め、何時間もかかることがあります。

2026年10月13日に手元（macOS・Intel）で実行した結果は次のとおりです。Lake 5.0.0ではlake new … mathの時点でMathlibの取得とキャッシュの展開まで進み、続けて実行したlake exe cache getは「No files to download」で約30秒で終わりました。

項目	実測値
Mathlibが指定したLeanの版	v4.35.0-rc4
`lake new … math`の所要時間	5分48秒（rc4ツールチェーンの取得込み）
取得したキャッシュ	9,004ファイル
プロジェクトの`.lake`	7.5GB（うちmathlib 6.8GB）
`import Mathlib`するファイルの検査	初回約2分10秒、2回目約34秒

今回の環境では、Mathlibのプロジェクト1つとツールチェーン2版（4.35.0とrc4で計5.6GB）を合わせて13GB前後のディスクを使いました。.lakeはプロジェクトごとに作られるので、練習用のプロジェクトは1つにまとめてファイルを足していくほうがディスクを節約できます。import Mathlibを書いたファイルでring・norm_num・linarith・by_contraを使う例も、この環境で通ることを確かめています。

import Mathlib

example (a b : ℝ) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by ring
example : Nat.Prime 101 := by norm_num
example (x y : ℝ) (h₁ : x < y) (h₂ : 0 < x) : 0 < y := by linarith

失敗例：Lean公開直後のMathlib対応タグ不足

先頭の+leanprover-community/mathlib4:lean-toolchainを省くと、手元の既定の版（ここでは4.35.0）でプロジェクトが作られ、lakefile.tomlにrev = "v4.35.0"が書き込まれます。Lean 4.35.0公開の翌日（2026年10月13日）の時点では、Mathlibにまだv4.35.0タグが無く、lake updateは次のエラーで止まりました。

$ lake new mymath math
$ cd mymath && lake update
info: leanprover-community/mathlib: fetching revision 'v4.35.0' from https://github.com/leanprover-community/mathlib4
fatal: couldn't find remote ref v4.35.0
error: leanprover-community/mathlib: failed to fetch the package revision

同じ時点のMathlibのlean-toolchainはv4.35.0-rc4で、タグもv4.35.0-rc4までしかありませんでした。Mathlibが本体の正式版に追いつく時期は一致しないことがあるので、Mathlibを使うプロジェクトでは手元の最新版ではなく「Mathlibが今使っている版」に合わせるのが原則です。公式手順の+…:lean-toolchainはそのための指定です。

既存プロジェクトへのMathlib追加とバージョン整合

stdテンプレートで作ったプロジェクトに後から入れる場合は、lakefile.tomlに依存を書き足し、lean-toolchainをMathlibと同じ版にそろえてから更新します。

[[require]]
name = "mathlib"
scope = "leanprover-community"

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update
lake exe cache get

lake updateは依存の版を解決してlake-manifest.jsonを書き換えます。Mathlibを更新するたびにLean本体の版も上がることがあるので、更新後はもう一度lake exe cache getを実行します。

定理の探し方：exact?・Loogle・ドキュメント

Mathlibの定理は数十万件あり、名前を覚えるより探し方を覚えるほうが早く進みます。証明の途中でexact?と書くと、今のゴールを閉じられる定理を探して提案してくれます。exact?はLean本体に入っているので、Mathlibが無くても使えます。

example (a b : Nat) : a + b = b + a := by exact?
-- Try this:
--   [apply] exact Nat.add_comm a b

型の形から定理を検索するならLoogle、名前空間から一覧を引くならMathlibのドキュメントを使います。

VS CodeでのLean4開発：Infoviewと記号入力

Infoviewの仮定・ゴール表示の読み方

拡張を入れた状態で.leanファイルを開き、by以下にカーソルを置くと、右側のInfoviewにその位置での仮定とゴールが表示されます。たとえば二重否定の証明でintro hまで進めると、次のように表示されます。

P : Prop
h : ¬¬P
⊢ P

⊢の上が使える仮定、下が示すべきゴールです。タクティクを1行書くたびにこの表示が変わるので、「次に何を示せばよいか」を常に確認しながら進められます。エラーは該当行に赤線で示され、すべてのゴールが閉じると「No goals」になります。

記号の入力方法：バックスラッシュ略語

Leanのコードには→や∀などの記号が出てきますが、キーボードから直接打つ必要はありません。拡張はバックスラッシュに続けて略語を打つと記号に置き換えます。

入力	記号	入力	記号
`\to`	→	`\N`	ℕ
`\and`	∧	`\or`	∨
`\not`	¬	`\forall`	∀
`\exists`	∃	`\iff`	↔
`\le`	≤	`\ne`	≠

対応表は拡張のソース（vscode-lean4のabbreviations.json）で確認しました。記号にマウスを乗せると入力方法がツールチップで出るので、他人のコードを写すときも困りません。VS Code以外では、EmacsとNeovimにもコミュニティ製の拡張があります。

Lean4の基本文法

def・#eval・#checkと型

defで定義し、#evalで評価、#checkで型を確認します。#で始まるコマンドの結果はInfoviewに出ます。

def answer : Nat := 42
#eval answer + 1      -- 43
#check answer         -- answer : Nat
#eval 7 / 2           -- 3
#eval (7 : Float) / 2 -- 3.500000

型は名前 : 型の形で書き、省略できる場面では型推論が補います。整数リテラルは既定でNat（自然数）になるので、7 / 2は切り捨てて3です。

Natの切り捨て減算とIntとの違い

#eval (5 : Nat) - 10  -- 0
#eval (5 : Int) - 10  -- -5

Natには負の数が無いため、引き算は0で止まります（切り捨て減算）。証明で「a - b + b = a」が常には成り立たない（b ≤ aのときだけ成り立つ）のはこのためで、初学者が最初にはまる箇所です。負の数が要る計算では最初からIntを使います。

関数・パターンマッチ・再帰

def double (n : Nat) : Nat := 2 * n

def fact : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * fact n

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

#eval fact 10  -- 3628800
#eval fib 20   -- 6765

引数の形で場合分けするパターンマッチで、再帰関数を素直に書けます。Leanは再帰が必ず止まることを確かめてから定義を受け付けます。fact nの呼び出しは引数が1つ小さくなっているので、自動で停止性が示されます。止まることを示せない再帰には、termination_byで減っていく量を指定するか、partialを付けて停止性の証明を省きます（その代わり、証明の中で関数の中身を展開して使えなくなります）（再帰そのものの考え方は再帰関数の仕組みとスタック・末尾再帰で扱っています）。

高階関数とラムダ式

def applyTwice {α : Type} (f : α → α) (x : α) : α := f (f x)

#eval applyTwice (· + 3) 10                  -- 16
#eval applyTwice (fun s => s ++ "!") "Lean"  -- "Lean!!"
#eval [1, 2, 3, 4].map (fun x => x * x)      -- [1, 4, 9, 16]
#eval [1, 2, 3, 4].filter (· % 2 == 0) |>.foldl (· + ·) 0  -- 6

{α : Type}の波かっこは暗黙引数で、呼び出し側では型を書かずに推論させます。(· + 3)はfun x => x + 3の短縮記法です。map・filter・foldlの考え方は他の関数型言語と共通なので、関数型プログラミングの純粋関数・高階関数の知識がそのまま使えます。

structureによる構造体定義とReprによる表示

structure Point where
  x : Float
  y : Float
deriving Repr

#eval ({ x := 1.5, y := 2.0 } : Point)  -- { x := 1.500000, y := 2.000000 }

deriving Reprを付けると、#evalで中身を表示できるようになります。複数の場合を持つ型はinductiveで定義します。

最初の定理の証明：タクティクの基本

証明はtheorem 名前 : 主張 := 証明の形で書きます。byの後ろに「タクティク」と呼ばれる命令を並べると、ゴールを少しずつ変形して閉じていけます。この章のコードはすべてLean本体だけで通り、Mathlibは使っていません。

rflとdecideによる計算を使った証明

theorem my_mul_zero (n : Nat) : n * 0 = 0 := rfl

example : 2 + 2 = 4 := by decide

n * 0 = 0は、自然数の掛け算が2番目の引数で定義されているため、両辺を計算するだけで一致します。rflは「両辺が計算上等しい」ことを示す証明です。decideは具体的な値どうしの命題を計算で真偽判定します。

inductionとrwによる帰納法と式の書き換え

一方、引数の順序を入れ替えた0 * n = 0はrflでは閉じません。既存の補題を使うsimpなら一手で通りますが、ここでは仕組みを見るために帰納法で証明します。

theorem my_zero_mul (n : Nat) : 0 * n = 0 := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.mul_succ, ih]

induction n withでn = 0の場合とn = k + 1の場合に分かれます。succの場合のゴールは0 * (k + 1) = 0で、rw [Nat.mul_succ]で0 * k + 0 = 0に書き換え、帰納法の仮定ih : 0 * k = 0で書き換えると閉じます。n * 0と0 * nでrflが通るかどうかが分かれるのは、定義がどちらの引数で場合分けしているかで決まるからです。

simp・omega・grindの自動証明と適用対象

example (a b : Nat) (h : a < b) : a + 1 ≤ b := by omega
example (a b c : Nat) : a + b + c = c + b + a := by omega
example (xs ys : List Nat) : (xs ++ ys).length = xs.length + ys.length := by simp
example (a b : Nat) (h₁ : a = b) (h₂ : b = 3) : a + 1 = 4 := by grind

omegaは整数・自然数の線形算術（足し算と定数倍、不等式）を自動で解きます。simpは登録された書き換え規則で式を簡約します。grindはSMTソルバーに着想を得た自動証明のタクティクで、Lean 4.16.0（2025年2月）に開発中の機能として入り、現在は仮定から等式をたどる証明を一手で閉じます。学習の初期は自動化に頼りすぎず、rwやinductionで手を動かして、Infoviewのゴールの変化を見たほうが理解が進みます。

古典論理の証明：Lean本体とMathlibの背理法の違い

「¬¬PならばP」のような背理法を使う証明では、ネット上の解説によくby_contraが出てきます。ところがMathlibを読み込まずにLean 4.35.0でintro h→by_contra nP→exact h nPと書くと、by_contraの行がunknown tacticになりました。by_contraはMathlib側で提供されるタクティクだからです。Lean本体だけで通る書き方は次のとおりです。

theorem double_negation (P : Prop) : ¬¬P → P := by
  intro h
  exact Classical.byContradiction h

Lean本体だけで書くなら、上のようにClassical.byContradictionを使うか、by_cases hp : Pで場合分けします。Mathlibを読み込んでいればby_contra nPと書けます。読んでいる解説のコードが通らないときは、まずそれがMathlib前提の記事かどうかを疑ってください。

sorryと#print axiomsによる未完成部分・依存公理の確認

theorem todo (n : Nat) : n + 0 = n := by sorry
-- warning: declaration uses `sorry`

#print axioms my_zero_mul      -- 'my_zero_mul' does not depend on any axioms
#print axioms double_negation  -- depends on axioms: [propext, Classical.choice, Quot.sound]
#print axioms todo             -- depends on axioms: [sorryAx]

sorryは「証明はあとで書く」という仮置きで、警告は出ますがファイル全体のチェックは通ります。そのため、他人の「Leanで証明済み」を信用する前に#print axiomsで依存を確かめます。sorryAxが出たら未完成です。それ以外に見慣れない公理（axiomで独自に追加したものなど）が並んでいないかも確認します。Classical.choiceが出るのは古典論理を使った証明で、誤りではありません。

メタプログラミングとmacroによる構文拡張

Leanでは、構文やタクティクそのものをLeanで追加できます。最小の例はmacroによる記法の追加です。

macro "twice! " n:term : term => `(2 * $n)
#eval twice! 21  -- 42

Mathlibのringやlinarithも、この仕組みでLean自身に書かれたタクティクです。分野ごとの記法（DSL）や独自の自動証明を足せることが、Leanを数学とソフトウェア検証の両方に広げた理由の1つです。入門段階では「標準のタクティクもユーザーが書いたコードである」と知っておけば十分です。

Lean 4.35.0の主な変更点

4.35.0のリリースノートによると、この版には214件の変更が入りました。入門者に関係するものを挙げます。

vcgen：命令的なプログラムの検証条件を生成するmvcgenの後継。mvcgenは非推奨に
lake check：プロジェクトをビルドして書き出し、カーネルで検査し直す。標準以外の公理を使っているとエラー
lake comparator：証明が与えられた命題と一致するかを照合する
Decidableの定義変更：Boolと証明を持つ構造体になり、rflで閉じる等式が増えた
constructorの警告：複数の構成子が当てはまるときに警告。従来の動きはconstructor!

lake checkは検査対象のコードをbwrapのサンドボックスで動かす設計です。macOSで実行すると「bwrap, which needs Linux namespaces」というエラーで止まりました。macOSで使う場合はLinuxのコンテナやCI上で走らせる前提になります。

Lean4を学ぶべき人と、向かない場面

Leanが向いているのは、次のどれかに当てはまる人です。

数学の証明を機械で検査したい、またはMathlibの形式化に参加したい
AIが生成した証明やコードの正しさを判定する仕組みを作りたい
暗号・認可・プロトコルなど、間違えたときの損失が大きいロジックの仕様を証明しておきたい

逆に、テストを手厚くすれば足りるWebアプリの品質確保が目的なら、Leanから入るのは遠回りです。まずプロパティベーステストで性質を書く習慣を付けるほうが、導入コストに対する効果は大きくなります。他の証明支援系との比較では、既存の大規模な検証資産（CompCertなど）を使うならRocq（旧Coq）、seL4のようなOS検証の蓄積を使うならIsabelleが候補になります。新しく数学を形式化する、AIと組み合わせる、という目的ならMathlibの規模と更新頻度からLeanを選んでよいでしょう。

学習教材は、公式のTheorem Proving in Lean 4（定理証明）とFunctional Programming in Lean（プログラミング）、Mathlibで数学を書くMathematics in Leanが定番です。日本語では、有志による翻訳や解説をまとめたlean-jaから入れます。ゲーム感覚で自然数の公理から証明を積み上げるNatural Number Gameはブラウザ上で動くので、インストール前にタクティクの感覚をつかむ教材に向いています。数式を美しく書く側の道具はLaTeXで、Leanとは役割が違います。

よくある質問

Lean4はインストールせずにブラウザで試せますか？

試せます。公式のLean 4 Web（live.lean-lang.org）を開けば、環境構築なしでコードを書いて検査結果を確認できます。Leanはブラウザ内ではなくサーバー側で動いており、Mathlibもインストール済みです。大きなプロジェクトは対象外なので、続けて学ぶならローカルに入れてください。