From asi
Visualizes Lean 4 formal proofs as paper-like diagrams showing hypotheses, goals, and tactics in VS Code. Verifies proof correctness via Lean integration.
npx claudepluginhub plurigrid/asi --plugin asiThis skill uses the workspace's default tool permissions.
> Formal Proof Visualization and Verification for Lean 4
Assists with Lean 4 theorem proving: editing .lean files, debugging builds (type mismatches, sorries, axioms, lake errors), searching mathlib lemmas, formalizing mathematics, and learning concepts via commands like /lean4:prove and /lean4:formalize.
Orchestrates collaborative theorem proving in Lean using lc CLI for state management and parallel agents. Employs skeleton verification, math cards, and architecture planning for complex goals.
Fills Lean4 sorry holes in proofs, generates counterexamples for false statements, and handles English/Lean4 inputs via Harmonic API. For formal verification with Mathlib/lake.
Share bugs, ideas, or general feedback.
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
This skill connects to the K-Dense-AI/claude-scientific-skills ecosystem:
cryptography: 1 citations in bib.duckdbThis 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
The skill participates in triads satisfying:
(-1) + (0) + (+1) ≡ 0 (mod 3)
This ensures compositional coherence in the Cat# equipment structure.