From asi
Generates formal Lean 4 proof state chains using GF(3)-balanced random walks with triad agents (Generator +1, Coordinator 0, Validator -1) for parallel verification. Invoke for theorem proving.
npx claudepluginhub plurigrid/asi --plugin asiThis skill uses the workspace's default tool permissions.
Generate formal Lean 4 proof state chains using GF(3)-balanced random walks.
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.
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.
Share bugs, ideas, or general feedback.
Generate formal Lean 4 proof state chains using GF(3)-balanced random walks.
| 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 N: Γ ⊢ G
where:
Γ = context (hypotheses: x : τ, h : P)
⊢ = turnstile (entailment)
G = goal (proposition to prove)
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
seed := 0x42D (or user-provided)
state := State 0 with full context and goal
triad := spawn 3 parallel agents with trits {-1, 0, +1}
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)
State m = "No Goals" → QED
Emit: formal statement, informal proof, detailed proof, state chain
/lean-proof-walk "∀ a b : ℤ, a + b = b + a"
/lean-proof-walk --seed=1069 --theorem="commutativity of addition"
| 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 |
γ = 0x9E3779B97F4A7C15 # golden ratio constant
def next_seed(seed, state_hash, trit):
return (seed ^ (state_hash * γ) ^ trit) & ((1 << 64) - 1)
lean-proof-walk (0) ⊗ bdd-mathematical-verification (+1) ⊗ chromatic-walk (-1) = 0 ✓
⟦State n⟧ = (Γₙ, Gₙ)
⟦S → S'⟧ = tactic application
⟦No Goals⟧ = proof complete
⟦Σ trits⟧ ≡ 0 (mod 3) always