mcpField
P
prove

prove

github.com/parcadei其他3.9k508 次安装39 周前更新
代码仓库

关于 prove

prove 面向希望获得机器验证证明、但不想学习 Lean 语法的数学家，按研究、设计、测试、实现和验证五个阶段推进定理证明。

主要功能

  1. 01五阶段证明工作流
  2. 02搜索 Mathlib 与外部资料
  3. 03反例测试
  4. 04实现 Lean 证明
  5. 05检查公理与 sorry

适用场景

  1. 01形式化代数定理
  2. 02为候选引理查找反例
  3. 03审计 Lean 证明中的公理依赖

MCP 相关

工作流可在可用时调用 Nia MCP 和 Perplexity MCP，搜索库资料与证明策略。

安装

复制下面的命令，在终端中运行。

$npx skills add https://github.com/parcadei/continuous-claude-v3 --skill prove

安装后在 Claude Code 中输入/prove确认已加载。

详细介绍

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

适合想要经过验证的证明、但不想学习 Lean 语法的数学家。

前提条件

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

# Check if lake is available
command -v lake &>/dev/null && echo "Lean4 installed" || echo "Lean4 NOT installed"

如果尚未安装：

# Install elan (Lean version manager)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# Restart shell, then verify
lake --version

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

用法

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

5 阶段工作流

┌─────────────────────────────────────────────────────────────┐
│  📚 RESEARCH → 🏗️ DESIGN → 🧪 TEST → ⚙️ IMPLEMENT → ✅ VERIFY  │
└─────────────────────────────────────────────────────────────┘
阶段 1：RESEARCH（编写任何 Lean 代码之前）

**目标：**了解此内容是否能形式化，以及如何形式化。

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

    # 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

    查询语法：

    • _ = 任意单一类型
    • ?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）接受公理，（c）中止”
阶段 2：DESIGN（带有 sorry 的骨架）

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

  1. 创建 Lean 文件，包含：

    • Imports
    • 所需的定义
    • 主定理陈述
    • 以 sorry 标记的辅助引理

  2. 为每个 sorry 添加注释：

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

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

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

阶段 3：TEST（反例搜索）

**目标：**在尝试证明引理之前，找出错误的引理。

针对每个候选公理 sorry：

  1. 生成测试用例

    -- Create #eval or example statements
#eval testLemma (randomInput1)  -- should return true
#eval testLemma (randomInput2)  -- should return true

  2. 运行测试

    lake env lean test_lemmas.lean

  3. 如果发现反例：

    • 报告反例
    • 使用 AskUserQuestion：“引理不成立。选项：（a）限制定义域，（b）重新表述，（c）中止”

**检查点：**只有所有候选公理都通过测试后，才能继续。

阶段 4：IMPLEMENT（填充 sorries）

**目标：**完成证明。

标准迭代循环：

  1. 选择一个 sorry
  2. 编写证明尝试
  3. 在编译器中循环检查（钩子自动触发）
  4. 如果出错，Godel-Prover 会提出修复建议
  5. 迭代，直到填充该 sorry
  6. 对所有 sorries 重复以上步骤

启用的工具：

  • 编译器中循环检查钩子（每次 Write 时触发）
  • Godel-Prover 建议（出错时触发）
阶段 5：VERIFY（审查）

**目标：**确认证明质量。

  1. 公理审查

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

  2. Sorry 计数

    grep -c "sorry" proofs/<file>.lean
    • 要称为“完整”证明，计数必须为 0

  3. 生成摘要

    ✓ 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

研究工具优先级

按以下顺序使用可用工具：

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

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

如果没有可用的搜索工具，请谨慎继续，并注明“已跳过研究阶段”。

检查点（自动触发）

在以下情况下，工作流会暂停并等待用户输入：

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

输出格式

┌─────────────────────────────────────────────────────┐
│ ✓ 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               │
└─────────────────────────────────────────────────────┘

我能证明的内容

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

局限

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

幕后技术

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

另请参阅

  • /loogle-search - 按类型签名搜索 Mathlib（用于第 1 阶段的 RESEARCH）
  • /math-router - 用于计算（积分、方程）
  • /lean4 - 直接访问 Lean 语法

评论

支持 Markdown