paperproof-validator

Formal Proof Visualization and Verification for Lean 4

Version: 1.0.0 Trit: -1 (Validator - verifies proof correctness) Bundle: verification Status: ✅ New (Lean 4 theorem proof visualization) Repository: Paper-Proof/paperproof

---

Overview

Paperproof Validator transforms formal Lean 4 proofs into intuitive, paper-like visualizations. It bridges the gap between abstract formal proofs and human understanding by displaying how hypotheses and goals evolve throughout a proof.

Key Innovation: Makes formal proofs accessible by visualizing proof structure in a way that mirrors mathematical notation on paper.

What Paperproof Does

Instead of abstract Lean code:

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

Paperproof shows:

┌─────────────────────────────────────┐
│ Hypotheses (green nodes):           │
│  - h : P                            │
├─────────────────────────────────────┤
│ Goal (red node):                    │
│  - Q                                │
├─────────────────────────────────────┤
│ Tactics (transparent):              │
│  - apply some_lemma                 │
│  - exact h.right                    │
└─────────────────────────────────────┘

---

Architecture

Three Core Components

1. Lean 4 Library Integration

import Paperproof

theorem my_theorem : P ∧ Q → R := by
  -- Paperproof automatically extracts proof state
  intro ⟨hp, hq⟩
  -- Visualization tracks hypotheses and goals
  exact some_proof_term

Capabilities:

• Integrates with Lean 4 InfoTree
• Extracts proof state at each tactic
• Provides proof metadata to VS Code extension

---

2. VS Code Extension

Responsibilities:

• Tracks cursor position (detects which theorem is being visualized)
• Communicates with Lean server for proof data
• Hosts webview panel for visualization
• Provides commands and settings
• Bridges Lean InfoTree to React frontend

Commands:

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

Architecture Flow:

User Cursor on Theorem
           ↓
Selection Changed Event
           ↓
Request Proof Data from Lean Server
           ↓
Lean Server Returns InfoTree
           ↓
BetterParser (extract structure)
           ↓
Converter Service (optimize for visualization)
           ↓
Send to React Frontend
           ↓
Render Visual Proof Tree

---

3. React Frontend Visualization

Component Hierarchy:

ProofTree (root)
├── GlobalContext Provider
├── Header (title, controls)
└── BoxEl (variable scope container)
    ├── Hypotheses Section
    │   └── HypothesisNode (green)
    │       └── Transparency = "in scope"
    ├── Tactics Section
    │   └── TacticNode (transparent, dashed border)
    │       └── Arrows to related nodes
    └── Goals Section
        └── GoalNode (red)

Visual Cues:

• Hypotheses: Green nodes at the top
• Goals: Red nodes at the bottom
• Tactics: Transparent nodes with dashed borders
• Scope: Nested boxes with darkening backgrounds
• Availability: Node opacity indicates scope accessibility

---

Capabilities

1. visualize-proof-structure

Display proof as hierarchical tree with visual nodes:

from paperproof_validator import PaperproofVisualizer

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

# Extract and render proof
proof_visual = visualizer.visualize(
    show_hypotheses=True,
    show_goals=True,
    show_tactics=True,
    show_scopes=True
)

# Output: Interactive HTML/React visualization

2. extract-proof-metadata

Pull structured proof information from Lean InfoTree:

-- Lean 4 code
theorem and_comm (p q : Prop) : p ∧ q → q ∧ p := by
  intro ⟨hp, hq⟩      -- Step 1: intro creates hypotheses
  exact ⟨hq, hp⟩      -- Step 2: exact provides proof term

Extracted Structure:

