mcpField
P
prove

prove

github.com/parcadeiその他3.9k508 回インストール39 週間前に更新
リポジトリ

prove について

proveは、Leanの構文を学ばずに機械検証可能な証明を求める数学者向けのスキルです。調査、設計、テスト、実装、検証の5段階で定理証明を進めます。

主な機能

  1. 015段階の証明ワークフロー
  2. 02Mathlibと外部資料の検索
  3. 03反例のテスト
  4. 04Lean証明の実装
  5. 05公理とsorryの監査

活用シーン

  1. 01代数の定理の形式化
  2. 02補題案の反例チェック
  3. 03Lean証明の公理依存の監査

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 ファイルを作成します：

    • インポート
    • 必要な定義
    • 主定理の命題
    • 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（sorry を埋める）

目標： 証明を完成させます。

標準的な反復ループ：

  1. sorry を 1 つ選ぶ
  2. 証明を試みる
  3. コンパイラーを使った反復チェック（フックが自動的に実行されます）
  4. エラーが発生した場合、Godel-Prover が修正案を提案します
  5. sorry が埋まるまで反復します
  6. すべての sorry について繰り返します

有効なツール：

  • コンパイラーを使った反復フック（すべての 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               │
└─────────────────────────────────────────────────────┘

私が証明できること

分野例
圏論関手、自然変換、米田
抽象代数学群、環、準同型
位相幾何学連続性、コンパクト性、連結性
解析学極限、導関数、積分
論理学命題論理、一階論理

制限事項

  • 複雑な証明には複数回の反復が必要になる場合があります
  • 新規の研究レベルの証明は能力の限界を超える場合があります
  • ℚ 上では証明できない命題もあります（ℝ への拡張が必要です）

裏側の仕組み

  • Lean 4.26.0 - 定理証明器
  • Mathlib - 10万件以上の形式化された定理
  • Godel-Prover - AI による戦術の提案（LMStudio 経由）
  • コンパイラー・イン・ザ・ループ - 書き込みのたびに自動検証
  • リサーチツール - Nia、Perplexity、WebSearch（機能が低下した場合も適切に対応）

関連項目

  • /loogle-search - Mathlib を型シグネチャで検索します（フェーズ 1 のリサーチで使用）
  • /math-router - 計算（積分、方程式）に使用します
  • /lean4 - Lean の構文に直接アクセスします

コメント

Markdown 対応