paperproof-validator

Lean 4 の形式的証明の可視化と検証

バージョン: 1.0.0 Trit: -1 (バリデーター - 証明の正当性を検証) バンドル: verification ステータス: ✅ 新機能 (Lean 4 定理証明の可視化) リポジトリ: Paper-Proof/paperproof

概要

Paperproof Validator は、形式的な Lean 4 の証明を直感的で紙面に近い可視化へと変換します。仮説とゴールが証明全体を通じてどのように進化するかを表示することで、抽象的な形式的証明と人間の理解の間のギャップを埋めます。

主な革新: 証明構造を紙上の数学記法と同じ方法で可視化することで、形式的証明をアクセスしやすくします。

Paperproof の機能

抽象的な Lean コードの代わりに:

theorem example : P → Q := by
  intro h
  apply some_lemma
  exact h.right

Paperproof は以下のように表示します:

┌─────────────────────────────────────┐
│ 仮説 (緑のノード):                  │
│  - h : P                            │
├─────────────────────────────────────┤
│ ゴール (赤のノード):                │
│  - Q                                │
├─────────────────────────────────────┤
│ タクティック (透過的):              │
│  - apply some_lemma                 │
│  - exact h.right                    │
└─────────────────────────────────────┘

アーキテクチャ

3 つのコアコンポーネント

1. Lean 4 ライブラリ統合

import Paperproof

theorem my_theorem : P ∧ Q → R := by
  -- Paperproof は証明状態を自動的に抽出します
  intro ⟨hp, hq⟩
  -- 可視化は仮説とゴールを追跡します
  exact some_proof_term

機能:

Lean 4 InfoTree と統合
各タクティックでの証明状態を抽出
VS Code 拡張機能に証明メタデータを提供

2. VS Code 拡張機能

責務:

カーソル位置を追跡 (可視化される定理を検出)
Lean サーバーと通信して証明データを取得
可視化用の Webview パネルをホスト
コマンドと設定を提供
Lean InfoTree を React フロントエンドにブリッジ

コマンド:

Paperproof: Open Paperproof Panel
Paperproof: Show Current Theorem
Paperproof: Export Proof as Image
Paperproof: Settings

アーキテクチャフロー:

ユーザーカーソルが定理上に
           ↓
選択変更イベント
           ↓
Lean サーバーから証明データをリクエスト
           ↓
Lean サーバーが InfoTree を返す
           ↓
BetterParser (構造を抽出)
           ↓
コンバーターサービス (可視化用に最適化)
           ↓
React フロントエンドに送信
           ↓
ビジュアル証明ツリーをレンダリング

3. React フロントエンド可視化

コンポーネント階層:

ProofTree (ルート)
├── GlobalContext プロバイダー
├── ヘッダー (タイトル、コントロール)
└── BoxEl (変数スコープコンテナ)
    ├── 仮説セクション
    │   └── HypothesisNode (緑)
    │       └── 透過度 = "スコープ内"
    ├── タクティックセクション
    │   └── TacticNode (透過的、破線枠)
    │       └── 関連ノードへの矢印
    └── ゴールセクション
        └── GoalNode (赤)

ビジュアルキュー:

仮説: 上部の緑ノード
ゴール: 下部の赤ノード
タクティック: 破線枠の透過ノード
スコープ: 背景が暗くなるネストされたボックス
利用可能性: ノード不透明度はスコープアクセス可能性を示します

機能

1. visualize-proof-structure

ビジュアルノードを備えた階層的ツリーとして証明を表示:

from paperproof_validator import PaperproofVisualizer

visualizer = PaperproofVisualizer(
    lean_file="example.lean",
    theorem_name="my_theorem"
)

# 証明を抽出してレンダリング
proof_visual = visualizer.visualize(
    show_hypotheses=True,
    show_goals=True,
    show_tactics=True,
    show_scopes=True
)

# 出力: インタラクティブな HTML/React 可視化

2. extract-proof-metadata

Lean InfoTree から構造化された証明情報を抽出:

