证明 SKILL

# Rocq-Grok 技能详解

Rocq-Grok 是一款面向 Rocq（原名 Coq）证明开发的智能代理技能包，为代理提供理解、构建、修复和审查证明的工作流程。适用于处理 `.v` 文件、`_CoqProject` 配置、定理陈述、证明目标、依赖类型、证明策略（tactic）失败、构建失败、以 `Admitted` 暂时跳过的证明义务、假设审计和反例等场景，也支持软件不变量、合约及新项目的形式化。

## 为什么需要这个技能？

AI 生成的数学手稿和候选证明需要核查其陈述、推导与假设。截至 2026 年 10 月 7 日，OpenAI 的 [openai/math 仓库](网页链接(github.com)按其 README 统计包含 722 篇数学手稿，归入 372 个成果家族。一个家族可以包含主要结果、配套论证、推论或其他证明。这些结果处于不同验证阶段，其中部分附有 Lean 形式化证明；README 也明确提示，部分未形式化结果可能存在问题。

另据[上海纽约大学 RITS 的报道](网页链接(rits.shanghai.nyu.edu)，OpenAI 于 2026 年 9 月 8 日公布了关于纳维–斯托克斯方程在平滑外力条件下出现有限时间奇性的证明主张及 Lean 形式化材料。这与十月的批量手稿发布是不同事件。引用这类成果时，应区分发布者的主张、机器检查的精确命题和数学审查结论。

对 Rocq/Coq 项目，Rocq-Grok 可协助挑战陈述的边界案例、分解证明义务、审计假设，并对编译产物中的证明进行类型检查。这些步骤为精确形式命题在记录的环境和允许假设下成立提供证据；形式命题是否忠实表达原始主张仍需单独审查。有限范围内未找到反例，也不等于已经证明。

## Lean、Rocq 与 Rocq-Grok 的关系

- **Lean**：编程语言与定理证明器，支持依赖类型、数学形式化和软件验证。其用途可参见[官方学习页](网页链接(lean-lang.org)。
- **Rocq**：编程语言与定理证明器，同样支持依赖类型、数学形式化和软件验证。[官网](网页链接(rocq-prover.org)列举了 Mathematical Components、CompCert 等项目。

Rocq-Grok 是面向 Rocq/Coq 工具链的代理技能，使用 `rocq compile`、`rocq check`、`Print Assumptions` 等工具组织证明开发与核查。选择 Lean 或 Rocq 时，应考虑已有代码、所需库、团队经验和项目验收要求。

Lean 材料应按其项目的 Lean 工具链和审计流程验证；例如 OpenAI 仓库提供了自己的 [Comparator 检查说明](网页链接(github.com)。本技能规定的 Rocq/Coq 流程不能直接核验 Lean 产物。若要在 Rocq 中复核同一结果，需要另行转写、重新证明，并核对两边的定义、命题和假设是否对应。

## 能在全栈开发中使用吗、什么价值、如何用？

### 能在全栈开发中使用吗？

能用，但只覆盖全栈里需要形式化的那一层规则，不替代前端、后端、数据库、测试和部署。没有 `.v` 文件也可以开始：先从一条跨层规则做最小模型。普通页面、接口 500、SQL 和发布，只要没有形式化目标，就不要因为文档里出现“状态机”或“API 合约”就启动这个技能。

| 全栈位置 | 可以形式化的目标 | 仍用工程工具做的事 |
|---|---|---|
| 前端表单与状态 | 数量、金额、状态是否满足前置条件 | 组件、交互、样式、浏览器兼容 |
| API 合约 | 请求域、成功/失败、前置与后置条件 | 路由、鉴权中间件、超时、未建模的序列化 |
| 后端业务 | 转账守恒、退款上限、订单状态机 | 框架、ORM、日志、性能 |
| 前后端交接 | 客户端校验与服务器判定是否同一含义 | 联调、集成测试、线上排障 |

内存安全、并发和权限也可以成为目标，但必须单独建模。一条业务规则的证明，不自动覆盖空指针、竞态或接口 500。

### 什么价值？

全栈里同一条规则常散在前端校验、API 文档和后端分支里。单测覆盖有限，可能漏掉边界或状态组合。Rocq-Grok 可协助把这条规则表达成可检查的命题，明确其适用条件。

- **对齐跨层含义。** 数量为正、金额不为负、“已发货必已支付”这类话，先对到量词、类型和边界，再看前端与后端是否在说同一件事。
- **检查可能漏测的边界。** 用 `nat` 表示余额时，`0 - 1 = 0`。若按 `b1 - a` 和 `b2 + a` 更新余额，未经余额检查的转账可能破坏守恒，例如两个零余额账户转账 1 后变成 0 和 1。实付 100、已退 60 后再走“全额退款”，要先定义退的是 100 还是剩余 40，并确认操作是否会被接受，才能判断是否超退。
- **审查重构和 AI 草稿。** 编译通过不等于契约还在。`Print Assumptions` 能列出目标依赖的全局假设，包括由 `Admitted` 引入的依赖；其输出本身不能区分该依赖源于 `Axiom` 还是 `Admitted`，仍需查看源码。定理类型中的显式前提也要单独检查，即使输出为 `Closed under the global context`。固定契约不能为了证过而偷偷加前提或改窄域。
- **价值有边界。** `KERNEL-CHECKED` 只说明：这条形式命题在记录的假设、工具链和信任政策下成立。它不证明前端、API 和数据库照做了。对应关系要单独复查；单测、集成测试和线上排障照旧。

### 如何用？

1. **只抽一条跨层规则。** 写下完整命题、量词顺序、定义域、允许和禁止的假设，并记下没有建模的部分（手续费、重试、溢出、并发、持久化）。已定死的陈述、定义和签名不要偷偷改。
2. **先探环境。** 从技能目录运行：
   ```bash
   python3 scripts/check_env.py --json
   ```
   脚本只探测 PATH 上的工具和版本。项目钉死的版本、导入、逻辑路径和构建入口仍要查配置与 CI。工具缺失时继续阅读和陈述分析，把未执行的检查标成“未运行”。
3. **先挑战陈述，再投入证明。** 查零、空对象、边界、截断减法和量词顺序。搜索已有引理，核对候选签名。精确反例只推翻对应的候选表述；没找到反例不等于证明。
4. **一小步一检查。** 先攻最硬的子目标。每步看真实 goal 和诊断。`Admitted` 只当草稿，依赖它的结果保持 `DRAFT`。复杂或多文件任务用 `assets/proof-record.md`。
5. **收尾过三关。** 用项目入口重编当前源码、必要依赖和受影响的调用方；检查目标的完整类型，执行 `Print Assumptions` 并对照允许的假设；对新的完整 `.vo` 做 `rocq check` 或 `coqchk`。检查器接受公理声明，因此产物检查成功不能代替假设审计。编辑器通过、旧产物或 `-vos` / `-vok` 不能当最终证据。按验收结果标为 `DRAFT`、`BLOCKED`、`REFUTED` 或 `KERNEL-CHECKED`；这些是技能自定义的状态，不是 Rocq 内置状态。
6. **映回全栈实现。** 对照前端校验、API 分支和持久化是否满足同样的前提、类型和状态迁移。模型里的精确反例可以引导回归测试，但要先确认代码确实允许同一行为。不要自动提交或改用户固定契约。

完成时报告：改了哪些文件和目标、精确陈述、构建与检查命令及结果、假设审计、审过的调用方，以及模型覆盖了全栈的哪一层。形式化只回答“在记录假设下是否成立”；业务代码和测试仍然要写。

## 这可以证明？我也要证明吗？

软件工程黑色幽默。四个角色，一句「证明」，四种意思。

产品指着流程图：「已发货必已支付，这还用证？」
测试把 CI 转过来：「全绿。这可以证明。」
模型说：「候选证明已生成。」
写业务的人把椅子往后挪了半寸：「……我也要证明吗？」

没有人在开玩笑，也没有人在说同一件事。产品要的是散会；测试展示的是已执行用例的结果；模型交出的候选证明可能仍含 `Admitted`。内核检查通过，表示形式证明符合相应环境中的类型规则；还要审计假设，才能说明结论成立的条件。前端、接口和数据库是否遵循同一模型，也要另查。

黑的是最后半寸。椅子往后挪，不能当 `Qed`。不想证，就标 `DRAFT`；别把「这可以证明」写成已经证明。