数学工作流程
解决用户陈述的问题。不要将其变成一个广泛的研究项目。
工作流程
- 重新陈述问题并确定其数学领域。确定用户需要的是证明、计算、语料库查找还是形式化验证；仅澄清阻碍性的歧义。
- 使用
math_search查找相关手稿和策略。从广泛搜索开始，然后通过术语或假设缩小范围。使用math_manuscript仅阅读相关的摘要、大纲或 LaTeX 章节。如果 TeX 源文件缺失或需要已发布的措辞，请在选定页面上使用math_pdf_text。 - 对于证明，在进行代数运算之前先给出引理计划。将从语料库中引用的结果与新的推导分开，并检查每个引用结果的假设是否适用。
- 对于请求的形式化验证或 Lean 语句，使用
math_lean_search定位现有的声明，首先在小的代码片段上使用math_lean_check，然后为聚焦的目标使用math_lean_build。仅当存在匹配的挑战配置时，才使用math_comparator。默认情况下不要构建整个包。 - 对于数值或符号工作，对白名单上的 SymPy 操作使用
math_compute。否则，展示计算过程并说明执行限制。数值证据不能证明精确的断言。 - 独立检查边界情况、量词、假设和中间步骤。确认每个 Lean 检查是否实际通过以及它检查了哪个语句；通过一个不相关的片段并不能验证所请求的定理。
语料库与验证护栏
math/CONTENTS.md映射了 373 个结果系列中的 721 篇手稿。该档案包含原始研究产出，而非经过独立认证的结果。- 目前有 175 篇论文具有 Lean 形式化证明；
math/lean/formalization.yaml是目录。目录中的存在并不证明论文中的每个断言。 - 当结果看起来可疑时，检查
math/history.md；它记录了修订和撤回。不要默默依赖已撤回的结果。 - 切勿仅仅因为论文在语料库中就声称已被验证。
- 除非相关的
math_lean_check、math_lean_build或math_comparator调用实际成功，否则切勿声称 Lean 验证。明确报告失败、跳过的检查、缺失的前提条件和剩余的差距。 math/lean/是单个 Lake 包OAI，锁定到leanprover/lean4:v4.34.1。优先使用聚焦的目标，例如OAI.Analysis。- 使用
math_status检查当前的可用性；不要将不可用的检查视为成功。原生 Windows Lean 构建可能因锁定依赖项集中 NTFS 无效的路径而被阻止，Comparator/landrun 需要 Linux/WSL。报告此类阻止器，而不是默默切换声明。 - 引用相对于
math/的源路径，例如lean/formalization.yaml，并尽可能提供手稿标识符和章节名称。
工具使用模式
- 先广泛查询，再逐步缩小；不要为局部问题执行整个仓库的发现。
- 阅读相关章节而非整个 PDF。从元数据解析已发布 PDF 的路径，而不是假设文件名；仅对选定页面使用
math_pdf_text。 - 优先使用
math_grep在 TeX、Markdown 和 Lean 中查找确切名称或符号；使用math_lean_search查找声明名称。尽可能将搜索范围限定在相关文件或目录。 - 使用
math_compute进行符号检查，但要说明操作并独立验证返回的表达式。 - 保持输出有界：总结匹配项，仅引用必要的语句或证明步骤。
- 当需要刷新索引时，在
math/更改后使用math_reindex。
答案结构
- 定理/声明： 精确的陈述、假设和范围。
- 证明/推导： 引理计划和经过验证的步骤，或请求的计算或查找。
- 验证状态： 实际运行的检查、结果及其覆盖范围的限制。
- 来源： 相关的语料库路径和章节；区分引用和新工作。
- 未解决的差距： 未解决的步骤或缺失的检查，或明确表示未发现任何问题。