Seminar deep study（セミナー深掘り研究）
1本の論文を深く研究してセミナー発表を準備します。まずエージェントは対話形式で証拠に基づいて論文選びを支援します。次に論文を、すべての主張に検証ステータスが付いたダイジェストに書き直します。数式処理システム（CAS）で計算を再実行し、Leanで論理を形式化し、論文内の発見事項を記録します。最後に、その唯一の真実源から発表資料を作成します。ユーザーが決定し、エージェントは証拠を提示して提案し、述べるすべてを検証します。
バンドルされているファイルはこのスキルのベースディレクトリ（スキル読み込み時に表示）からの相対パスです。以下これを$SKILLと呼びます。プロジェクトファイルはユーザーのプロジェクトディレクトリに置かれ、$SKILLの中に置かれることはありません。
フェーズと読むべきもの
| フェーズ | 最初に読むもの | 残すもの |
|---|---|---|
| 0 インテーク | references/intake.md | MEMORY.md内の回答、PLAN.md内の未決定事項 |
| 1 トピックアイデア出し | references/ideation.md | 選ばれた論文、すべての候補はJOURNAL.mdに |
| 2 ソース、足場、ダイジェスト | references/digest.md | リポジトリ、source/SOURCE.md、発見事項レジスタ付きダイジェスト |
| 3 検証 | references/verification.md、references/lean-palomar.md、references/compute.md | CASトランスクリプト、数値スクリーン、Leanライブラリ、監査、ログ |
| 4 資料 | references/materials.md、templates/briefs/ | ノート、スライド、黑板計画、Verso文書、ランディングページ、Vault |
| 5 ライブデモ | references/live-demo.md | リハーサル済みデモファイルとフォールバック |
| 6 文書化 | references/documentation.md | ジャーナル、計画、メモリ、Vaultノート、コミット |
| 7 公開 | references/publishing.md | なし（このセッションでユーザーが要求した場合を除く） |
| 任意 | references/traps.md | Lean、クラスター、CAS、サイト作業の前に読む |
| CS論文 | references/computer-science.md | フェーズ1～5の計算機科学向け読み替え |
フェーズはメニューであり、順番に従う必要はありません。読み物のみの発表ならフェーズ0～2と必要な資料までで十分です。既に論文を持って始めたユーザーはフェーズ0から始め、フェーズ1をスキップします。
原則
- ユーザーが選び、あなたは証拠を添えて提案する。 論文、深さ、公開先を黙って決めてはいけません。方向転換（「納得できない」「もっと最近のもの」）は普通です：それはプロファイルを洗練させるので、前回のものを擁護する代わりに新しいラウンドを始めましょう。
- 一次情報源のみを使用する。 タイトル、著者、日付、バージョン、ページ数、コードの入手可能性は、arXivのアブストラクトページまたはAPI、PDF自体、リポジトリで確認します。企業や報道によるアナウンスは「主張」としてラベル付けします。
- 表示されるすべての数値は計算されたものであり、記憶から呼び出したものではない。 スライド、ページ、ノート上の数値は、実行されたノートブック、CASトランスクリプト、Lean出力、またはビルドログから取得します。
- 真実は一つ。 ダイジェストが数学的な真実の源です。その各主張には
[Lean]、[CAS]、[num]、[exp]、[paper]のタグが付きます。ノート、スライド、Verso文書、ページはこれから派生し、決して矛盾しません。 - CASが見つけ、証明検証器が確認する。 証明書はCASトランスクリプトからジェネレータ（
tools/cert2lean.py）を通ってLeanに送られます。生成されたファイルは再ビルドされ、手で編集されることはありません。 - 難しいが標準的な事実は明示的な仮説とし、公理にはしない。 それぞれをダイジェストと形式化メタデータに記録します。
- 発見事項はデフォルトで機密。 他人の未発表論文に関する発見事項は、ユーザーが決定するまでプロジェクト内に留めます。実際のエラーの場合は、まず著者に伝えることを提案します。
- マシンと共有リソースを保護する。 ツールチェーンをインストールする前に空きディスク容量を確認し、
MATHLIB_NO_CACHE_ON_UPDATE=1なしでlake updateを実行せず、ユーザーの他のプロジェクト内ではビルドしません。references/compute.mdのクラスターエチケットに従います。 - ファイルの所有者は一つ。 各サブエージェントは自身のディレクトリのみを書き込み、あなたが統合、レビュー、コミットします。
- 外部向けのアクションは、現在のセッションでの明示的な要求が必要。 これには、デプロイ、プッシュ、リモートリポジトリの作成、アーティファクトの公開が含まれます。秘密（パスワード、トークン、秘密鍵）をファイルに書き込んではいけません。
- ユーザーの専門用語は、まずユーザー自身のファイルで調べる。 なじみのない用語（「register class」、セミナーの略語など）は、ユーザーのノートやプロジェクトで定義されていることがよくあります。そこで検索し、次にウェブ、それから質問します。
フェーズ0: インテーク
まず環境を読み取り専用で調査し、質問が具体的な選択肢を提示できるようにします。空きディスク容量（df -h ~）、インストール済みLeanツールチェーン、利用可能なCAS（ローカルまたはリモート）、Pythonとuv、ユーザーがコピー先の形式として指定したプロジェクトを確認します。次に質問ツール（Claude CodeのAskUserQuestion）で質問します：呼び出しごとに最大4つの質問、各質問に2～4の選択肢、推奨オプションを最初に「（推奨）」とマークします。質問バンクはreferences/intake.mdにあります。発表、トピックと深さ、CASと計算、成果物、ダッシュボードの配信方法（ローカルのみかオンラインか、どこに、今か後か）、gitをカバーします。ユーザーの最初のメッセージで既に回答されているものはスキップし、1行で確認します。回答は日付付きの決定としてMEMORY.mdに記録します。未決定のものはPLAN.mdに❓として入れます。
フェーズ1: トピックアイデア出し（論文が指定されていない場合）
ユーザーが選ぶまでラウンドを実行します（references/ideation.md）：
- ユーザーのarXiv記録（
tools/arxiv_scan.py author）、現在のプロジェクトのREADME、ユーザーの発言から興味プロファイルを構築します。3行で表示して修正を促します。 - 並行して検索：ニュースのウェブ検索、カテゴリ×トピック×最近の期間でのarXiv API（
tools/arxiv_scan.py scan、次にrank）、GitHub APIとスクラッチパッドへの浅いクローンによるコードリポジトリ（Leanコード用tools/tactic_census.py）。 - 提示するすべての候補を検証します（ID、タイトル、著者、日付、バージョン、PDFからのページ数、コードリンク）。安価にできる場合は、目覚ましい主張を自分で再確認します。
- 短縮リストを散文で提示します：ユーザーと形式に合う理由を含む1つの推奨、トレードオフを含む2～3の代替案、フィルターのすぐ外にある論文、5分の価値があるニュース、および情報源。最後に1つの直接質問で終わります。質問ツールは最終選択を明確にするための便利な手段です。ユーザーが明確化のために辞退した場合は、話したいということなので、何を変更したいか尋ねます。
- すべての候補とそれが却下された理由を記録します。足場構築時に
JOURNAL.mdに入ります。
フェーズ2: ソース、足場、ダイジェスト
PDFとLaTeXソースをsource/に取得します（git管理外）。バージョンとSHA-256チェックサムをsource/SOURCE.mdに記録します。数式とリストはLaTeXから転記し、PDFのテキストレイヤーからは決して転記しません。tools/scaffold.pyでプロジェクトの足場を構築します（ドキュメントテンプレート、ダイジェスト、オプションでLean、CAS、クラスター、サイト、スライド、ブック、Verso、Vaultの骨格）。次にダイジェスト（templates/digest/digest.md）を書きます：結果を3行で、背景、準備、定理ごとのセクション（証明のアーキテクチャとステータスタグ付き）、発見事項レジスタ（重要度：confirmed / wording / implicit hypothesis / strengthening / error）、練習問題。詳細：references/digest.md。
フェーズ3: 検証
すべての計算に関する主張と「確認すればわかる」をPLAN.mdの検証テーブルの行に変換し、それを処理します：
- 最初に数値スクリーン（高精度；転記ミスをキャッチし、何も証明しない）；
- コミットされたトランスクリプト付きのCASスクリプト。
CHECK行は真でなければならず、不一致は発見事項レジスタに送られます（references/verification.md）； - 証明書：CASが
CERTブロックを出力し、tools/cert2lean.pyがLeanファイルを書き、linear_combinationまたはringが各恒等式をチェックします。grindは証明書なしで同じステップを再証明でき、それを見せる価値があります； - Lean：まずステートメント、次に証明。ライト版またはPalomarクラス（
Challenge.lean/Solution.lean/comparator.json、標準公理のみ、import allによる公理監査、lake comparator --paranoid、警告なしビルド、ログ）。references/lean-palomar.mdとreferences/compute.md（ローカル対クラスタービルド、ディスク容量ルール）を参照。
リンターワーニングは発見事項の可能性として扱います：未使用のインスタンス引数は、定理が論文の主張よりも一般的に成り立つことを意味する可能性があります。
フェーズ4: 資料（並列サブエージェントによる）
成果物ごとに1つのバックグラウンドエージェントを起動し、それぞれが自分のディレクトリを所有します：CAS再検証、Verso文書、ノート（Jupyter Book）、スライド付き黑板計画、ヒーローイメージとVault付きランディングページ。templates/briefs/のブリーフを埋めます。各ブリーフは、真実の源（ダイジェスト、Leanファイル、トランスクリプト）、述べてよい事実、実行してよいコマンド、そして数値、名前、時間、部屋を決して捏造してはいけないことを指定します。それらが実行中も検証を続けます。事実が変わったら（新しい結果、新しいカウント、新しいデモ）、各実行中のエージェントにSendMessageで短い自己完結型の更新を送ります：「何が変わったか、どこにあるか、何を追加するか、'オプション、現在の計画を維持'」。エージェントは数値を再導出するため、ダイジェストの審判も行います：不一致を報告するよう依頼し、ダイジェストを修正し（日付付き）、他のエージェントに伝えます。複数のエージェントが実行中は空きディスクを監視します。エージェントが終了したら、その出力をレビューし（ビルド、開く、ヘッドレススクリーンショット）、成果物を相互にリンクし、コミットします。生成された資料はソースから再ビルドされます：スライドは逐語的な抜粋でないコードを拒否し、オフラインでも動作するようにベンダーライブラリを含みます。詳細：references/materials.md。
フェーズ5: ライブデモ
数秒で実行される1つのデモファイルを構築します：メイン定理の#checkと#print axioms、linear_combinationでチェックされる証明書、grindで証明される同じ事実、そしてコメントアウトされた「壊す」バリアント（目に見えて失敗する）。ローカルで、またはクラスタードライバーのdemoコマンドを介してリモートで実行します。2回リハーサルし、フォールバック（レンダリングされたVerso文書またはスクリーンショット）を保持します。詳細：references/live-demo.md。
フェーズ6: 文書化とセッション終了
プロジェクトにはCLAUDE.md（操作手順）、MEMORY.md（日付付きの事実と決定）、JOURNAL.md（日付付きエントリ）、PLAN.md（✅ 完了・🟡 進行中・⬜ 未着手・❓ ユーザー決定待ち）、MAINTENANCE.md（運用手順書）、README.md、Vaultが含まれます。各セッションの終了時に：ジャーナルエントリを追加し、計画を更新し、新しい概念と決定のVaultノートを追加し、コミットします（Conventional Commits）。クライアントメモリファイルには、プロジェクトを超えて存続すべき事実のみを保持します。詳細：references/documentation.md。
フェーズ7: 公開（明示的な要求があった場合のみ）
まずすべてをローカルでビルドします。このセッションで、フェーズ0で選ばれたターゲットに、ユーザーが要求したものだけを公開します：プライベートなClaudeアーティファクト、GitHub Pages、または許可リスト方式のデプロイスクリプト（ドライラン、リンクチェック、リークスキャン（tools/leak_scan.py）付き）を介したウェブサーバー。公開リポジトリは、ユーザーがプッシュする前に新しい履歴とリークスキャンを取得します。詳細：references/publishing.md。
開始チェックリスト
- フェーズ0の質問に回答し、決定を記録。
- 論文が選択された（フェーズ1）か与えられた。ソースを取得しチェックサムを確認。
python3 "$SKILL/tools/scaffold.py" <project> ...；git init；最初のコミット。- ダイジェストを作成、主張にタグ付け、
PLAN.mdに検証テーブルを作成。 - 検証と形式化を開始。ダイジェストが安定したら資料エージェントを起動。
- セッション終了：ジャーナル、計画、Vault、コミット。