diff --git a/scripts/populate_ene_tables.py b/scripts/populate_ene_tables.py
index bdff4ecf..9626b948 100644
--- a/scripts/populate_ene_tables.py
+++ b/scripts/populate_ene_tables.py
@@ -288,6 +288,33 @@ def make_ingest_event_sql(event_id: str, pkg_id: str, source_uri: str,
     )
 
 
+def make_prover_state_sql(theorem_id: str, name: str, statement: str,
+                          status: str = "raw", signature_hash: str = "",
+                          dependencies: list = None) -> str:
+    """Generate INSERT for ene.prover_state."""
+    deps = json.dumps(dependencies or [], ensure_ascii=False)
+    return (
+        f"INSERT INTO ene.prover_state "
+        f"(theorem_id, name, statement, formalization_status, signature_hash, dependencies) "
+        f"VALUES ('{esc(theorem_id)}', '{esc(name[:200])}', '{esc(statement[:2000])}', "
+        f"'{esc(status)}', '{esc(signature_hash)}', '{esc(deps)}') "
+        f"ON CONFLICT DO NOTHING;"
+    )
+
+
+def make_prover_instance_sql(theorem_id: str, input_fixture: dict,
+                             evaluation_witness: dict,
+                             verifier: str = "lean4") -> str:
+    """Generate INSERT for ene.prover_instances."""
+    return (
+        f"INSERT INTO ene.prover_instances "
+        f"(theorem_id, input_fixture, evaluation_witness, verifier_identity) "
+        f"VALUES ('{esc(theorem_id)}', {jsonb(input_fixture)}, "
+        f"{jsonb(evaluation_witness)}, '{esc(verifier)}') "
+        f"ON CONFLICT DO NOTHING;"
+    )
+
+
 # ── Build SQL batches ────────────────────────────────────────────────────────
 
 def build_sql_batches(sources: dict) -> dict:
@@ -387,6 +414,25 @@ def build_sql_batches(sources: dict) -> dict:
                 make_gossip_node_sql(f"gsn_{cid}", cid, fold, nh, desc[:200] if desc else name, wm, gr)
             )
 
+        # Prover state (all theorems and lemmas)
+        if ctype in ("theorem", "lemma"):
+            formalization_status = "verified" if lean_status == "DEFINED" else "raw"
+            sig_hash = hashlib.sha256((lean_name or cid).encode()).hexdigest()[:16]
+            deps = concept.get("related", [])[:10]
+            batches["prover_state"].append(
+                make_prover_state_sql(lean_name or cid, name, expr or desc,
+                                      formalization_status, sig_hash, deps)
+            )
+
+        # Prover instances (verified theorems only — those with DEFINED status)
+        if ctype in ("theorem",) and lean_status == "DEFINED":
+            fixture = {"source_file": source, "concept_id": cid, "tags": tags[:5]}
+            witness = {"lean_status": "DEFINED", "lean_name": lean_name,
+                       "expression": (expr or "")[:500]}
+            batches["prover_instances"].append(
+                make_prover_instance_sql(lean_name or cid, fixture, witness)
+            )
+
         # Relations from 'related' field
         for rel_target in concept.get("related", []):
             rel_key = f"{cid}->{rel_target}"
@@ -637,7 +683,8 @@ def main():
     print("  ─────────────────────────┼───────────────")
     for table in ["packages", "receipts", "sidon_labels", "braid_strands",
                    "eigensolid_snapshots", "gossip_surface_nodes",
-                   "gossip_surface_edges", "relations", "sessions", "ingest_events"]:
+                   "gossip_surface_edges", "relations", "sessions",
+                   "ingest_events", "prover_state", "prover_instances"]:
         count = len(batches.get(table, []))
         marker = "" if count > 0 else " (empty)"
         print(f"  {table:<24s} | {count}{marker}")
@@ -646,7 +693,7 @@ def main():
     # Skip tables
     skip_tables = ["crossing_weights", "fractal_nodes", "fractal_manifolds",
                    "fractal_graph_entities", "vectors", "dsp_nodes",
-                   "prover_instances", "prover_state", "nspace_kv",
+                   "nspace_kv",
                    "wiki_pages", "wiki_revisions", "wiki_categories", "wiki_links", "routes"]
     print("  Skipped tables (no clean mapping):")
     for t in skip_tables:
@@ -701,7 +748,8 @@ def main():
     print("\n── Final row counts ──")
     for table in ["packages", "receipts", "sidon_labels", "braid_strands",
                    "eigensolid_snapshots", "gossip_surface_nodes",
-                   "gossip_surface_edges", "relations", "sessions", "ingest_events"]:
+                   "gossip_surface_edges", "relations", "sessions",
+                   "ingest_events", "prover_state", "prover_instances"]:
         count = neon(f"SELECT COUNT(*) FROM ene.{table}")
         print(f"  {table}: {count}")