Asi lean-proof-walk

GF(3)-balanced random walk through Lean proof states. Use when generating formal proof chains with parallel triad verification. Invokes 3 agents (Generator +1, Coordinator 0, Validator -1) to traverse proof space via prime geodesics.

install

source · Clone the upstream repo

git clone https://github.com/plurigrid/asi

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/plurigrid/asi "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/lean-proof-walk" ~/.claude/skills/plurigrid-asi-lean-proof-walk-3e4ebc && rm -rf "$T"

manifest: skills/lean-proof-walk/SKILL.md

source content

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