研討會深度研究

一場以深度研究方式準備的研討會報告。首先，代理程式協助使用者以證據為基礎的互動討論選定論文。接著，它將論文改寫為一份摘要，其中每個聲明都附有驗證狀態。它使用電腦代數系統（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 文件、著陸頁、筆記庫
5 現場示範	`references/live-demo.md`	一份排練過的示範檔案與備用方案
6 文件	`references/documentation.md`	日誌、計畫、記憶、筆記庫筆記、提交記錄
7 發布	`references/publishing.md`	無，除非使用者在本次工作階段要求
任意階段	`references/traps.md`	在進行 Lean、叢集、CAS 或網站工作前閱讀
電腦科學論文	`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）提問：每次呼叫最多四個問題，每個問題二到四個選項，推薦選項排在第一個並標記為「(Recommended)」。問題庫在 references/intake.md 中；涵蓋範圍包括：報告本身、主題與深度、CAS 與計算、可交付成果、儀表板的傳遞方式（僅限本地或線上，以及位置；現在或稍後），以及 git。跳過使用者第一則訊息已經回答的內容，並用一行文字確認。將答案記錄為 MEMORY.md 中的日期決策；未定決策則以 ❓ 放入 PLAN.md。

階段 1：主題構思（當未指定論文時）

重複回合直到使用者選定（references/ideation.md）：

從使用者的 arXiv 紀錄（tools/arxiv_scan.py author）、其當前專案的 README 以及他們所說的內容建立興趣輪廓。以三行顯示，以便使用者更正。
並行搜尋：網路搜尋新聞；透過 arXiv API 按類別 × 主題 × 時效性範圍搜尋（tools/arxiv_scan.py scan，然後 rank）；透過 GitHub API 及在暫存區進行淺層克隆搜尋程式碼儲存庫（針對 Lean 程式碼使用 tools/tactic_census.py）。
驗證將呈現的每個候選論文（ID、標題、作者、日期、版本、PDF 頁數、程式碼連結）。在成本低廉時自行重新檢查驚人的聲明。
以散文形式呈現候選清單：一項推薦（說明為何適合使用者與格式）、兩到三個替代方案（附帶權衡取捨）、剛好落在篩選條件之外的論文、值得花五分鐘了解的新聞，以及來源。最後以一個直接問題作結。問題工具是為了最終明確選擇的便利；如果使用者拒絕該問題以進行澄清，代表他們想討論，因此詢問他們想要改變什麼。
記錄每個候選論文及其被淘汰的原因；在建置骨架時將其放入 JOURNAL.md。

階段 2：來源、骨架、摘要

將 PDF 與 LaTeX 原始碼擷取到 source/（已加入 gitignore）。在 source/SOURCE.md 中記錄版本與 SHA-256 校驗和。從 LaTeX（而非 PDF 文字層）轉錄公式與列表。使用 tools/scaffold.py 為專案建立骨架（文件範本、摘要，以及可選的 Lean、CAS、叢集、網站、投影片、書籍、Verso 與筆記庫骨架）。然後撰寫摘要（templates/digest/digest.md）：三行結論、背景、設定、每個定理一節（含證明架構與狀態標籤）、發現登錄表（嚴重性：已確認 / 措辭問題 / 隱含假設 / 強化 / 錯誤），以及練習題。詳細資訊：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 以了解本地與叢集建置以及磁碟空間規則。

將 linter 警告視為可能的發現：未使用的實例參數可能意味著定理的成立範圍比論文所述更廣泛。

階段 4：材料，由平行子代理程式處理

每個可交付成果啟動一個背景代理程式，每個代理程式擁有自己的目錄：CAS 重新驗證、Verso 文件、筆記（Jupyter Book）、含白板規劃的投影片，以及含英雄圖片的著陸頁與筆記庫。填寫 templates/briefs/ 中的簡報。每個簡報指定事實來源（摘要、Lean 檔案、轉錄）、可以陳述的事實、可以執行的命令，以及絕對不能發明數字、名稱、時間或房間。在它們執行期間持續進行驗證。當事實改變時（新結果、新計數、新示範），透過 SendMessage 向每個正在執行的代理程式發送一個簡短的獨立更新：變更內容、位置、要新增的內容、「可選，保留你目前的計畫」。代理程式會重新推導數字，因此它們也會審查摘要：要求它們報告任何不一致，然後修正摘要（附上日期）並告知其他代理程式。在多個代理程式執行時監控可用磁碟空間。當代理程式完成時，審查其輸出（建置它、開啟它、進行無頭截圖），將可交付成果互相連結，然後提交。生成的材料會從其來源重建：投影片拒絕使用非逐字摘錄的程式碼，並且它們會攜帶供應商函式庫，以便報告在離線時也能運作。詳細資訊：references/materials.md。

階段 5：現場示範

建立一個可在幾秒內執行的示範檔案：#check 與 #print axioms 主要定理、由 linear_combination 檢查的一個憑證、由 grind 證明的相同事實，以及一個已註解掉的「破壞它」變體（會明顯失敗）。在本地執行，或透過叢集驅動程式的 demo 命令遠端執行。排練兩次並保留備用方案（渲染後的 Verso 文件或截圖）。詳細資訊：references/live-demo.md。

階段 6：文件與工作階段結束

專案包含 CLAUDE.md（操作說明）、MEMORY.md（帶日期的事實與決策）、JOURNAL.md（帶日期的條目）、PLAN.md（✅ 已完成 · 🟡 進行中 · ⬜ 待辦 · ❓ 使用者決策）、MAINTENANCE.md（操作手冊）、README.md 以及筆記庫。在每次工作階段結束時：附加日誌條目、更新計畫、為新概念與決策新增筆記庫筆記，然後提交（遵循 Conventional Commits）。客戶端記憶體檔案僅保存應比專案更長久的事實。詳細資訊：references/documentation.md。

階段 7：發布（僅在明確要求時）

先在本機建置所有內容。僅發布使用者要求的內容，在本次工作階段內，發布到階段 0 選擇的目標：私密的 Claude artifact、GitHub Pages，或透過允許清單部署腳本（包含試執行、連結檢查與洩漏掃描 tools/leak_scan.py）的網頁伺服器。公開儲存庫應有全新的歷史記錄，並在使用者推送前進行洩漏掃描。詳細資訊：references/publishing.md。

開始檢查清單

階段 0 問題已回答，決策已記錄。
論文已選定（階段 1）或已給定；來源已擷取並計算校驗和。
python3 "$SKILL/tools/scaffold.py" <project> ...；git init；首次提交。
摘要已撰寫，聲明已標記，PLAN.md 中已有驗證表。
驗證與形式化已啟動；一旦摘要穩定，材料代理程式即啟動。
工作階段結束：日誌、計畫、筆記庫、提交。

seminar-deep-study