Installation

$ npx skills add smithery/plurigrid --skill lean-proof-walk

Agent compatibility

Declared targets from SKILL.md / docs. Unmarked agents are not listed — the skill may still install via the CLI.

Claude Code Not declared

Cursor Not declared

Codex Not declared

GitHub Copilot Not declared

Windsurf Not declared

Gemini CLI Not declared

Cline Not declared

OpenCode Not declared

Package contents

Files included with this skill beyond the listing page.

skill md SKILL.md 3,081 B

docs SUMMARY.md 256 B

SKILL.md

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

lean-proof-walk