Track L: 学習者能動化
目的: Track K（#61）で意味層・カード・証明骨子・エージェント製 Lean・演習解答が揃った。しかし 学習者が自力で解く・形式化する・反論に答える工程がどのプランにも存在しない。progress.md の ✅ は「教材あり」と「学習者ができる」を混同している。Track L はこの需要側（学習者の能動的訓練）を埋める。
GitHub トラッキング: #122 [topology][tracking] Track L: 学習者能動化
現状とギャップ
Section titled “現状とギャップ”Track K（#61）完了。教材（意味層・カード・証明骨子・エージェント製 Lean・演習解答）は供給側が揃っている。一方、学習者が自力で解く・形式化する・反論に答える工程がどのプランにも存在しない。progress.md の ✅ は「教材あり」と「学習者ができる」を混同している。
Track S（#96、学習ループ/SRS）は recall・reprove・SRS を担当。Track L はその補完（自力 Lean 形式化・セルフゼミ・達成ゲート）で、重複しない。
L-A: Lean 自力形式化ループ
Section titled “L-A: Lean 自力形式化ループ”エージェントによる Notes/ChapterN.lean 量産は現行路線を全速継続し、コーパスを学習インフラとして扱う:
- 機械検証済み参照解答 —
refs/math/topology/royal-road-to-topology/lean/Notes/のChapterI–IV,VII–Xの 8 章分（V・VI は未形式化。sorry ゼロ、lake build完走済み）。例:RoyalRoad.ChapterII.prop_II_1_1。 - 本書記法 → Mathlib の statement 対訳集 — 各
Notes/ChapterN.lean冒頭の「規約ブリッジ」節（例:chapter2.mdの規約ブリッジ節、フィルター順序 $\mathcal{F} \subset \mathcal{G}$ ↔𝓖 ≤ 𝓕の逆順序対応）。 sorry版演習の自動派生元 — 参照解答の statement 部分のみを残し証明本体をsorryに置換したExercises/ChapterN.leanを生成する（L-3, #119 で第II章を試作）。- 学習者 statement の同値性検証器 — 学習者が書いた statement が参照解答と同値かを機械的に確認する仕組み（
Notes/の型シグネチャと比較）。
学習者は statement + sorry の演習版（Exercises/ChapterN.lean）を自力で埋める。まず読了済みの II 章から。
L-B: セルフゼミ・プロトコル
Section titled “L-B: セルフゼミ・プロトコル”章ごとの想定問答ページ exercises/seminar-chapterN.md。
問いテンプレ:
- なぜこの定義か
- 仮定を弱めるとどこで壊れるか
- 反例を挙げよ
- 別証明・別特徴づけは
進め方: 学習者が先に回答 → エージェントが原著ページと突き合わせて赤入れ。
第II章試作は L-4（#120）。
L-C: progress.md 理解検証ゲート
Section titled “L-C: progress.md 理解検証ゲート”既存 ✅=「教材あり」、新設 🎓=「学習者達成」（自力演習・自力 Lean・セルフゼミ）。「第III章を読む」等の次アクションにゲートを紐付ける。
凡例・列構成の具体化は L-5（#121）。
L-D: 学習セッション指示規約
Section titled “L-D: 学習セッション指示規約”チューター役エージェントの規約:
- 答えを直接言わない
- 段階ヒント制: ①goal 言語化 → ②補題名 → ③骨子 → ④参照解答は最後の手段
- 出典ページ即答: 学習者が出典を求めたら即座にページ番号を返す（ヒント段階を飛ばしてよい）
- 誤答は原著該当箇所を指して自己修正させる（正解を直接示さない）
この規約は L-2（#118）でチューター用スキル lean-tutor として実装する。本節が正本。
Phase 一覧と issue
Section titled “Phase 一覧と issue”| Phase | issue | 内容 | 依存 |
|---|---|---|---|
| L-1 | #117 | Track L 正本ページ新設＋導線＋学習セッション指示規約 | — |
| L-2 | #118 | lean-tutor スキル新設（段階ヒント制チューター） | #117 |
| L-3 | #119 | 第II章 sorry 版演習の派生（Exercises/ChapterII.lean） | #117 |
| L-4 | #120 | セルフゼミ想定問答 第II章試作（seminar-chapter2.md） | #117 |
| L-5 | #121 | progress.md 学習者達成ゲート（🎓 凡例・列の分離） | #117 |
| tracking | #122 | [topology][tracking] Track L: 学習者能動化 | — |
#117 ──┬──→ #118 ├──→ #119 ├──→ #120 └──→ #121#118〜#121 は相互独立（依存関係なし）。ただし progress.md を触る issue（L-5）は Track K・S 側の同時実行と直列にする。
Track S（#96）との役割分担
Section titled “Track S（#96）との役割分担”recall・SRS・reprove（想起・再導出・記憶維持）は Track S、能動形式化・セルフゼミ・達成ゲート（学習者が自力で解く・証明する・反論に答える）は Track L。両者は重複しない相補プランで、progress.md に対する変更もそれぞれ別列・別注記で行う。
progress.md— 全体進捗の正本chapter2.mdの規約ブリッジ節 — 本書記法 ↔ Mathlib 対訳の前例refs/math/topology/royal-road-to-topology/lean/Notes/（ChapterI–IV, VII–X の 8 章、sorry ゼロ、lake build完走済み）— L-A の参照解答コーパス。例:RoyalRoad.ChapterII.prop_II_1_1
運用（完了後）
Section titled “運用（完了後）”- GitHub で #122 を開く
- issue 本文の「状態」を実リポジトリと突き合わせてから作業する（本ページを正本として更新）
- 新規の学習セッション規約の変更が発生した場合は、1 コミットでまとめて push し、対応 issue を更新する
- 導線・役割分担の点検は、本ページ・Track S ページ（
00_System/track-s-learning-loop.md）・progress.mdをセットで確認する