Paperproof Validator

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

GF(3) Integration

Trit Assignment

Paperproof Validator: -1 (MINUS - critical validator)

Can form balanced triads with:

Potential Triad (Formal Verification):

Comparison with Other Proof Tools

vs. Lean Native REPL

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

Scientific Skill Interleaving

This skill connects to the K-Dense-AI/claude-scientific-skills ecosystem:

Graph Theory

• networkx [○] via bicomodule
  • Universal graph hub

Bibliography References

• cryptography: 1 citations in bib.duckdb

SDF Interleaving

This skill connects to Software Design for Flexibility (Hanson & Sussman, 2021):

Primary Chapter: 10. Adventure Game Example

Concepts: autonomous agent, game, synthesis

GF(3) Balanced Triad

paperproof-validator (○) + SDF.Ch10 (+) + [balancer] (−) = 0

Skill Trit: 0 (ERGODIC - coordination)

Secondary Chapters

• Ch6: Layering
• Ch5: Evaluation

Connection Pattern

Adventure games synthesize techniques. This skill integrates multiple patterns.

Cat# Integration

This skill maps to Cat# = Comod(P) as a bicomodule in the equipment structure:

Trit: 0 (ERGODIC)
Home: Prof
Poly Op: ⊗
Kan Role: Adj
Color: #26D826

GF(3) Naturality

The skill participates in triads satisfying:

(-1) + (0) + (+1) ≡ 0 (mod 3)

This ensures compositional coherence in the Cat# equipment structure.