Back to Details

prove

Compare original and translation side by side

🇺🇸

Original

English
🇨🇳

Translation

Chinese

/prove - Machine-Verified Proofs (5-Phase Workflow)

/prove - 机器可验证证明（5阶段工作流）

For mathematicians who want verified proofs without learning Lean syntax.
面向无需学习Lean语法即可获取可验证证明的数学家。

Prerequisites

前置条件

Before using this skill, check Lean4 is installed:
bash
undefined
使用本技能前，请检查Lean4是否已安装：
bash
undefined

Check if lake is available

检查lake是否可用

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

**If not installed:**
```bash
command -v lake &>/dev/null && echo "Lean4 installed" || echo "Lean4 NOT installed"

**若未安装：**
```bash

Install elan (Lean version manager)

安装elan（Lean版本管理器）

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

Restart shell, then verify

重启Shell后验证

lake --version

First run of `/prove` will download Mathlib (~2GB) via `lake build`.
lake --version

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

Usage

使用方法

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

The 5-Phase Workflow

5阶段工作流

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

Phase 1: RESEARCH (before any Lean)

阶段1：研究（在使用Lean之前）

Goal: Understand if/how this can be formalized.
  1. Search Mathlib with Loogle (PRIMARY - type-aware search)
    bash
    # Use loogle for type signature search - finds lemmas by shape
loogle-search "pattern_here"

# Examples:
loogle-search "Nontrivial _ ↔ _"           # Find Nontrivial lemmas
loogle-search "(?a → ?b) → List ?a → List ?b"  # Map-like functions
loogle-search "IsCyclic, center"           # Multiple concepts
    Query syntax:
    • _
      = any single type
    • ?a
      , 
      ?b
      = type variables (same var = same type)
    • Foo, Bar
      = must mention both
  2. Search External - What's the known proof strategy?
    • Use Nia MCP if available: 
      mcp__nia__search
    • Use Perplexity MCP if available: 
      mcp__perplexity__search
    • Fall back to WebSearch for papers/references
    • Check: Is there an existing formalization elsewhere (Coq, Isabelle)?
  3. Identify Obstacles
    • What lemmas are NOT in Mathlib?
    • Does proof require axioms beyond ZFC? (Choice, LEM, etc.)
    • Is the statement even true? (search for counterexamples)
  4. Output: Brief summary of proof strategy and obstacles
CHECKPOINT: If obstacles found, use AskUserQuestion:
  • "This requires [X]. Options: (a) restricted version, (b) accept axiom, (c) abort"
目标： 理解该定理是否可形式化、如何形式化。
  1. 使用Loogle搜索Mathlib（首选 - 类型感知搜索）
    bash
    # 使用loogle进行类型签名搜索 - 根据形式查找引理
loogle-search "pattern_here"

# 示例：
loogle-search "Nontrivial _ ↔ _"           # 查找Nontrivial相关引理
loogle-search "(?a → ?b) → List ?a → List ?b"  # 类Map函数
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. 输出： 证明策略和障碍的简要总结
检查点： 若发现障碍，将向用户提问：
  • "此证明需要[X]。选项：(a) 限制命题范围，(b) 接受公理，(c) 终止任务"

Phase 2: DESIGN (skeleton with sorries)

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

Goal: Build proof structure before filling details.
  1. Create Lean file with:
    • Imports
    • Definitions needed
    • Main theorem statement
    • Helper lemmas as 
      sorry
  2. Annotate each sorry:
    lean
    -- SORRY: needs proof (straightforward)
-- SORRY: needs proof (complex - ~50 lines)
-- AXIOM CANDIDATE: v₂ constraint - will test in Phase 3
  3. Verify skeleton compiles (with sorries)
Output: 
proofs/<theorem_name>.lean
with annotated structure
目标： 在填充细节之前搭建证明框架。
  1. 创建Lean文件，包含：
    • 导入语句
    • 所需的定义
    • 主定理命题
    • 以
      sorry
      暂代的辅助引理
  2. 为每个
    sorry
    添加注释：
    lean
    -- SORRY: 需要证明（简单直接）
-- SORRY: 需要证明（复杂 - 约50行）
-- AXIOM CANDIDATE: v₂约束 - 将在阶段3测试
  3. 验证框架可编译（包含sorry）
输出： 
proofs/<theorem_name>.lean
，带有注释的框架文件