{
  "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

Verify that proof reaches expected conclusion:

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

if validation.passes:
    print("✓ Proof correctly establishes Q")
else:
    print(f"✗ Proof does not establish Q")
    print(f"  Final goal: {validation.final_goal}")

4. analyze-tactic-effects

Show how each tactic transforms proof state:

analysis = visualizer.analyze_tactics()

for step in analysis.steps:
    print(f"\nTactic: {step.name}")
    print(f"Hypotheses before: {step.hypotheses_before}")
    print(f"Hypotheses after: {step.hypotheses_after}")
    print(f"Goals before: {step.goals_before}")
    print(f"Goals after: {step.goals_after}")
    print(f"Variables in scope: {step.scope}")

5. support-multiple-proof-tactics

Handle common Lean 4 tactics:

-- apply: Uses a hypothesis/lemma to transform goal
theorem proof_with_apply : P → Q := by
  intro hp
  apply lemma_p_implies_q
  exact hp

-- have: Introduces intermediate hypothesis
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: Proves by 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: Proof by contradiction
theorem by_contra_proof : P := by
  by_contra hnp
  have : False := contradiction_from_not_p hnp
  exact absurd this (by simp)

-- cases: Case analysis
theorem cases_proof : P := by
  cases some_disjunction with
  | left h => exact left_proof h
  | right h => exact right_proof h

All tactics are visualized with their proof state transformations.

6. export-proof-visualization

Generate static or interactive proof representations:

# Export as interactive HTML
visualizer.export_html("proof.html")

# Export as static image (PNG/SVG)
visualizer.export_image("proof.png", format="png")

# Export as LaTeX (for papers)
visualizer.export_latex("proof.tex")

# Export as JSON (for programmatic use)
visualizer.export_json("proof.json")

---

Integration with Lean 4 Ecosystem

Installation

# 1. Install VS Code Extension
# Via VS Code Extensions marketplace: search "Paperproof"

# 2. Add to Lean project (lakefile.toml)
require paperproof from git
  "https://github.com/Paper-Proof/paperproof.git"

# 3. Update
lake update

# 4. Import in Lean files
import Paperproof

Usage in Lean 4

import Paperproof

-- Define a theorem
theorem associativity : ∀ (a b c : Nat), (a + b) + c = a + (b + c) := by
  intro a b c
  -- When cursor is here, Paperproof shows:
  -- - Hypotheses: a : Nat, b : Nat, c : Nat
  -- - Goal: (a + b) + c = a + (b + c)
  induction a with
  | zero =>
    -- Paperproof shows base case context
    rfl
  | succ k ih =>
    -- Paperproof shows inductive step
    -- - ih : (k + b) + c = k + (b + c) [inductive hypothesis]
    simp [Nat.add_succ, ih]

---

Formal Proof Theory Background

Proof Trees and Natural Deduction

Paperproof visualization is based on natural deduction systems:

Hypotheses (context)
───────────────────────
    | Tactics apply
    | Goal transforms
───────────────────────
    Final conclusion

Gentzen Sequent Calculus Connection

Paperproof extends traditional proof visualization with modern web technologies:

Traditional Gentzen style:

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

Paperproof visualization:

• Shows Γ (hypotheses) visually
• Shows goals in red
• Shows proof steps with connecting arrows
• Indicates variable scope with nested boxes

Color Semantics

Color	Element	Meaning
Green	Hypotheses	Available facts in scope
Red	Goals	Targets to prove
Transparent	Tactics	Proof steps (white box)
Dark gray	Scope boundaries	Variable scope nesting
Opacity	Node visibility	Whether element is in scope

---

GF(3) Integration

Trit Assignment

Paperproof Validator: -1 (MINUS - critical validator)

Can form balanced triads with:

Potential Triad (Formal Verification):

Trit	Skill	Role
-1	paperproof-validator	Validates formal proofs
0	proof-instrumentation	Tracks proof steps
+1	theorem-generator	Generates provable theorems
Sum	0 (mod 3)	✓ Conserved

---

Comparison with Other Proof Tools

vs. Lean Native REPL

Aspect	Lean REPL	Paperproof
Visualization	Text-based	Visual tree
Scope Tracking	Implicit	Explicit boxes
Learning Curve	Steep	Gentle
Understanding	Abstract	Intuitive
Accessibility	Expert-only	Beginner-friendly

vs. Tactic State Window

Tactic State (raw):

⊢ (0 + 0) + 0 = 0

Paperproof (visual):

┌─────────────────────────────┐
│ Goal: (0 + 0) + 0 = 0       │
│ (After simp)                │
└─────────────────────────────┘

---

Configuration

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

rendering:
  color_scheme: dark        # or '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

---

Example Workflow

# 1. Install extension
# Open VS Code Extensions, search "Paperproof", click Install

# 2. Add to Lean project
# Edit lakefile.toml, add dependency

# 3. Import in Lean file
# Add: import Paperproof

# 4. Open Paperproof panel
# Cmd+Shift+P → "Paperproof: Open Panel"

# 5. Click on theorem
# Click on any 'theorem' or 'lemma' in editor

# 6. View visualization
# Paperproof shows interactive proof tree in side panel

# 7. Export proof
# Cmd+Shift+P → "Paperproof: Export Proof as Image"

---

Technical Implementation

BetterParser

Converts Lean InfoTree (raw proof structure) to simplified representation:

Lean 4 InfoTree (complex, nested)
        ↓
   BetterParser
        ↓
Simplified Proof Structure (clean)
        ↓
   Converter
        ↓
React-Friendly Format
        ↓
Visual Rendering

Converter Service

Optimizes proof structure for visualization:

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

# Process through converter
visual_tree = convert_to_visual_format(lean_tree)
# Output: { "type": "intro", "hypotheses": [...], "goals": [...] }

# Pass to React
render_to_webview(visual_tree)

VS Code Extension Communication

// VS Code Extension (TypeScript)
vscode.window.onDidChangeTextEditorSelection((e) => {
  const theorem_name = getSymbolAtCursor(e);

  // Request proof from Lean server
  const proof_data = getLeanProofData(theorem_name);

  // Send to webview
  webview.postMessage({
    type: "updateProof",
    data: proof_data
  });
});

// React Webview receives message
window.addEventListener("message", (event) => {
  if (event.data.type === "updateProof") {
    renderProofTree(event.data.data);
  }
});

---

Related Skills

• bisimulation-game - Verifies equivalence of proofs
• langevin-dynamics-skill - Analyzes proof dynamics
• fokker-planck-analyzer - Validates proof convergence
• spi-parallel-verify - Checks proof structure invariants

---

Learning Resources

Examples from the wild:

• Proofs from "Mathematics in Lean 4"
• Proofs from Mathlib4
• The Hitchhiker's Guide to Logical Verification
• Lean 4 tutorials and documentation

Tutorial Examples Included:

• Natural deduction proofs
• Inductive proofs
• Proof by contradiction
• Case-by-case proofs

---

Development

Paperproof is actively developed and welcomes contributions:

• Repository: GitHub - Paper-Proof/paperproof
• Issues & Discussion: Open for feature requests and bug reports
• License: Open source (check repository for details)

Development Setup

# Clone repository
git clone https://github.com/Paper-Proof/paperproof.git

# Install dependencies
npm install

# Development environment
# See repository for full setup guide

# Build extension
npm run build

# Package for distribution
npm run package

---

Example: Proving Commutativity of Addition

Lean 4 Proof

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 Visualization

Step 1: Base Case (zero)

┌─────────────────────────────────────┐
│ Hypotheses:                         │
│  - n : Nat                          │
├─────────────────────────────────────┤
│ Goal: 0 + n = n + 0                 │
├─────────────────────────────────────┤
│ Tactic: simp                        │
│ (simplifies by reflexivity)         │
└─────────────────────────────────────┘

Step 2: Inductive Case (succ)

┌─────────────────────────────────────────────────┐
│ Hypotheses:                                     │
│  - k : Nat                                      │
│  - n : Nat                                      │
│  - ih : k + n = n + k  [inductive hypothesis]  │
├─────────────────────────────────────────────────┤
│ Goal: succ k + n = n + succ k                   │
├─────────────────────────────────────────────────┤
│ Tactics:                                        │
│  - rw [Nat.succ_add]                            │
│  - rw [Nat.add_succ]                            │
│  - rw [ih]                                      │
│ (rewrites transform goal to reflexivity)        │
└─────────────────────────────────────────────────┘

---

Integration with AI Agents

Use in Plurigrid

Paperproof Validator can integrate with AI agent learning:

Agent learns by proving theorems:

Agent Generates Theorem
         ↓
Lean 4 Verifies Proof
         ↓
Paperproof Visualizes Structure
         ↓
Agent Learns from Visualization

Feedback Loop:

# Agent proposes proof
proof_sketch = agent.propose_theorem_proof(statement)

# Paperproof validates
validation = paperproof.validate(proof_sketch)

if validation.passes:
    # Extract visualization for learning
    structure = paperproof.extract_structure()
    agent.update_knowledge(structure)
else:
    # Return error visualization to agent
    agent.learn_from_error(validation.error_path)

---

Status & Roadmap

✅ Current: Lean 4 support, VS Code integration, proof visualization 🔄 Planned:

• Proof search assistance
• Tactic suggestions based on goal
• Machine learning integration
• Export to LaTeX for papers

---

Skill Name: paperproof-validator Type: Formal Proof Visualization / Verification Trit: -1 (MINUS - validator) Key Property: Transforms formal proofs into intuitive paper-like visualizations Status: ✅ Production Ready Repository: Paper-Proof/paperproof VS Code Extension: Available in marketplace