Skip to main content

Theorem Generator Demo

This document presents a verified demonstration of self-improving theorem generation — a system that uses canonical forms and verified lemmas to reduce future verification costs.

Verified Results​

All demonstrations pass verification:

======================================================================
THEOREM GENERATOR: COMPLETE VERIFICATION
======================================================================

[1] CANONICAL NORMAL FORM
----------------------------------------
  lhs_input: (x + y)
  rhs_input: (y + x)
  canonical_match: True
  receipt: f5bf0b27fdeb631f...

[2] SELF-IMPROVING THEOREM GENERATION
----------------------------------------
  [CANONICAL] (x + y) = (y + x) (already canonical)
  [CANONICAL] (x * y) = (y * x) (already canonical)
  [CANONICAL] (x + (y + x)) = ((x + y) + x) (already canonical)
  [CANONICAL] (x * (y * x)) = ((x * y) * x) (already canonical)
  Total lemmas: 4
  Collapsed: 4
  Monotone: True

[3] LEMMA RECONSTRUCTION
----------------------------------------
  Lemma set size: 5
  Events: 7
  Total cost: 60

[4] BOUNDARY FLOW CONSERVATION
----------------------------------------
  Conservation: True

[5] COUNTEREXAMPLE DETECTION
----------------------------------------
  Claim: (x + 1) = x
  Result: REFUTED
  Counterexample: mod=2, x=0, LHS=1, RHS=0

======================================================================
VERIFICATION SUMMARY
======================================================================

  Canonical Form:     PASS
  Self-Improvement:   PASS
  Boundary Flow:      PASS
  Refutation Check:   PASS

  ALL DEMOS PASS:     YES

Demo 1: Canonical Normal Form​

Question: How to define canonical form so LemID and receipts are identical across implementations?

Answer:

def canon_json(obj) -> str:
    return json.dumps(obj, sort_keys=True, separators=(",", ":"))

def make_lem_id(lhs_str, rhs_str, mods):
    obj = {
        "type": "lemma",
        "lhs": lhs_str,  # canonical string
        "rhs": rhs_str,  # canonical string
        "witness_mods": sorted(mods),
        "verifier": "exhaustive_finite_model_check"
    }
    return sha256_hex(canon_json(obj))

Verification:

  • (x + y) and (y + x) canonicalize to the same string
  • LemID is deterministic and implementation-independent

Demo 2: Self-Improving Theorem Generation​

Key Insight: Canonicalization enables self-improvement.

When we try to verify (x + y) = (y + x):

  1. Canonicalize both sides
  2. They become identical under canonical form
  3. No verification needed — the equality is already absorbed

This demonstrates monotone improvement: as more lemmas are verified, future verification costs can only decrease.

Demo 3: Lemma Reconstruction​

Question: What minimal lemma set to use for a toy reconstruction?

Answer:

L_now = [
    ("x + 0 = x", "PASS"),      # additive identity
    ("x * 1 = x", "PASS"),      # multiplicative identity
    ("x * 0 = 0", "PASS"),      # annihilator
    ("x + y = y + x", "PASS"),  # commutativity
    ("x * y = y * x", "PASS"),  # commutativity
]

Reconstructed History:

The system builds from minimal axioms to verified identities, demonstrating how a small set of foundational lemmas can bootstrap more complex verifications.

Demo 4: Boundary Flow Conservation​

The system verifies that boundary flows between subsystems satisfy conservation laws — local structure can increase only if compensated by the environment.

Verification: Conservation: True

Demo 5: Counterexample Detection​

Claim: (x + 1) = x

Result: REFUTED

Counterexample:

  • mod = 2, x = 0
  • LHS = 1, RHS = 0

When a claim cannot be verified, the system returns a concrete counterexample.

Key Takeaways​

  1. Proofs become reusable tests — verified lemmas reduce future verification costs
  2. Counterexamples are concrete — failed claims return explicit witnesses
  3. Conservation is verified — boundary flows satisfy global constraints

Related: MAPF Demo — Another validation demo