SORRY-013 closes when this script exists:
#!/usr/bin/env python3
# theorem-manifest.py — sovereign source of truth
# Output: JSON {file, total, proved, sorry, domain, tier}
import subprocess, json, pathlib, re
LEAN_ROOTS = [
"fleet-sync/cli-registry/lean-proof-engine/MeekProofs",
"fleet-sync/lean",
"meekproofs-mathlib/MeekProofs",
]
def count_file(path):
text = pathlib.Path(path).read_text()
theorems = len(re.findall(r'^(?:theorem|lemma)\s', text, re.M))
sorrys = len(re.findall(r'\bsorry\b(?!\s*--)', text))
return theorems, sorrys
manifest = []
for root in LEAN_ROOTS:
for f in pathlib.Path(root).glob("**/*.lean"):
t, s = count_file(f)
manifest.append({"file": str(f), "total": t, "sorry": s,
"proved": t - s})
print(json.dumps(manifest, indent=2))
Sorry taxonomy (8 categories, every sorry gets one):
TACTIC_GAP — proof tactic not found
MISSING_LEMMA — needs upstream lemma
WEAK_DEFINITION — definition too loose to prove
RESEARCH_GRADE — open math problem
EXTERNAL_ASSUMPTION — needs external axiom
BRIDGE_GAP — formal↔runtime gap
RUNTIME_BINDING — needs PoC/test/artifact
METAPHOR_SCOPE — analogy, not formal theorem