Lean モードをオンにすると、自然演繹で組み立てた証明と同じ証明を、定理証明支援系 Lean 4 のコード（タクティクによる証明）として見られます。プレイ画面の証明図の欄にある「Lean モード」のスイッチで切り替えます。

⟦0⟧

たとえば 2-4「関数の合成」を解くと、次のコードが書き上がります。

⟦1⟧

画面の見方

Lean の欄：証明図の上に開きます。操作するたびに、対応するタクティクが書き加えられ、直前の操作で増えた行が光ります。
sorry：まだ開いていない扉です。証明図の ⋮ や証明項の ? にあたり、いま取り組んでいる扉の sorry は枠で囲まれます。
右側のコメント（-- の後ろ）：その行に対応する推論規則です。→I¹ などの番号は、証明図の [P]¹ や証明項の x₁ と同じです。
並び方：操作した順番ではなく、扉の分かれ方に沿って並びます。扉が二つに分かれると、それぞれが · で始まる字下げされたまとまりになり、新しい行はその扉の場所に差し込まれます。
証明図の注記：証明図の各規則の横に、対応するタクティク（intro x₁ など）が小さく添えられます。
クリア画面：完成した証明木の下に Lean のコードが表示されます。再生ボタンで証明図を一手ずつたどると、Lean のコードも同じ手まで巻き戻り、まだ組み上がっていない部分は sorry になります。

操作とタクティクの対応

操作	規則	Lean
扉の → をタップ	→I	`intro x₁`
扉の ∧ ／鍵の ∧ をタップ	∧I ／ ∧E	`constructor` ／ `have ⟨d₁, d₂⟩ := h₁`
扉の ∨ ／鍵の ∨ をタップ	∨I ／ ∨E	`left`・`right` ／ `rcases h₁ with x₁ \| x₂`
鍵を同じ形の扉へ	⟦2⟧	`exact h₁`
鍵 A→B を扉 B へ／鍵を鍵へ	→E	`apply h₁` ／ `have d₁ := h₁ h₂`
⊥ を目指す	⊥E	`exfalso`
背理法の魔法	RAA	`apply Classical.byContradiction` と `intro x₁`
扉の ∀ ／鍵の ∀	∀I ／ ∀E	`intro a` ／ `have d₁ := h₁ a`
扉の ∃ ／鍵の ∃	∃I ／ ∃E	`refine ⟨a, ?_⟩` ／ `obtain ⟨a, x₁⟩ := h₁`
扉の = ／等式の鍵で書き換え	=I ／ =E	`rfl` ／ `rewrite [← d₁]`
点線の記号を展開	⟦3⟧	`show …`
補題を立てる／帰納法	⟦4⟧ ／ ⟦5⟧	`have x₁ : … := by` ／ `induction a with`

書き換えには、rw ではなく rewrite を使います。rw は書き換えた後で自動的に扉を閉じてしまうことがあり、ゲームの「= をタップする」一手と食い違うためです。また、鍵の ∧ を分解するときは、元の鍵を残すために obtain ではなく have ⟨…⟩ := を使います。

命題の書き方

問題の主張は example (…) : 目標 := by の形で書かれます。( ) の中が仮定で、入口の鍵が h₁, h₂, …、定理カードが c₁, … です。

住人（⟦6⟧ 以降）：住人の型を α とし、「住人は少なくとも一人いる」という約束を [Nonempty α] と書きます。述語は P : α → Prop、∀x P(x) は ∀ x, P x です。新しく呼んだ住人は、コードの最初に [Nonempty α] から取り出します。
集合（⟦7⟧）：集合は「住人についての述語」として扱い、∈・⊆・∩・∪・ᶜ をゲームと同じ定義で前置きに書きます。定義の展開は、その定義どおりの形を show で示すことにあたります。
自然数（⟦8⟧〜⟦9⟧）：0 と「次の数」s だけからなる型 N を前置きで定義します。足し算・掛け算の性質は、ゲームと同じく公理（仮定）として与えます。⟦10⟧ の ≤ は、Lean の ≤ と区別して ≼ と書きます。

前置きは長いので、Lean の欄では「▶ 前置き」として折りたたまれています。押すと開きます。

本物の Lean で試すには

表示されるコードは、Mathlib を使わない Lean 4 だけで通るように書いてあります。このゲームを作るときに、すべてのステージのお手本の解き方から作ったコード（クリア画面の再生の各段階も含む）を、Lean 4（バージョン 4.35.0）で検査しています。前置きがあるときは前置きも含めて写せば、そのまま Lean のファイルとして使えます。証明の途中のコードも、sorry の警告が出るだけで読み込めます。

対応している範囲

証明する問題（⊢）のある層に対応しています。反例を作る問題（⊬）と、隠し層・公理の鏡では、Lean のコードは出ません。

Lean で背理法を使うには、Classical（選択公理などから導かれる古典論理の定理）を使います。隠し層「魔法の扉」の扉は、Lean でも Classical を使わなければ証明できない式です。