Lean Proof Walk Skill | Agent Skills

Lean Proof Walk

Generate formal Lean 4 proof state chains using GF(3)-balanced random walks.

Triad Structure

| Agent | Trit | Role | Action | |-------|------|------|--------| | Generator | +1 | Create | Propose next proof state | | Coordinator | 0 | Transport | Formalize transition, derive seed | | Validator | -1 | Verify | Check soundness, GF(3) conservation |

Invariant: trit(G) + trit(C) + trit(V) = (+1) + 0 + (-1) = 0

State Chain Format

State N: Γ ⊢ G

where:
  Γ = context (hypotheses: x : τ, h : P)
  ⊢ = turnstile (entailment)
  G = goal (proposition to prove)

Example Chain

State 0: a : ℤ, b : ℤ, h : a + b = 0 ⊢ b = -a

State 1: a : ℤ, b : ℤ, h : a + b = 0 ⊢ a + b - a = 0 - a

State 2: a : ℤ, b : ℤ, h : a + b = 0 ⊢ b = -a

State 3: No Goals

Protocol

1. Initialize

seed := 0x42D (or user-provided)
state := State 0 with full context and goal
triad := spawn 3 parallel agents with trits {-1, 0, +1}

2. Walk Step (repeat until No Goals)

Generator (+1):  propose tactic τ, predict State n+1
Coordinator (0): formalize Γₙ ⊢ Gₙ  →  Γₙ₊₁ ⊢ Gₙ₊₁
Validator (-1):  verify transition sound, Σ trits = 0
Commit:          seed_{n+1} = hash(seed_n ⊕ state_n)

3. Terminate

State m = "No Goals" → QED
Emit: formal statement, informal proof, detailed proof, state chain

Invocation

/lean-proof-walk "∀ a b : ℤ, a + b = b + a"
/lean-proof-walk --seed=1069 --theorem="commutativity of addition"

Output Structure

Formal Statement (Lean 4 syntax)
Informal Proof (1-2 sentences)
Detailed Informal Proof (numbered steps)
Chain of States (with interleaved explanations)

Tactics Vocabulary

| Tactic | State Transition | |--------|------------------| | intro x | Γ ⊢ ∀x.P → Γ, x:τ ⊢ P | | apply h | Γ, h:P→Q ⊢ Q → Γ ⊢ P | | exact h | Γ, h:P ⊢ P → No Goals | | rfl | Γ ⊢ a = a → No Goals | | simp | Γ ⊢ P → Γ ⊢ P' (simplified) | | ring | Γ ⊢ polynomial_eq → No Goals | | omega | Γ ⊢ linear_arith → No Goals | | cases h | Γ, h:P∨Q ⊢ R → Γ, h:P ⊢ R and Γ, h:Q ⊢ R | | induction n | Γ ⊢ P(n) → base case + inductive step |

GF(3) Seed Derivation

γ = 0x9E3779B97F4A7C15  # golden ratio constant

def next_seed(seed, state_hash, trit):
    return (seed ^ (state_hash * γ) ^ trit) & ((1 << 64) - 1)

Bundled Triad Skills

lean-proof-walk (0) ⊗ bdd-mathematical-verification (+1) ⊗ chromatic-walk (-1) = 0 ✓

Quick Reference

⟦State n⟧ = (Γₙ, Gₙ)
⟦S → S'⟧ = tactic application
⟦No Goals⟧ = proof complete
⟦Σ trits⟧ ≡ 0 (mod 3) always

Agent Skills: Lean Proof Walk

Install this agent skill to your local

Skill Files