lean-formalize

Lean 形式化

每次审查前，请遵循 可选审查者： 通过规范的辅助解析器使用 reviewer_route.py，依次解析调用参数 → .aris/reviewer.json → Claude Code 默认设置（Codex MCP），同时保留本审查环节的等级、新鲜上下文、源文件/图像输入和确定性关卡。 以下 Codex 示例/固定配置仅适用于 backend=codex；其他路由使用各自的首次调用/回复约定。保存路由和实际返回的身份；不可用的选择记为 REVIEW_UNAVAILABLE。根据实际模型系列/完成情况/范围对验收结果分类。将调用参数中的审查者/模型/工作量覆盖设置传递给包含审查者的子任务。生成工作线程保持不变。

将用户的数学陈述转化为保留其含义、并通过检查的 Lean 定理。已编译的条件引理也算进展；是否完成取决于原始陈述以及实际采用的信任基础。

何时使用 Lean

当用户要求使用 Lean、继续现有 Lean 证明，或形式化验证能够解决核心主张中的具体不确定性时（例如依赖链很长、化简过程微妙，或需要覆盖有限分类），请使用此技能。说明它将帮助解决的义务，并在获准的任务范围内继续。单凭难度不足以构成形式化的理由。普通推导和简短证明可以继续使用 formula-derivation 或 proof-writer；不要将 Lean 设为每项数学结果的先决条件。遵循用户选择的证明方法以及所请求工作的规模。

核心工作流

Original statement and Lean definitions
  → A: cross-family adversarial statement alignment
  → Proof obligations, representations, and lemma interfaces
  → Lean implementation ↔ B: adversarial review of key arguments and connections
  → Actual inputs connected; original theorem assembled
  → Executed type, definition, and transitive-axiom audit
  → C: cross-family adversarial review of the final exported result
  → Reproducible delivery and research-state update

对于实质性的新证明项目，A/B/C 都是工作流的一部分。对于续做任务，未变更的主张可复用已完成的检查；受影响的主张则应重新检查。小型常规形式化所需的检查应与实际主张相称；用户明确要求跨模型系列审查时，也仍须满足这一要求。

使用当前宿主环境中获准的审查者模型系列。如果用户同时指定 Grok 和 Gemini，则必须获取并记录两者；同系列 Agent 或其他提供方不能在未说明的情况下替代任何一项。若某个选项不可用，该检查点保持待处理状态，同时继续独立的证明工作。通过检查的定理与完整完成所请求的审查工作流是两项独立的交付成果。

范围与入口

遵循用户要求的范围：实现、续做、审计或打包。审计时应检查并报告，不要悄悄修复或弱化定理。实现时，既要发展数学论证，也要完成 Lean 证明：检索相关文献或库中已有结果，探索替代路径，并补全缺失的引理。继续完成剩余接口和顶层组装；不要止步于目标声明或首次成功编译。

阅读权威陈述、现有 Lean 入口、工具链和锁文件，以及最新的进度记录。沿用项目及其文档名称。现有环境适用时，不要重新安装工具、更改依赖项或启动新的证明框架。根据固定版本的库确认 API。

现有证明路线可行时，应沿用它。如果数学论证本身缺失，则隔离该义务，并使用 proof-writer 或常规证明工作。委派给 proof-writer 的任务负责发展该论证，并将证明或剩余缺口返回本次运行；不得再次调用 lean-formalize。语法自动化不能证明尚未证明的前提。不要承诺可以形式化或解决任意开放问题。

开始或继续正确的工作

当前输入	首个有用操作
只有数学陈述	修正定义和量词，然后制定证明路线及其首个难点
文字证明	识别非平凡的依赖关系并选择 Lean 表示；在编写代码前指出任何缺失的论证
部分 Lean 项目	检查目标及其实际调用方，阅读最近有用的构建／错误记录，并从尚未闭合的最高层连接处继续
审计请求	阅读定义和导出类型，运行适用的检查并报告；不要暗中修复目标
准备交接的已完成证明	检查当前入口点和证据，然后准备可移植的源文件和命令，不要重新开始数学探索

尽早说明预期的主模块、导出声明和当前的下一项义务。如果尚无完整的数学路线，请说明正在尝试证明哪个陈述；不要仅仅因为实现已经开始，就宣称它可证。工具／API 问题和数学论证缺失需要采取不同的后续步骤。

1. 在实现之前明确含义

记录简短的数学规格，或引用现有规格：

