⚡

证明Skill prove

这是一个机器辅助定理证明的技能，使用Lean4和Mathlib进行正式验证，通过五阶段工作流程（研究、设计、测试、实现、验证）帮助数学家快速生成机器验证的证明，无需学习复杂语法。关键词：定理证明、数学验证、Lean4、Mathlib、AI辅助、形式化方法、研究工具、测试验证。

论文写作 0 次安装 0 次浏览 更新于 3/14/2026

name: 证明 description: 具有研究、测试和验证阶段的正式定理证明 triggers: [“prove”, “verify”, “show that”, “is it true”, “formalize”] allowed-tools: [Bash, Read, Write, Edit, WebSearch, WebFetch, AskUserQuestion, Grep, Glob] priority: high

/prove - 机器验证证明（五阶段工作流程）

面向不想学习Lean语法的数学家的验证证明。

先决条件

在使用此技能前，检查Lean4是否已安装：

# 检查lake是否可用
command -v lake &>/dev/null && echo "Lean4已安装" || echo "Lean4未安装"

如果未安装：

# 安装elan（Lean版本管理器）
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# 重启shell，然后验证
lake --version

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

使用方法

/prove 每个群同态保持单位元
/prove Monsky定理
/prove 紧集上的连续函数一致连续

五阶段工作流程

┌─────────────────────────────────────────────────────────────┐
│  📚 研究 → 🏗️ 设计 → 🧪 测试 → ⚙️ 实现 → ✅ 验证  │
└─────────────────────────────────────────────────────────────┘

阶段1：研究（在任何Lean代码之前）

目标： 理解是否可以以及如何形式化。

  1. 使用Loogle搜索Mathlib（主要 - 类型感知搜索）

    # 使用loogle进行类型签名搜索 - 通过形状查找引理
loogle-search "pattern_here"

# 示例：
loogle-search "Nontrivial _ ↔ _"           # 查找Nontrivial引理
loogle-search "(?a → ?b) → List ?a → List ?b"  # 类似映射的函数
loogle-search "IsCyclic, center"           # 多个概念

    查询语法：

    • _ = 任何单个类型
    • ?a, ?b = 类型变量（相同变量表示相同类型）
    • Foo, Bar = 必须同时提及

  2. 外部搜索 - 已知的证明策略是什么？

    • 如果可用，使用Nia MCP：mcp__nia__search
    • 如果可用，使用Perplexity MCP：mcp__perplexity__search
    • 备用WebSearch搜索论文/参考资料
    • 检查：其他地方是否有现有形式化（Coq、Isabelle）？

  3. 识别障碍

    • 哪些引理不在Mathlib中？
    • 证明是否需要超出ZFC的公理？（选择公理、排中律等）
    • 陈述是否真的成立？（搜索反例）

  4. 输出： 证明策略和障碍的简要总结

检查点： 如果发现障碍，使用AskUserQuestion：

  • “这需要[X]。选项：(a) 限制版本，(b) 接受公理，© 中止”

阶段2：设计（带sorry的骨架）

目标： 在填充细节前构建证明结构。

  1. 创建Lean文件，包含：

    • 导入
    • 所需定义
    • 主定理陈述
    • 辅助引理作为sorry

  2. 注释每个sorry：

    -- SORRY: 需要证明（直接）
-- SORRY: 需要证明（复杂 - 约50行）
-- AXIOM CANDIDATE: v₂约束 - 将在阶段3测试

  3. 验证骨架编译（带sorry）

输出： proofs/<theorem_name>.lean带注释的结构

阶段3：测试（反例搜索）

目标： 在尝试证明前捕捉错误引理。

对于每个AXIOM CANDIDATE sorry：

  1. 生成测试用例

    -- 创建#eval或example语句
#eval testLemma (randomInput1)  -- 应返回true
#eval testLemma (randomInput2)  -- 应返回true

  2. 运行测试

    lake env lean test_lemmas.lean

  3. 如果找到反例：

    • 报告反例
    • 使用AskUserQuestion：“引理是假的。选项：(a) 限制域，(b) 重新表述，© 中止”

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

阶段4：实现（填充sorry）

目标： 完成证明。

标准迭代循环：

  1. 选择一个sorry
  2. 编写证明尝试
  3. 编译器在环检查（自动触发钩子）
  4. 如果错误，Godel-Prover建议修复
  5. 迭代直到sorry被填充
  6. 重复所有sorry

活动工具：

  • 编译器在环钩子（每次写入时）
  • Godel-Prover建议（错误时）

阶段5：验证（审计）

目标： 确认证明质量。

  1. 公理审计

    lake build && grep "depends on axioms" output
    • 标准：propext, Classical.choice, Quot.sound ✓
    • 自定义公理：列出每一个

  2. Sorry计数

    grep -c "sorry" proofs/<file>.lean
    • 必须为0以表示“完整”证明

  3. 生成总结

    ✓ 机器验证（或 ⚠️ 部分 - N公理）

定理：<陈述>
证明策略：<简要描述>

已证明：
- <引理1>
- <引理2>

公理化（如果有）：
- <公理>：<为什么需要>

文件：proofs/<名称>.lean

研究工具优先级

使用任何可用的工具，按顺序：

工具 最适合 命令
Loogle 类型签名搜索（主要） loogle-search "pattern"
Nia MCP 库文档 mcp__nia__search
Perplexity MCP 证明策略、论文 mcp__perplexity__search
WebSearch 一般参考资料 WebSearch工具
WebFetch 特定论文/页面内容 WebFetch工具

Loogle设置： 需要~/tools/loogle带Mathlib索引。运行loogle-server &进行快速查询。

如果无搜索工具可用，谨慎进行并注明“研究阶段跳过”。

检查点（自动）

工作流程在以下情况暂停用户输入：

  • ⚠️ 研究发现障碍
  • ❌ 测试发现反例
  • 🔄 实现遇到N次尝试后无法填充的sorry

输出格式

┌─────────────────────────────────────────────────────┐
│ ✓ 机器验证                                          │
│                                                     │
│ 定理：∀ φ : G →* H, φ(1_G) = 1_H                  │
│                                                     │
│ 证明策略：直接应用                                 │
│ MonoidHom.map_one 来自 Mathlib.                    │
│                                                     │
│ 阶段：                                              │
│   📚 研究：在 Mathlib.Algebra.Group.Hom 中找到    │
│   🏗️ 设计：单个引理，无需sorry                     │
│   🧪 测试：不适用（平凡）                          │
│   ⚙️ 实现：3行                                    │
│   ✅ 验证：0自定义公理，0 sorry                    │
│                                                     │
│ 文件：proofs/group_hom_identity.lean               │
└─────────────────────────────────────────────────────┘

我可以证明什么

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

限制

  • 复杂证明可能需要多次迭代
  • 新颖的研究级证明可能超出能力范围
  • 一些陈述在ℚ上不可证（需要ℝ扩展）

幕后

  • Lean 4.26.0 - 定理证明器
  • Mathlib - 100K+ 形式化定理
  • Godel-Prover - AI战术建议（通过LMStudio）
  • 编译器在环 - 每次写入时自动验证
  • 研究工具 - Nia、Perplexity、WebSearch（优雅降级）

另请参阅

  • /loogle-search - 通过类型签名搜索Mathlib（在阶段1研究中使用）
  • /math-router - 用于计算（积分、方程）
  • /lean4 - 直接Lean语法访问