Phase 3: TEST (counterexample search)

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

Goal: Catch false lemmas BEFORE trying to prove them.
For each AXIOM CANDIDATE sorry:
  1. Generate test cases
    lean
    -- Create #eval or example statements
#eval testLemma (randomInput1)  -- should return true
#eval testLemma (randomInput2)  -- should return true
  2. Run tests
    bash
    lake env lean test_lemmas.lean
  3. If counterexample found:
    • Report the counterexample
    • Use AskUserQuestion: "Lemma is FALSE. Options: (a) restrict domain, (b) reformulate, (c) abort"
CHECKPOINT: Only proceed if all axiom candidates pass testing.
目标： 在尝试证明之前找出错误的引理。
针对每个标记为AXIOM CANDIDATE的sorry：
  1. 生成测试用例
    lean
    -- 创建#eval或example语句
#eval testLemma (randomInput1)  -- 应返回true
#eval testLemma (randomInput2)  -- 应返回true
  2. 运行测试
    bash
    lake env lean test_lemmas.lean
  3. 若找到反例：
    • 报告反例
    • 向用户提问："引理不成立。选项：(a) 限制定义域，(b) 重新表述命题，(c) 终止任务"
检查点： 仅当所有候选公理通过测试后才继续。

Phase 4: IMPLEMENT (fill sorries)

阶段4：实现（填充sorry）

Goal: Complete the proofs.
Standard iteration loop:
  1. Pick a sorry
  2. Write proof attempt
  3. Compiler-in-the-loop checks (hook fires automatically)
  4. If error, Godel-Prover suggests fixes
  5. Iterate until sorry is filled
  6. Repeat for all sorries
Tools active:
  • compiler-in-the-loop hook (on every Write)
  • Godel-Prover suggestions (on errors)
目标： 完成证明。
标准迭代循环：
  1. 选择一个sorry
  2. 编写证明尝试
  3. 编译器实时检查（自动触发钩子）
  4. 若出现错误，Godel-Prover会提供修复建议
  5. 迭代直到sorry被填充
  6. 重复上述步骤直到所有sorry被填充
激活的工具：
  • 编译器实时钩子（每次写入时触发）
  • Godel-Prover错误建议（出现错误时）

Phase 5: VERIFY (audit)

阶段5：验证（审计）

Goal: Confirm proof quality.
  1. Axiom Audit
    bash
    lake build && grep "depends on axioms" output
    • Standard: propext, Classical.choice, Quot.sound ✓
    • Custom axioms: LIST EACH ONE
  2. Sorry Count
    bash
    grep -c "sorry" proofs/<file>.lean
    • Must be 0 for "complete" proof
  3. Generate Summary
    ✓ MACHINE VERIFIED (or ⚠️ PARTIAL - N axioms)

Theorem: <statement>
Proof Strategy: <brief description>

Proved:
- <lemma 1>
- <lemma 2>

Axiomatized (if any):
- <axiom>: <why it's needed>

File: proofs/<name>.lean
目标： 确认证明质量。
  1. 公理审计
    bash
    lake build && grep "depends on axioms" output
    • 标准公理：propext, Classical.choice, Quot.sound ✓
    • 自定义公理：逐一列出
  2. Sorry计数
    bash
    grep -c "sorry" proofs/<file>.lean
    • 若要标记为“完整”证明，计数必须为0
  3. 生成总结
    ✓ MACHINE VERIFIED（或⚠️ PARTIAL - N个公理）

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

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

公理化内容（若有）：
- <公理>：<使用原因>

文件：proofs/<name>.lean

Research Tool Priority

研究工具优先级

Use whatever's available, in order:
ToolBest ForCommand
LoogleType signature search (PRIMARY)
loogle-search "pattern"
Nia MCPLibrary documentation
mcp__nia__search
Perplexity MCPProof strategies, papers
mcp__perplexity__search
WebSearchGeneral referencesWebSearch tool
WebFetchSpecific paper/page contentWebFetch tool
Loogle setup: Requires 
~/tools/loogle
with Mathlib index. Run 
loogle-server &
for fast queries.
If no search tools available, proceed with caution and note "research phase skipped".
按以下优先级使用可用工具：
工具适用场景命令
Loogle类型签名搜索（首选）
loogle-search "pattern"
Nia MCP库文档查询
mcp__nia__search
Perplexity MCP证明策略、论文查找
mcp__perplexity__search
WebSearch通用参考文献WebSearch工具
WebFetch特定论文/页面内容WebFetch工具
Loogle设置： 需要在
~/tools/loogle
目录下有Mathlib索引。运行
loogle-server &
以实现快速查询。
若没有可用的搜索工具，请谨慎操作并标注“研究阶段已跳过”。