-- Lean 4 コード
theorem and_comm (p q : Prop) : p ∧ q → q ∧ p := by
  intro ⟨hp, hq⟩      -- ステップ 1: intro は仮説を作成
  exact ⟨hq, hp⟩      -- ステップ 2: exact は証明項を提供

抽出された構造:

{
  "theorem": "and_comm",
  "steps": [
    {
      "tactic": "intro",
      "hypotheses": [
        {"name": "hp", "type": "p"},
        {"name": "hq", "type": "q"}
      ],
      "goals": [{"type": "q ∧ p"}]
    },
    {
      "tactic": "exact",
      "hypotheses": [
        {"name": "hp", "type": "p"},
        {"name": "hq", "type": "q"}
      ],
      "goals": []
    }
  ]
}

3. validate-proof-correctness

証明が予想される結論に到達することを検証:

validation = visualizer.validate_proof(
    expected_conclusion="Q"
)

if validation.passes:
    print("✓ 証明は Q を正しく確立しています")
else:
    print(f"✗ 証明は Q を確立していません")
    print(f"  最終ゴール: {validation.final_goal}")

4. analyze-tactic-effects

各タクティックが証明状態をどのように変換するかを表示:

analysis = visualizer.analyze_tactics()

for step in analysis.steps:
    print(f"\nタクティック: {step.name}")
    print(f"変更前の仮説: {step.hypotheses_before}")
    print(f"変更後の仮説: {step.hypotheses_after}")
    print(f"変更前のゴール: {step.goals_before}")
    print(f"変更後のゴール: {step.goals_after}")
    print(f"スコープ内の変数: {step.scope}")

5. support-multiple-proof-tactics

一般的な Lean 4 タクティックを処理:

-- apply: 仮説/補題を使用してゴールを変換
theorem proof_with_apply : P → Q := by
  intro hp
  apply lemma_p_implies_q
  exact hp

-- have: 中間的な仮説を導入
theorem proof_with_have : P → Q → R := by
  intro hp hq
  have h : X := lemma_from_p hp
  apply lemma_h_q_to_r h hq

-- induction: 帰納法で証明
theorem induction_proof : ∀ n, P n := by
  intro n
  induction n with
  | zero => exact base_case
  | succ k ih => exact inductive_step k ih

-- by_contra: 背理法で証明
theorem by_contra_proof : P := by
  by_contra hnp
  have : False := contradiction_from_not_p hnp
  exact absurd this (by simp)

-- cases: ケース分析
theorem cases_proof : P := by
  cases some_disjunction with
  | left h => exact left_proof h
  | right h => exact right_proof h

すべてのタクティックは証明状態の変換とともに可視化されます。

6. export-proof-visualization

静的またはインタラクティブな証明表現を生成:

# インタラクティブな HTML としてエクスポート
visualizer.export_html("proof.html")

# 静的画像 (PNG/SVG) としてエクスポート
visualizer.export_image("proof.png", format="png")

# LaTeX としてエクスポート (論文用)
visualizer.export_latex("proof.tex")

# JSON としてエクスポート (プログラマティック使用)
visualizer.export_json("proof.json")

Lean 4 エコシステムとの統合

インストール

# 1. VS Code 拡張機能をインストール
# VS Code の拡張機能経由: "Paperproof" で検索

# 2. Lean プロジェクトに追加 (lakefile.toml)
require paperproof from git
  "https://github.com/Paper-Proof/paperproof.git"

# 3. 更新
lake update

# 4. Lean ファイルでインポート
import Paperproof

Lean 4 での使用

import Paperproof

-- 定理を定義
theorem associativity : ∀ (a b c : Nat), (a + b) + c = a + (b + c) := by
  intro a b c
  -- カーソルがここにあるとき、Paperproof は以下を表示します:
  -- - 仮説: a : Nat, b : Nat, c : Nat
  -- - ゴール: (a + b) + c = a + (b + c)
  induction a with
  | zero =>
    -- Paperproof はベースケースのコンテキストを表示
    rfl
  | succ k ih =>
    -- Paperproof は帰納的ステップを表示
    -- - ih : (k + b) + c = k + (b + c) [帰納的仮説]
    simp [Nat.add_succ, ih]

形式的証明論の背景

証明ツリーと自然推論

