prove

用途

prove 是一个机器验证证明（Machine-Verified Proofs）技能，面向希望获得经过形式化验证的证明、但不想学习 Lean 语法的数学家。它通过五阶段工作流，将自然语言描述的数学命题转化为 Lean 4 中可编译、可验证的证明文件。

前置条件

使用前需确认 Lean4 已安装：

command -v lake &>/dev/null && echo "Lean4 installed" || echo "Lean4 NOT installed"

若未安装，需先安装 elan（Lean 版本管理器）：

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

重启 shell 后验证：

lake --version

首次运行 /prove 会通过 lake build 下载 Mathlib（约 2GB）。

使用方式

以自然语言描述待证命题即可，例如：

/prove every group homomorphism preserves identity
/prove Monsky's theorem
/prove continuous functions on compact sets are uniformly continuous

五阶段工作流

工作流为：📚 RESEARCH → 🏗️ DESIGN → 🧪 TEST → ⚙️ IMPLEMENT → ✅ VERIFY。

阶段 1：RESEARCH（研究）

在编写任何 Lean 代码之前，先判断命题能否以及如何被形式化。

使用 Loogle 进行类型感知搜索（主要方式），例如：
```
loogle-search "Nontrivial _ ↔ _"
loogle-search "(?a → ?b) → List ?a → List ?b"
loogle-search "IsCyclic, center"
```
查询语法：_ 表示任意单一类型；?a、?b 为类型变量（同名即同类型）；Foo, Bar 表示必须同时提及。
搜索外部资料：若可用则使用 Nia MCP（mcp__nia__search）或 Perplexity MCP（mcp__perplexity__search），否则回退到 WebSearch 查找论文与参考文献。
检查是否已有其他形式化实现（Coq、Isabelle 等）。
识别障碍：Mathlib 中缺少哪些引理、证明是否需要 ZFC 之外的公理（选择公理、排中律等）、命题本身是否成立（搜索反例）。

输出：证明策略与障碍的简要总结。

检查点：若发现障碍，会通过 AskUserQuestion 询问，例如“这需要 [X]。选项：(a) 受限版本，(b) 接受公理，(c) 中止”。

阶段 2：DESIGN（设计）

在填充细节之前先搭建证明结构。创建 Lean 文件，包含导入、所需定义、主定理陈述，以及以 sorry 占位的辅助引理。每个 sorry 需标注，例如：

-- SORRY: needs proof (straightforward)
-- SORRY: needs proof (complex - ~50 lines)
-- AXIOM CANDIDATE: v₂ constraint - will test in Phase 3

验证骨架（含 sorry）可编译。输出：proofs/<theorem_name>.lean，带注释结构。

阶段 3：TEST（测试）

在尝试证明之前先捕获错误的引理。对每个 AXIOM CANDIDATE 的 sorry 生成测试用例，例如：

#eval testLemma (randomInput1)  -- should return true
#eval testLemma (randomInput2)  -- should return true

运行测试：

lake env lean test_lemmas.lean

若发现反例，报告反例并通过 AskUserQuestion 询问：“引理为假。选项：(a) 限制定义域，(b) 重新表述，(c) 中止”。

检查点：仅当所有公理候选通过测试后才继续。

阶段 4：IMPLEMENT（实现）

完成证明。标准迭代循环：选取一个 sorry → 编写证明尝试 → 编译器在环自动检查（hook 自动触发）→ 若出错，Godel-Prover 建议修复 → 迭代直到该 sorry 被填充 → 对所有 sorry 重复。

启用的工具：compiler-in-the-loop hook（每次 Write 时触发）、Godel-Prover 建议（出错时）。

阶段 5：VERIFY（验证）

确认证明质量。

公理审计：
```
lake build && grep "depends on axioms" output
```
标准公理为 propext、Classical.choice、Quot.sound；自定义公理需逐一列出。
sorry 计数：
```
grep -c "sorry" proofs/<file>.lean
```
完整证明必须为 0。
生成总结，标明 ✓ MACHINE VERIFIED 或 ⚠️ PARTIAL - N axioms，并列出定理、证明策略、已证引理、被公理化的内容（如有）及文件路径。

研究工具优先级

按可用性依次使用：Loogle（类型签名搜索，主要）、Nia MCP（库文档）、Perplexity MCP（证明策略、论文）、WebSearch（通用参考）、WebFetch（特定论文/页面内容）。Loogle 需 ~/tools/loogle 及 Mathlib 索引，运行 loogle-server & 可获得快速查询。若无搜索工具可用，则谨慎推进并注明“研究阶段已跳过”。

检查点（自动）

工作流在以下情况暂停等待用户输入：研究阶段发现障碍、测试阶段发现反例、实现阶段在 N 次尝试后仍无法填充某个 sorry。

输出格式

以框式摘要呈现，包含验证状态、定理陈述、证明策略、各阶段说明、自定义公理与 sorry 数量、文件路径。

可证明的领域

范畴论（函子、自然变换、Yoneda）、抽象代数（群、环、同态）、拓扑（连续性、紧致性、连通性）、分析（极限、导数、积分）、逻辑（命题逻辑、一阶逻辑）。

限制

复杂证明可能需要多次迭代；新颖的研究级证明可能超出能力范围；某些命题在 ℚ 上不可证（需要扩展到 ℝ）。

背后技术

Lean 4.26.0（定理证明器）、Mathlib（10 万+ 形式化定理）、Godel-Prover（通过 LMStudio 提供 AI 策略建议）、Compiler-in-the-loop（每次写入自动验证）、研究工具（Nia、Perplexity、WebSearch，优雅降级）。

技能介绍

用途