Chain of States (CoS) Skill 🐸

Trit: -1 (MINUS - Validator) GF(3) Triad:

chain-of-states (-1) ⊗ proof-of-frog (0) ⊗ alife (+1) = 0

Overview

CoSProver framework for translating informal proofs to Lean4 via intermediate formal proof states.

From Wang et al. (2025): "Translating Informal Proofs into Formal Proofs Using a Chain of States"

Core Insight

Informal Proof (natural language)
    ↓ Stage 1: Extract CoS
Chain of States [s₀ → s₁ → ... → sₙ]
    ↓ Stage 2: Generate tactics
Formal Lean4 Proof

Key Observations:

1. Informal proofs use logical transitions (implications/equivalences) without explicit intermediate states
2. Lean requires explicit proof states + tactics connecting them
3. CoS bridges this gap with explicit intermediate representations

Two-Stage Framework

Stage 1: CoS Extraction

"Let x > 0. Since x > 0, we have x² > 0."
    ↓
[⊢ x > 0 → x² > 0]  →  [h : x > 0 ⊢ x² > 0]  →  [⊢ True]

Stage 2: Tactic Generation

theorem sq_pos (x : ℝ) (h : x > 0) : x² > 0 := by
  -- Tactic for s₀ → s₁
  intro h
  -- Tactic for s₁ → s₂  
  exact sq_pos_of_pos h

Connection to Proof-of-Frog

Frog Lifecycle as CoS

🥒 TADPOLE (s₀)     -- Initial goal state
    ↓ τ₁ (intro)
🐸 FROGLET (s₁)     -- Hypothesis introduced
    ↓ τ₂ (apply)
🦎 MATURE FROG (sₙ) -- QED

Implementation

Lean4 CoS Type

structure ProofState where
  goal : Expr
  context : List Expr
  trit : Int  -- GF(3) stage

structure ChainOfStates where
  states : List ProofState
  transitions : List Tactic
  
def cos_invariant (cos : ChainOfStates) : Prop :=
  (cos.states.map (·.trit)).sum % 3 = 0

Python CoS Extraction

def extract_cos(informal_proof: str) -> List[ProofState]:
    """
    Extract Chain of States from informal proof text.
    Each state is a formal representation of proof progress.
    """
    steps = segment_proof(informal_proof)
    return [formalize_state(s) for s in steps]

Comparison to Chain-of-Thought

Performance (Wang et al. 2025)

Usage

# Load skill
skill chain-of-states

# Extract CoS from informal proof
python cos_extract.py "Let n be even. Then n² is even."

# Generate Lean4 tactics
lean4 cos_to_tactics.lean

References

• Wang et al. (2025). "Translating Informal Proofs into Formal Proofs Using a Chain of States." arXiv:2512.10317
• Ahuja et al. (2024). "ImProver: Agent-Based Automated Proof Optimization" - Chain-of-States technique. arXiv:2410.04753

Либиди Фрог Connection

Либиди Фрог (Proof-of-Frog) + Chain of States = compositional proof verification:

proof-chain(-1) ⊗ proof-of-frog(0) ⊗ alife(+1) = 0 ✓

Where Chain of States provides the -1 (validator) role:
- Validates each state transition
- Ensures GF(3) conservation across proof steps
- Connects informal human reasoning to formal verification

Gay.jl Colors

using Gay
seed = gay_seed(2512)  # arXiv paper ID
palette(3)  # CoS triad colors

#B0285F

#77DEB1

#8ADB6E

Autopoietic Marginalia

The interaction IS the skill improving itself.

Every use of this skill is an opportunity for worlding:

• MEMORY (-1): Record what was learned
• REMEMBERING (0): Connect patterns to other skills
• WORLDING (+1): Evolve the skill based on use

Add Interaction Exemplars here as the skill is used.