Checkpoints (automatic)

检查点（自动触发）

The workflow pauses for user input when:
  • ⚠️ Research finds obstacles
  • ❌ Testing finds counterexamples
  • 🔄 Implementation hits unfillable sorry after N attempts
当出现以下情况时，工作流将暂停并等待用户输入：
  • ⚠️ 研究阶段发现障碍
  • ❌ 测试阶段找到反例
  • 🔄 实现阶段经过N次尝试仍无法填充sorry

Output Format

输出格式

┌─────────────────────────────────────────────────────┐
│ ✓ MACHINE VERIFIED                                  │
│                                                     │
│ Theorem: ∀ φ : G →* H, φ(1_G) = 1_H                │
│                                                     │
│ Proof Strategy: Direct application of              │
│ MonoidHom.map_one from Mathlib.                    │
│                                                     │
│ Phases:                                             │
│   📚 Research: Found in Mathlib.Algebra.Group.Hom  │
│   🏗️ Design: Single lemma, no sorries needed       │
│   🧪 Test: N/A (trivial)                           │
│   ⚙️ Implement: 3 lines                            │
│   ✅ Verify: 0 custom axioms, 0 sorries            │
│                                                     │
│ File: proofs/group_hom_identity.lean               │
└─────────────────────────────────────────────────────┘
┌─────────────────────────────────────────────────────┐
│ ✓ MACHINE VERIFIED                                  │
│                                                     │
│ 定理：∀ φ : G →* H, φ(1_G) = 1_H                │
│                                                     │
│ 证明策略：直接应用Mathlib中的MonoidHom.map_one。                    │
│                                                     │
│ 阶段：                                             │
│   📚 研究：在Mathlib.Algebra.Group.Hom中找到相关内容  │
│   🏗️ 设计：单引理，无需使用sorry       │
│   🧪 测试：不适用（ trivial）                           │
│   ⚙️ 实现：3行代码                            │
│   ✅ 验证：0个自定义公理，0个sorry            │
│                                                     │
│ 文件：proofs/group_hom_identity.lean               │
└─────────────────────────────────────────────────────┘

What I Can Prove

可证明的领域

DomainExamples
Category TheoryFunctors, natural transformations, Yoneda
Abstract AlgebraGroups, rings, homomorphisms
TopologyContinuity, compactness, connectedness
AnalysisLimits, derivatives, integrals
LogicPropositional, first-order
领域示例
范畴论函子、自然变换、Yoneda引理
抽象代数群、环、同态
拓扑学连续性、紧性、连通性
分析学极限、导数、积分
逻辑学命题逻辑、一阶逻辑

Limitations

局限性

  • Complex proofs may take multiple iterations
  • Novel research-level proofs may exceed capabilities
  • Some statements are unprovable over ℚ (need ℝ extension)
  • 复杂证明可能需要多次迭代
  • 前沿研究级别的证明可能超出能力范围
  • 部分命题在ℚ上无法证明（需要扩展到ℝ）

Behind The Scenes

幕后技术

  • Lean 4.26.0 - Theorem prover
  • Mathlib - 100K+ formalized theorems
  • Godel-Prover - AI tactic suggestions (via LMStudio)
  • Compiler-in-the-loop - Automatic verification on every write
  • Research tools - Nia, Perplexity, WebSearch (graceful degradation)
  • Lean 4.26.0 - 定理证明器
  • Mathlib - 包含10万+形式化定理的库
  • Godel-Prover - AI策略建议工具（基于LMStudio）
  • 编译器实时检查 - 每次写入时自动验证
  • 研究工具 - Nia、Perplexity、WebSearch（支持优雅降级）

See Also

相关功能

  • /loogle-search
    - Search Mathlib by type signature (used in Phase 1 RESEARCH)
  • /math-router
    - For computation (integrals, equations)
  • /lean4
    - Direct Lean syntax access
  • /loogle-search
    - 按类型签名搜索Mathlib（用于阶段1研究）
  • /math-router
    - 用于计算（积分、方程求解）
  • /lean4
    - 直接使用Lean语法