• 对象、定义域、量词、原始假设和结论。
• 便捷表示与原始对象之间的等价关系。
• 用户对计算、外部证书和逻辑基础的约束。
• 用于表达并证明结果的 Lean 声明。

区分原始假设与通过归约引入的性质。指出有限性、非空性、可判定性、规范化和索引约定在何处改变了陈述，或需要衔接论证。检查实际定理中可能出现的空泛情况和量词错误，而不是凭空提出无关的边界情况。

在用户更改目标之前，始终以用户的原始陈述作为比较基准。为匹配实现而改写工作规格，并不会改变该基准。明确记录经授权的范围变更；对于本会话中已获授权的变更，不要再次请求确认。如果修复只得到更强的假设或更弱的结论，请指出已证明的变体，以及仍未解决的原始义务。若能补上蕴含关系，更强的已证明结果也可以确立原始主张。

针对实际定义体和拟议目标运行检查点 A。请独立地将其回译后，再与原始数学内容进行比较。输入材料包和提示词见 references/adversarial-review.md。只看过预期文字的审阅者，并未检查其编码。

2. 设计连接，再构建有用的部分

梳理从任意原始输入到结论的路径。对于每个重要接口，记录：

声明 / 义务	所作的假设	实际输入的来源	证据 / 剩余缺口
一个条件结果	它的额外假设	原始输入中的一个命名构造或定理	当前实际情况

优先处理尚未闭合的最高优先级连接。具体而言，要区分：

1. 一个公式或证书计算出所需的数值。
2. 实际的数学对象实现了该公式或证书。
3. 计算出的事实推出原始结论。

这三者可能都需要单独证明。若某个结构将所需性质存储为字段、直接给出概率界，或假设等价于结论，都不能免除构造该输入的义务。

将条件引理作为开发接口，并明确标记为此类引理。将未完成的实验放在经认证目标的依赖链之外；任何临时的 sorry 都必须保持可见，作为未完成工作，且不能通过最终目标审计。应进行足够的中间编译，以便定位错误，但不要把文件数量或已证明的算术命题视为工作已完成。

按稳定的引理签名和模块所有权拆分并行工作。向每位工作者提供其假设、结论、依赖项和具体编译目标。在关闭工作台账之前，将其结果与实际调用方集成并验证。不要让并行工作者为了适配自己的证明而暗中重新定义共享对象。

实现循环

实现或修复义务时，请阅读 references/lean-working-loop.md。该文档介绍了搜索 → 实际调用方实验 → 诊断 → 修复循环，涵盖表示方式的选择和性能问题，并附有一个已编译的库应用示例。

1. 选择一个缺失的连接或数学引理，确保它能改变主定理可证明的内容。明确写出其 Lean 接口以及调用方的义务。
2. 在固定版本的库和项目中查找所需结果。使用 #check 在本地测试不熟悉的声明；当现有等价表示能解决实际瓶颈时，就使用它。
3. 实现引理并补上实际调用点。编译受影响的模块；集成后，编译状态依赖于该模块的下游目标。
4. 诊断第一个相关错误。 elaboration/API 不匹配需要通过本地实现修复；假设不可用则需要推导该假设、改用其他论证，或明确列出尚待解决的数学义务。
5. 当有限归约变得耗时时，可以考虑通用计数引理、递推关系或更小的已检查证书。切勿仅为让 tactic 完成而暗中扩大信任基础。
6. 在新的承重论证或接口处运行检查点 B。实施有效修复并编译，然后针对已变更的义务请求后续跟进。
7. 更新现有台账，记录声明、实际调用方、验证证据和剩余前提，然后继续处理下一个连接。

例如，类型为 Certificate x → Desired x 的定理，只有在项目能为所需的每个原始输入构造 Certificate x 时才有用。完成该构造并连接调用方，与证明这个条件定理是两项不同的结果。内核检查不会仅仅因为某个参数的类型名称听起来可靠，就自动解除该参数。

不要用计时器、反复运行没有变化的构建，或反复调用模型来替代进展。遇到具体失败后，尝试其他有依据的表示方式或证明路径；如果请求的工作暂时无法完成，就保留确切的阻碍。区分实现失败、中间结论失败和整个方法遇到的障碍。应说明理由并放弃未成功的路径；否定该路径并不能反驳原始定理。若并行探索的方案可能因不同原因失败，这种探索最有价值。

3. 使用带有已证明解释的计算

