Formal Proof Visualization and Verification for Lean 4
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
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.
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 │
└─────────────────────────────────────┘
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:
Responsibilities:
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
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:
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
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": []
}
]
}
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}")
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}")
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.
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")
# 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
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]
Paperproof visualization is based on natural deduction systems:
Hypotheses (context)
───────────────────────
| Tactics apply
| Goal transforms
───────────────────────
Final conclusion
Paperproof extends traditional proof visualization with modern web technologies:
Traditional Gentzen style:
Γ ⊢ A Γ ⊢ B
──────────────────
Γ ⊢ A ∧ B
Paperproof visualization:
| 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 |
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 |
| 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 |
Tactic State (raw):
⊢ (0 + 0) + 0 = 0
Paperproof (visual):
┌─────────────────────────────┐
│ Goal: (0 + 0) + 0 = 0 │
│ (After simp) │
└─────────────────────────────┘
# 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
# 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"
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
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 (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);
}
});
Examples from the wild:
Tutorial Examples Included:
Paperproof is actively developed and welcomes contributions:
# 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
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]
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) │
└─────────────────────────────────────────────────┘
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)
✅ Current: Lean 4 support, VS Code integration, proof visualization 🔄 Planned:
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
