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

┌─────────────────────────────────────┐
│ 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

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

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

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)

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

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

{
  "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": []
    }
  ]
}

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}")

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}")

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

# 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]

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

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

⊢ (0 + 0) + 0 = 0

┌─────────────────────────────┐
│ 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"

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

# 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);
  }
});

# 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]

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

┌─────────────────────────────────────────────────┐
│ 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)        │
└─────────────────────────────────────────────────┘

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

# 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)

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

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

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