区分有限示例、在已证明定义域上的穷举计算、已检查证书，以及符号或一般性证明。有限范围内的搜索只能作为对其搜索输入的证据。若覆盖范围、编码对应关系和验证过程都已确立，且符合用户的约束，那么穷举有限验证可以构成证明。要得到端到端的 Lean 结果，覆盖范围和解释本身必须位于声明的基础之下、已证明的依赖链中。注释声称有限列表是穷尽的，并不会让已检查的列表项变成 Lean 的全称定理。

对于数值论证，凡是结论要求精确时，都应使用精确算术。使用数值结论前，先证明实际对象或事件与有限数据之间的对应关系。记录相关约定：有序对还是无序对、重数、索引、零的情形以及舍入方式。

根据规范和项目惯例，就预期的信任基础达成一致。不要暗中引入公理或依赖编译器的计算，让原本不完整的内核级证明看起来完整。反过来，也不要把某个项目禁止枚举或使用 native_decide 的规定，扩大成普遍禁令。说明任何额外的信任假设，以及它是否符合这项任务的要求。

4. 审查仍未确定的数学义务

按照核心工作流中的说明运行 A、B 和 C。阅读 references/adversarial-review.md，了解阶段 触发条件、源材料包、对抗性提示词、异议处理、恢复和停止规则。这些是数学检查， 不是对是否信任执行者摘要的投票。

使用 proof-checker 承担现有的 ARIS 证明审计／提交职责。此技能不会取代其工件或审阅者约定。由父级证明审计调用时，将已检查的范围和证据返回给该次运行；不要递归调用 proof-checker。独立的 Lean 任务不一定需要单独的论文审计工作流。在已安装的环境中，使用 research-review / auto-review-loop 进行有针对性的讨论和修复，并遵循当前宿主的审阅者路由。

直接咨询模型时，使用可用且已授权的工具，并遵循其实际约定。Grok 或 Antigravity MCP 咨询并不会自动成为 ARIS 审阅者叠加层。不要在可移植工作流中硬编码供应商是否可用、配额、重试次数、代理设置或特定模型。

提出具体问题：翻译此声明；证明这些调用方假设；为这个新引理寻找反例；检查此归约是否覆盖完整。保留原始回复、实际阅读／执行范围，以及执行者对每个问题的处理。模型意见一致不等于证明。同一系列模型的意见仍属暂定结论；跨系列意见是额外的审阅证据，而非数学真理的证明。

未阅读的工件、未获答复的问题、失败的调用或空回复，都不构成实质性的审阅结论。计划审阅不等于最终代码审阅；阅读现有日志不等于执行构建。保留实际检查过的声明／版本。仅在当前授权和提供方规则允许的范围内重试；后续成功后，不要将失败改写为通过。

通过具体推导、经验证的见证、修正或有充分理由的驳回来解决异议。保留尚未解决的争议。遵循已调用的 ARIS 循环自身的轮次／继续约定；不要在其外部再创建轮询循环。对于直接咨询，重新审查已变更的义务，并在问题解决或达到实际的可用性／预算限制时停止。尚未解决的数学问题仍处于开放状态；无法进行的所请求审阅仍处于待处理状态。审阅者评分和轮次耗尽都不能作为证明完成的规则。

主机执行与审查

阅读本地主机的审查者路由，了解当前的模型／推理力度策略和工具契约。使用此技能中的 A/B/C 数学数据包；它们不需要论文、发表评分或新的审查服务。对于委派的证明工作，请遵循适用的扇出约定，分配稳定的引理接口，并在各结果的实际调用方处完成整合。

在 Claude Code 上，使用主机的文件／Shell 工具处理 Lean，并使用 Agent 开展有价值的并行证明工作。默认审查者是 Codex MCP：使用明确的项目 cwd、只读沙箱，以及根据路由参考确定的模型／推理力度组合，启动 mcp__codex__codex。使用其已保存的会话标识和提示词，通过 mcp__codex__codex-reply 继续审查。为 A 和 C 启动全新上下文；B 的修复检查可以继续使用发现问题的审查者。请核实执行器／审查者所属的模型系列，不要假定每个运行此主线技能的主机都是 Claude。

对于每个 A/B/C 检查点，都要通过可选审查者确定所选路由。遵守明确的模型系列要求，并将未满足要求的检查点保持为待处理状态。Claude、Grok 和 Gemini 的直接传输方式，其文件访问和会话续接契约各不相同；使用这些方式时，请阅读审查传输说明。这些 Lean 咨询不会更改其他技能的审查后端或验收规则。

5. 验证实际的最终目标

准备最终构建、信任审计或可移植软件包时，请使用 references/verification-and-handoff.md。