Paperproof の可視化は自然推論システムに基づいています:

仮説 (コンテキスト)
───────────────────────
    | タクティックを適用
    | ゴールを変換
───────────────────────
    最終的な結論

ゲンツェン列計算との関連性

Paperproof は従来の証明可視化を最新の Web テクノロジーで拡張します:

従来のゲンツェン形式:

Γ ⊢ A    Γ ⊢ B
──────────────────
  Γ ⊢ A ∧ B

Paperproof 可視化:

Γ (仮説) をビジュアルに表示
ゴールを赤で表示
接続矢印を伴う証明ステップを表示
ネストされたボックスで変数スコープを示します

色の意味論

色	要素	意味
緑	仮説	スコープ内で利用可能な事実
赤	ゴール	証明するべきターゲット
透過	タクティック	証明ステップ (白ボックス)
濃い灰色	スコープ境界	変数スコープのネスト
不透明度	ノード表示	要素がスコープ内かどうか

GF(3) 統合

Trit 割り当て

Paperproof Validator: -1 (MINUS - 重要なバリデーター)

以下と均衡した三元組を形成できます:

潜在的な三元組 (形式的検証):

Trit	スキル	役割
-1	paperproof-validator	形式的証明を検証
0	proof-instrumentation	証明ステップを追跡
+1	theorem-generator	証明可能な定理を生成
合計	0 (mod 3)	✓ 保存される

他の証明ツールとの比較

vs. Lean ネイティブ REPL

側面	Lean REPL	Paperproof
可視化	テキストベース	ビジュアルツリー
スコープ追跡	暗黙的	明示的なボックス
学習曲線	急勾配	緩やか
理解	抽象的	直感的
アクセス可能性	エキスパートのみ	初心者向け

vs. タクティック状態ウィンドウ

タクティック状態 (生):

⊢ (0 + 0) + 0 = 0

Paperproof (ビジュアル):

┌─────────────────────────────┐
│ ゴール: (0 + 0) + 0 = 0     │
│ (simp の後)                 │
└─────────────────────────────┘

設定

# paperproof-validator.yaml
visualization:
  show_hypotheses: true
  show_goals: true
  show_tactics: true
  show_scopes: true
  show_arrows: true

rendering:
  color_scheme: dark        # または 'light'
  node_size: medium         # small, medium, large
  scope_nesting_depth: 5

export:
  formats: [html, png, svg, json, latex]
  include_metadata: true

lean_integration:
  lean_version: "v4.0.0"
  vscode_extension: true
  webview_enabled: true

ワークフロー例

# 1. 拡張機能をインストール
# VS Code の拡張機能を開き、"Paperproof" で検索して、インストールをクリック

# 2. Lean プロジェクトに追加
# lakefile.toml を編集して依存関係を追加

# 3. Lean ファイルにインポート
# 追加: import Paperproof

# 4. Paperproof パネルを開く
# Cmd+Shift+P → "Paperproof: Open Panel"

# 5. 定理をクリック
# エディター内の任意の 'theorem' または 'lemma' をクリック

# 6. 可視化を表示
# Paperproof がサイドパネルにインタラクティブな証明ツリーを表示

# 7. 証明をエクスポート
# Cmd+Shift+P → "Paperproof: Export Proof as Image"

技術的実装

BetterParser

Lean InfoTree (生の証明構造) を簡略された表現に変換:

Lean 4 InfoTree (複雑でネストされた)
        ↓
   BetterParser
        ↓
簡略化された証明構造 (クリーン)
        ↓
   コンバーター
        ↓
React フレンドリー形式
        ↓
ビジュアルレンダリング

コンバーターサービス

可視化用に証明構造を最適化:

# 入力: Lean InfoTree
lean_tree = {
  "kind": "Tactic",
  "name": "intro",
  "children": [...]
}

# コンバーターを通じて処理
visual_tree = convert_to_visual_format(lean_tree)
# 出力: { "type": "intro", "hypotheses": [...], "goals": [...] }

# React に渡す
render_to_webview(visual_tree)

VS Code 拡張機能通信

