论文深度研读研讨会 是做什么的？
一场研讨会报告，以一篇论文的深度研究形式准备。首先，代理在基于证据的交互式讨论中帮助用户选择论文。然后，它将该论文重写为一份摘要，其中每个论断都附带其验证状态。它使用计算机代数系统（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 或站点工作前阅读 |
| 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。生成的文件将被重建，绝不手工编辑。 - 困难但标准的事实成为显式假设，而不是公理。 在摘要和形式化元数据中记录每个此类事实。
- 关键发现默认保密。 关于他人未发表论文的关键发现保留在项目中，直到用户决定。对于真正的错误，建议先通知作者。
- 保护机器和共享资源。 在安装工具链前检查可用磁盘空间，绝不运行
lake update而不带MATHLIB_NO_CACHE_ON_UPDATE=1，绝不在用户的其他项目内部构建。遵循references/compute.md中的集群礼仪。 - 每个文件一个所有者。 每个子代理只写入自己的目录；你负责整合、审查和提交。
- 面向外部的操作需要当前会话中的显式请求。 这包括部署、推送、创建远程仓库和发布工件。绝不将秘密（密码、令牌、私钥）写入任何文件。
- 首先在用户自己的文件中查找用户的术语。 不熟悉的术语（“寄存器类别”、研讨会缩写）通常在其笔记或项目中定义。在那里搜索，然后搜索网络，最后询问。
阶段 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 和临时目录中的浅克隆搜索代码仓库（tools/tactic_census.py用于 Lean 代码）。 - 验证将要呈现的每个候选论文（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 和知识库。在每个会话结束时：追加一条日志条目、更新规划、为新概念和决策添加知识库笔记，并提交（遵循约定式提交）。客户端记忆文件仅保存应比项目生命周期更长久的事实。详细信息：references/documentation.md。
阶段 7：发布（仅在明确要求时）
首先在本地构建所有内容。仅发布用户要求的内容，在当前会话中，发布到阶段 0 中选择的目标：私有的 Claude 工件、GitHub Pages，或通过一个允许列表部署脚本（包含预演、链接检查和泄漏扫描 tools/leak_scan.py）发布到 Web 服务器。公共仓库在用户推送之前会有一个全新的提交历史和泄漏扫描。详细信息：references/publishing.md。
启动检查清单
- 阶段 0 问题已回答，决策已记录。
- 论文已选择（阶段 1）或已给出；来源已获取并校验和。
python3 "$SKILL/tools/scaffold.py" <project> ...；git init；首次提交。- 摘要已编写，论断已标记，
PLAN.md中验证表已创建。 - 验证和形式化工作已开始；摘要稳定后启动材料代理。
- 会话结束：日志、规划、知识库、提交。