交付完成后，需确立以下适用的证据。已证明的定理应与仍待完成的复现或审查要求区分开来：

• 命题已有证明： 检查导出声明的实际类型，而不是它使用的关键字。theorem、lemma 或 def 都可能提供目标命题的证明项。仅仅定义该命题、证明 P → P，或证明无关命题，都不能证明原始目标。
• 陈述一致性： 其展开后的类型和定义表达了原始主张；除非原始主张包含，否则不应留有任何需要用户提供的内部配置文件、证书有效性、覆盖范围或成功前提。
• 实际组装： 归约、分情况讨论、见证和回到原始结论的过程彼此衔接，且所有调用方假设都已得到处理。
• 已执行验证： 显式构建证明目标的模块，并输出其类型和传递依赖的公理。对于多模块项目，还要独立导入实际入口点以检查其导出结果。对于小型自包含文件，直接编译并输出类型和公理即可；不要仅为再创建一次导入而构建新项目。保存命令、退出状态和输出。成功构建了其他根模块并不算数。
• 信任核算： 目标的依赖链上不得存在 sorryAx 或未经批准的额外公理。请根据预期的基础解释实际依赖；所需列表不必与任何固定的公理名称集合完全一致。
• 可复现性： 保留相关源代码和固定版本的环境，并提供其他读者可以运行的命令。
• 所需审查： C 关注的是最终导出类型、定义体、公理输出和原始主张，而不是早期计划。请分别记录每位所需审查者的实质性意见，或说明其无法审查的情况。

这些检查能在既定基础下确立形式化结果。文字证明或 HTML 版本需要单独进行对应性检查；Lean 不会验证单独阐述中的每句话。即使形式化定理已检查完毕，明确要求的导入审计、外部复现或审查仍可能待完成。应如实报告缺失的证据，不要将其说成新发现的数学漏洞。

一个示例审计可以区分 available_interface : Target → Target 和 original_proof : Target，即使二者编译时都没有额外公理。前者并未解决原始主张；如果 Target 与用户的陈述一致，后者则提供了该主张的证明。审查者调用失败不会改变二者的类型。

6. 持久化并移交实际获得的证据

复用现有的规格说明、证明台账和续接文件。简短的进度报告，加上 Lean 源码、锁文件、审计入口和日志，通常就足够了。只有在读者或执行方面确有具体需求时，才添加新文件。

报告不同的事实，不要只给出含糊的“通过”：

• 原始定理：已核验、部分完成、仅变更了主张，或已由经核验的反例证伪；注明声明名称及任何尚未履行的义务。
• 陈述对齐情况以及实际的逻辑信任依据。
• 复现情况：实际发生的是现有构建／增量构建、干净的项目重建，还是他人的独立复现。
• 审查情况：谁阅读了什么、谁运行了代码，以及任何仍待完成的审查请求。

对于尚未完成的工作，保存最小的剩余数学／Lean 义务、已知依赖项、最后一个有用的错误，以及下一步行动。对于已完成的工作，记录完成情况，避免下一次会话重新提出已过时的缺口。

使用简洁的续接说明，而不是再建一套状态系统：

Original target and source:
Current exported declaration / main module:
Closed connections and actual build evidence:
Next unclosed obligation or completion:
A/B/C reviews: source scope, reviewer, raw record, remaining issue:
Next action:

依据实际工件确定当前状态，不要依赖旧叙述中“已完成”或“尚未完成”的说法。恢复工作时，先检查有哪些变化，再决定是否重复工作。不要把历史审查范围和当前审查范围合并，形成范围更大的审计声明。

如果正在使用研究维基，请通过现有的 research-wiki / proof-checker 工作流，基于精确的证据和范围更新受影响的主张；不要覆盖其生成的图谱，也不要另创一套验收格式。文献检索应当用于解决数学缺口、API 问题或查找相关先前成果，而不应成为一项无关的穷尽文献要求。

移交时，提供便于读者阅读的证明、源码、固定版本的依赖项、独立审计命令，以及已知的信任边界。如有助于制作单文件阅读版，可使用 render-html。数学源码变更需要进行适当的重建及陈述／公理检查。在 Markdown 或 HTML 中变更定理或假设，同样属于主张变更：应重新进行对齐检查，并重新执行受影响的审查。保持主张不变的布局或措辞调整，只需进行呈现检查。在研究记录中保留变更历史，并直接呈现完成的证明。不要仅为遵循工作流仪式而重启已完成的证明工作。