// VS Code 拡張機能 (TypeScript)
vscode.window.onDidChangeTextEditorSelection((e) => {
  const theorem_name = getSymbolAtCursor(e);

  // Lean サーバーから証明をリクエスト
  const proof_data = getLeanProofData(theorem_name);

  // webview に送信
  webview.postMessage({
    type: "updateProof",
    data: proof_data
  });
});

// React Webview がメッセージを受け取る
window.addEventListener("message", (event) => {
  if (event.data.type === "updateProof") {
    renderProofTree(event.data.data);
  }
});

学習リソース

実例:

「Mathematics in Lean 4」からの証明
Mathlib4 からの証明
The Hitchhiker's Guide to Logical Verification
Lean 4 チュートリアルとドキュメント

含まれるチュートリアル例:

自然推論証明
帰納的証明
背理法の証明
ケースバイケースの証明

開発

Paperproof は積極的に開発されており、貢献を歓迎します:

リポジトリ: GitHub - Paper-Proof/paperproof
問題と議論: 機能リクエストとバグレポートに対応
ライセンス: オープンソース (詳細はリポジトリを確認)

開発セットアップ

# リポジトリをクローン
git clone https://github.com/Paper-Proof/paperproof.git

# 依存関係をインストール
npm install

# 開発環境
# 詳細なセットアップガイドについてはリポジトリを参照

# 拡張機能をビルド
npm run build

# 配布用にパッケージ化
npm run package

例: 加算の交換可能性を証明

Lean 4 証明

theorem add_comm (m n : Nat) : m + n = n + m := by
  induction m with
  | zero => simp
  | succ k ih =>
    rw [Nat.succ_add, Nat.add_succ, ih]

Paperproof 可視化

ステップ 1: ベースケース (ゼロ)

┌─────────────────────────────────────┐
│ 仮説:                               │
│  - n : Nat                          │
├─────────────────────────────────────┤
│ ゴール: 0 + n = n + 0               │
├─────────────────────────────────────┤
│ タクティック: simp                  │
│ (反射性によって簡約)                │
└─────────────────────────────────────┘

ステップ 2: 帰納的ケース (succ)

┌─────────────────────────────────────────────────┐
│ 仮説:                                           │
│  - k : Nat                                      │
│  - n : Nat                                      │
│  - ih : k + n = n + k  [帰納的仮説]             │
├─────────────────────────────────────────────────┤
│ ゴール: succ k + n = n + succ k                 │
├─────────────────────────────────────────────────┤
│ タクティック:                                  │
│  - rw [Nat.succ_add]                            │
│  - rw [Nat.add_succ]                            │
│  - rw [ih]                                      │
│ (書き換えはゴールを反射性に変換)               │
└─────────────────────────────────────────────────┘

AI エージェントとの統合

Plurigrid での使用

Paperproof Validator は AI エージェント学習と統合できます:

エージェントは定理を証明することで学習:

エージェントが定理を生成
         ↓
Lean 4 が証明を検証
         ↓
Paperproof が構造を可視化
         ↓
エージェントが可視化から学習

フィードバックループ:

# エージェントが証明を提案
proof_sketch = agent.propose_theorem_proof(statement)

# Paperproof が検証
validation = paperproof.validate(proof_sketch)

if validation.passes:
    # 学習用の可視化を抽出
    structure = paperproof.extract_structure()
    agent.update_knowledge(structure)
else:
    # エージェントにエラー可視化を返す
    agent.learn_from_error(validation.error_path)

ステータスとロードマップ

✅ 現在: Lean 4 サポート、VS Code 統合、証明可視化 🔄 計画中:

証明検索支援
ゴールに基づくタクティック提案
機械学習統合
論文用 LaTeX へのエクスポート

スキル名: paperproof-validator タイプ: 形式的証明の可視化/検証 Trit: -1 (MINUS - バリデーター) 主な特性: 形式的証明を直感的な紙面に近い可視化に変換 ステータス: ✅ 本番環境対応 リポジトリ: Paper-Proof/paperproof VS Code 拡張機能: マーケットプレイスで利用可能

ライセンス: MIT(寛容ライセンスのため全文を引用しています) · 原本リポジトリ

SKILL.md 本文