""" SZLHOLDINGS/lean-proof-playground Interactive Lean 4 proof explorer — Lutar Thesis formal verification 6 tabs: 1. Theorem index browser 2. Proof source viewer with tactic explanation 3. Proof structure + static analysis (no server-side Lean) 4. DOI / Zenodo cross-link panel 5. MadhavaBound + TwoWitness PR status 6. Open-problem axioms surfaced honestly SPDX-License-Identifier: Apache-2.0 Copyright 2026 SZL Holdings / Lutar, Stephen P. ORCID 0009-0001-0110-4173 Doctrine V6 Strict. Honest disclosures: - 1 residual sorry: Lutar/SBOMProvenance.lean line 109 (canonicalEncoding_injective — structural framing, not a new axiom) - 13 declared axioms across 8 files (listed in Tab 6) - Lake-verified count = theorems in files with zero sorry occurrences """ from __future__ import annotations import json import math import re import urllib.parse from pathlib import Path from typing import Optional import gradio as gr import plotly.graph_objects as go # --------------------------------------------------------------------------- # Constants # --------------------------------------------------------------------------- THESIS_DOI = "https://doi.org/10.5281/zenodo.20434276" SPACE_URL = "https://huggingface.co/spaces/SZLHOLDINGS/lean-proof-playground" GITHUB_URL = "https://github.com/szl-holdings/lutar-lean" LEAN_LIVE_URL = "https://live.lean-lang.org/" BROWSER_SPACE = "https://huggingface.co/spaces/SZLHOLDINGS/lutar-lean-browser" ORCID = "https://orcid.org/0009-0001-0110-4173" # Canonical numbers from thesis (theorem-level, not file-level) CANON_TOTAL_THMS = 375 # 134 lake-verified + 241 skeletons CANON_LAKE_VERIFIED = 134 CANON_SKELETONS = 241 CANON_THESIS_THMS = 76 # 72 theorem + 4 corollary named in thesis CANON_TOTAL_FILES = 6022 # all .lean in the repo CANON_LUTAR_FILES = 71 # Lutar/ directory .lean files RESIDUAL_SORRY_FILE = "Lutar/SBOMProvenance.lean" RESIDUAL_SORRY_LINE = 109 # All thesis DOIs DOIS = [ {"key": "concept", "doi": "10.5281/zenodo.19944926", "label": "Concept DOI (always latest)", "url": "https://doi.org/10.5281/zenodo.19944926"}, {"key": "v18", "doi": "10.5281/zenodo.20434276", "label": "v18 — Thesis (canonical)", "url": "https://doi.org/10.5281/zenodo.20434276"}, {"key": "proof-lib","doi": "10.5281/zenodo.20434308", "label": "Proof library (lutar-lean)", "url": "https://doi.org/10.5281/zenodo.20434308"}, {"key": "v17", "doi": "10.5281/zenodo.20431181", "label": "v17 — Wheeler + Shannon + QEC","url": "https://doi.org/10.5281/zenodo.20431181"}, {"key": "v16", "doi": "10.5281/zenodo.20424996", "label": "v16", "url": "https://doi.org/10.5281/zenodo.20424996"}, {"key": "v15", "doi": "10.5281/zenodo.20424995", "label": "v15", "url": "https://doi.org/10.5281/zenodo.20424995"}, {"key": "v14", "doi": "10.5281/zenodo.20424992", "label": "v14", "url": "https://doi.org/10.5281/zenodo.20424992"}, ] # PR status (static, as of 2026-05-29) PR_MADHAVA = { "number": 56, "title": "feat(pac-bayes): MadhavaBound — Mādhava alternating-series bound", "url": "https://github.com/szl-holdings/lutar-lean/pull/56", "status": "OPEN", "files": ["Lutar/PACBayes/MadhavaBound.lean", "Lutar/TwoWitness.lean"], "sorry_count": 4, "sorry_detail": "MadhavaBound: 3 sorry (lines 105, 126, 145); TwoWitness: 1 sorry (line 163)", "description": ( "MadhavaBound formalises the Mādhava–Leibniz alternating-series remainder bound " "(c. 1400 CE, three centuries before Gregory/Leibniz). " "TwoWitness states Kochen–Specker 18-vector NCHV soundness. " "Both carry tracked sorry placeholders — honest open obligations, not silent gaps." ), } # Declared axioms (all 13, from grep) DECLARED_AXIOMS = [ {"file": "DPOFeasibility.lean", "axioms": ["pinsker", "klDivergence_nonneg"], "note": "Pinsker's inequality and KL non-negativity — standard information theory, Mathlib-trivial but not yet linked"}, {"file": "PACBayes.lean", "axioms": ["MomentSubGaussian"], "note": "Sub-Gaussian moment bound — standard but proof deferred"}, {"file": "Banach/LiuHuiPi.lean", "axioms": ["liu_hui_pi_converges"], "note": "Liu Hui π-convergence — historically attributed (~263 CE), Mathlib approach pending"}, {"file": "Knot/ReidemeisterConjecture.lean", "axioms": ["r1_invariance", "r2_invariance"], "note": "Reidemeister move invariance — stated as axiom; proof requires knot homology machinery"}, {"file": "Lambda/SchurConcave.lean", "axioms": ["lambda_schur_concave_n_axis"], "note": "Schur concavity of Λ_k — Hardy–Littlewood–Pólya 1952; Lean proof is open engineering task"}, {"file": "Feynman/PathIntegralAuditSum.lean", "axioms": ["canonicalReceipt", "audit_reidemeister_invariance", "lambda_stationary_unique"], "note": "Three path-integral audit axioms — governance framing axioms, physically motivated"}, {"file": "Gates/GleasonMod8.lean", "axioms": ["gleason_length_mod_8"], "note": "Gleason mod-8 length constraint — open proof obligation"}, {"file": "Thesis/TH_V18_14_SHA256CollisionHonest.lean", "axioms": ["sha256", "sha256_collision_resistant"], "note": "SHA-256 collision resistance — cryptographic assumption, not provable in Lean without axiom"}, ] # --------------------------------------------------------------------------- # Data loading # --------------------------------------------------------------------------- THEOREMS_DIR = Path(__file__).parent / "theorems" INDEX_FILE = THEOREMS_DIR / "index.json" def _load_index() -> list[dict]: if INDEX_FILE.exists(): return json.loads(INDEX_FILE.read_text()) return [] THEOREMS: list[dict] = _load_index() def _get_by_name(name: str) -> Optional[dict]: for t in THEOREMS: if t["name"] == name: return t return None def _read_source(t: dict) -> str: group = t.get("group", "lutar-lean") rel = t.get("file", "") if group == "lutar-lean": p = THEOREMS_DIR / "Lutar" / rel else: p = THEOREMS_DIR / "skeletons" / Path(rel).name if p.exists(): return p.read_text(errors="replace") for candidate in THEOREMS_DIR.rglob(Path(rel).name + ".lean"): return candidate.read_text(errors="replace") return f"-- Source not found: {rel}" def _all_names() -> list[str]: return [t["name"] for t in THEOREMS] def _all_chapters() -> list[str]: return ["All"] + sorted({t["chapter"] for t in THEOREMS}) def _all_statuses() -> list[str]: return ["All", "lake-verified", "skeleton"] # --------------------------------------------------------------------------- # Tab 1 — Theorem Index Browser # --------------------------------------------------------------------------- LIB_HEADERS = [ "File", "Chapter", "Status", "Lake-Verified", "Sorries", "Theorems", "Axioms", "Lines", ] def build_library(search: str = "", status: str = "All", chapter: str = "All") -> list[list]: rows = [] q = search.lower().strip() for t in THEOREMS: if q and q not in t["name"].lower() \ and q not in t.get("chapter", "").lower() \ and q not in " ".join(t.get("theorem_names", [])).lower(): continue if status != "All" and t["status"] != status: continue if chapter != "All" and t["chapter"] != chapter: continue rows.append([ t["name"], t["chapter"], t["status"], "yes" if t["lake_verified"] else "no", t["sorry_count"], t["theorem_count"], len(t.get("axiom_names", [])), t["lines"], ]) return rows # --------------------------------------------------------------------------- # Tab 2 — Proof viewer + tactic explanation # --------------------------------------------------------------------------- TACTIC_DOC: dict[str, str] = { "apply": "Backward chaining: unify goal with conclusion of a lemma, leaving hypotheses as sub-goals.", "exact": "Close goal with a specific term whose type equals the goal exactly.", "simp": "Simplify using a library of rewrite lemmas until no more apply.", "norm_num": "Evaluate numeric arithmetic goals (equalities/inequalities over ℤ, ℚ, ℝ).", "ring": "Prove ring equalities by polynomial normalisation.", "linarith": "Decide linear arithmetic goals over ordered fields via Farkas's lemma.", "omega": "Complete solver for linear arithmetic over ℤ and ℕ.", "decide": "Evaluate a decidable proposition by kernel computation.", "rfl": "Close a goal of the form a = a by reflexivity.", "intro": "Introduce a universally quantified variable or hypothesis into context.", "cases": "Case analysis: split on constructors of an inductive type.", "induction": "Structural induction: base case + inductive step sub-goals.", "have": "Assert an intermediate lemma, binding it as a named hypothesis.", "rw": "Rewrite goal using an equation (left-to-right by default; ← for reverse).", "field_simp": "Clear denominators and simplify field expressions.", "positivity": "Prove 0 < e or 0 ≤ e by syntactic analysis of expression structure.", "constructor": "Split a conjunctive goal (A ∧ B, A ↔ B) into its components.", "funext": "Prove function extensionality: f = g by proving ∀ x, f x = g x.", "gcongr": "Generalised congruence: prove f a ≤ f b from a ≤ b using monotonicity.", "calc": "Chain of equalities/inequalities; Lean checks transitivity.", "by_cases": "Classical case split on P: one branch h : P, one h : ¬P.", "push_neg": "Push negations inward through quantifiers: ¬∀ x, P x → ∃ x, ¬P x.", "use": "Provide a witness for an existential goal ∃ x, P x.", "aesop": "Meta-tactic: searches for a proof using a configurable rule set.", "tauto": "Propositional tautology solver.", "contrapose": "Replace P → Q with ¬Q → ¬P.", "sorry": "Placeholder: accepts goal without proof. Introduces sorryAx. Marks an open obligation.", "unfold": "Expand a definition in the goal to make it available for other tactics.", "simp_all": "Simplify both goal and all hypotheses simultaneously.", "trivial": "Close trivially-true goals (True, obvious disjunctions).", } def explain_proof(name: str) -> tuple[str, str]: """Return (lean_source, tactic_walkthrough_markdown).""" if not name: return "", "Select a theorem file." t = _get_by_name(name) if t is None: return "", f"Not found: {name}" src = _read_source(t) lines = src.splitlines() # Find tactics found_order: list[tuple[str, int]] = [] # (tactic, line_no) seen: set[str] = set() for i, line in enumerate(lines): stripped = line.strip() if stripped.startswith("--"): continue for tac in TACTIC_DOC: if tac not in seen and re.search(r'\b' + tac + r'\b', stripped): found_order.append((tac, i + 1)) seen.add(tac) # Meta header meta = ( f"**File:** `{t['file']}` \n" f"**Chapter:** {t['chapter']} \n" f"**Status:** {t['status']} " + ("(no `sorry`)" if t['lake_verified'] else f"({t['sorry_count']} `sorry` — open obligation)") + " \n" f"**Lines:** {t['lines']} \n" f"**Theorems defined:** {', '.join(t['theorem_names'][:6]) or '—'} \n" f"**Axioms declared:** {', '.join(t.get('axiom_names', [])) or 'none'} \n" ) if t.get("residual_sorry"): rs = t["residual_sorry"] meta += f"\n> **Residual sorry** line {rs['line']}: {rs['description']}\n" if not found_order: walkthrough = ( meta + "\n---\n\n" "No recognized tactics found. The file may contain only `def`, `abbrev`, or `axiom` declarations." ) return src, walkthrough parts = [meta, "\n---\n", f"\n**{len(found_order)} tactic(s) used** (in order of first appearance):\n"] for step, (tac, lno) in enumerate(found_order, 1): src_line = lines[lno - 1].strip() if lno <= len(lines) else "" parts.append( f"\n### {step}. `{tac}` (line {lno})\n\n" f"{TACTIC_DOC[tac]}\n\n" f"```lean\n{src_line[:120]}\n```\n" ) return src, "\n".join(parts) # --------------------------------------------------------------------------- # Tab 3 — Proof structure + static analysis # --------------------------------------------------------------------------- def static_analysis(name: str) -> str: if not name: return "Select a theorem file to analyse." t = _get_by_name(name) if t is None: return f"Not found: {name}" src = _read_source(t) lines = src.splitlines() # Count various structures thm_defs = [(i+1, l.strip()) for i, l in enumerate(lines) if re.match(r'^(?:theorem|lemma|corollary)\s', l)] ax_defs = [(i+1, l.strip()) for i, l in enumerate(lines) if re.match(r'^axiom\s', l)] sorry_loc = [(i+1, l.strip()) for i, l in enumerate(lines) if 'sorry' in l and not l.strip().startswith('--')] imports = [l.strip() for l in lines if l.startswith('import')] by_count = sum(1 for l in lines if re.search(r'\bby\b', l)) have_count = sum(1 for l in lines if re.search(r'\bhave\b', l)) # Lean4Web URL for the file lean4web_url = build_lean4web_url(src) # Complexity estimate proof_lines = sum(1 for l in lines if l.strip() and not l.strip().startswith('--') and not l.startswith('import')) complexity = "low" if proof_lines < 50 else "medium" if proof_lines < 150 else "high" out = [ f"## Static analysis: `{name}`\n", f"**File:** `{t['file']}` ", f"**Status:** {t['status']} ", f"**Lines:** {t['lines']} ", f"**Proof complexity:** {complexity} ({proof_lines} non-comment, non-import lines)\n", "---\n", f"### Declarations ({len(thm_defs)} theorem/lemma, {len(ax_defs)} axiom)\n", ] for lno, decl in thm_defs[:12]: out.append(f"- Line {lno}: `{decl[:90]}`") if len(thm_defs) > 12: out.append(f"- … ({len(thm_defs) - 12} more)") out.append("") if ax_defs: out.append(f"### Axioms declared ({len(ax_defs)})\n") for lno, decl in ax_defs: out.append(f"- Line {lno}: `{decl[:90]}`") out.append("") if sorry_loc: out.append(f"### Sorry locations ({len(sorry_loc)} — open obligations)\n") for lno, text in sorry_loc: out.append(f"- Line {lno}: `{text[:80]}`") out.append("") else: out.append("### Sorry: none — file is lake-verified\n") out += [ f"### Import summary ({len(imports)} imports)\n", ] mathlib = [i for i in imports if i.startswith("import Mathlib")] lutar = [i for i in imports if i.startswith("import Lutar")] other = [i for i in imports if not i.startswith("import Mathlib") and not i.startswith("import Lutar")] if mathlib: out.append(f"**Mathlib ({len(mathlib)}):** {', '.join(i.replace('import Mathlib.','') for i in mathlib[:6])}" + (" …" if len(mathlib) > 6 else "")) if lutar: out.append(f"**Lutar ({len(lutar)}):** {', '.join(i.replace('import ','') for i in lutar)}") if other: out.append(f"**Other ({len(other)}):** {', '.join(other)}") out.append("") out += [ f"### Proof mechanics\n", f"- `by` tactic blocks: {by_count}", f"- `have` intermediate lemmas: {have_count}", "", "### Open in live Lean 4 WASM IDE\n", f"Click to check this proof in your browser (no Lean install needed):", f"[Open in live.lean-lang.org]({lean4web_url})", "", "> Note: Mathlib imports may time out in the WASM IDE without pre-compiled `.olean` files.", "> For full Mathlib, run `lake build` locally against commit `23480eba`.", ] return "\n".join(out) def build_lean4web_url(code: str) -> str: encoded = urllib.parse.quote(code[:4000]) # URL length limit return f"https://live.lean-lang.org/#code={encoded}" # --------------------------------------------------------------------------- # Tab 4 — DOI / Zenodo cross-link panel # --------------------------------------------------------------------------- def build_doi_panel() -> str: rows = [] for d in DOIS: rows.append( f"| [{d['doi']}](https://doi.org/{d['doi']}) " f"| {d['label']} " f"| [Zenodo](https://zenodo.org/records/{d['doi'].split('.')[-1]}) |" ) return ( "## Thesis DOI Register\n\n" "All thesis versions with persistent DOIs. " f"The canonical citation target is **v18** ([{DOIS[1]['doi']}]({DOIS[1]['url']})).\n\n" "| DOI | Version | Zenodo |\n" "|-----|---------|--------|\n" + "\n".join(rows) + "\n\n---\n\n" "## Proof Library\n\n" f"**GitHub:** [{GITHUB_URL}]({GITHUB_URL}) \n" f"**Proof library DOI:** [{DOIS[2]['doi']}]({DOIS[2]['url']}) \n\n" "### Canonical counts (theorem-level)\n\n" "| Metric | Value | Source |\n" "|--------|-------|--------|\n" f"| Total theorem declarations | {CANON_TOTAL_THMS} | grep over Lutar/ + skeletons |\n" f"| Lake-verified (no sorry) | {CANON_LAKE_VERIFIED} | theorem decls in sorry-free files |\n" f"| Skeleton (sorry present) | {CANON_SKELETONS} | theorem decls in files with sorry |\n" f"| Thesis named theorems | {CANON_THESIS_THMS} | 72 theorem + 4 corollary |\n" f"| Total .lean files in repo | {CANON_TOTAL_FILES} | find lutar-lean -name '*.lean' |\n" f"| Lutar/ directory files | {CANON_LUTAR_FILES} | Lutar/ only |\n" f"| Declared axioms | 13 | 8 files |\n\n" "### Honest disclosure: 1 residual sorry\n\n" f"> **{RESIDUAL_SORRY_FILE}** line {RESIDUAL_SORRY_LINE}: \n" "> `canonicalEncoding_injective` — structural framing proof for SBOM schema formalisation. \n" "> This is a `theorem` (not a new axiom). The structural fact is decidable; proof deferred \n" "> to follow-on PR (P2-IQT-CANONENC-FRAMING). No published result depends on this sorry.\n\n" "---\n\n" "## BibTeX (v18 canonical)\n\n" "```bibtex\n" "@phdthesis{lutar2026thesis,\n" " title = {Lutar: A Lambda-Governance Calculus for Agentic AI Systems},\n" " author = {Lutar, Stephen P.},\n" " year = {2026},\n" " doi = {10.5281/zenodo.20434276},\n" " url = {https://doi.org/10.5281/zenodo.20434276},\n" " note = {206 pp., 76 declared theorems, Lean 4 + Mathlib v4.13.0,\n" " 134 lake-verified theorem declarations,\n" " 1 residual sorry in SBOMProvenance.lean:109}\n" "}\n" "```\n\n" "---\n\n" "## ORCID\n\n" f"[{ORCID}]({ORCID})" ) DOI_PANEL_TEXT = build_doi_panel() # --------------------------------------------------------------------------- # Tab 5 — MadhavaBound + TwoWitness PR status # --------------------------------------------------------------------------- def build_pr_panel(name: str) -> tuple[str, str]: """Return (lean_source_or_empty, pr_status_markdown).""" # Load source for the selected file t = _get_by_name(name) if name else None # PR overview pr = PR_MADHAVA md = [ f"## PR #{pr['number']} — MadhavaBound + TwoWitness\n", f"**Status:** {pr['status']} ", f"**URL:** [{pr['url']}]({pr['url']}) ", f"**Title:** {pr['title']} \n", "---\n", "### What these files prove\n", "**MadhavaBound** (`Lutar/PACBayes/MadhavaBound.lean`): ", "Formalises the Mādhava–Leibniz alternating-series remainder bound, attributed to", "Mādhava of Sangamagrama (~1340–1425 CE), three centuries before Gregory and Leibniz.", "The generic bound states: for any alternating series with monotone-decreasing positive", "terms converging to L, the truncation error after N terms is bounded by the (N+1)-th term.", "", "**TwoWitness** (`Lutar/TwoWitness.lean`): ", "States the Kochen–Specker 18-vector NCHV soundness theorem.", "IF an agent's distribution over 18 KS vectors is a non-contextual hidden-variable", "assignment satisfying the exactly-one-true-per-context rule,", "THEN the runtime witness returns zero inconsistencies.", "The hardness direction (no such assignment exists) is captured as a parity contradiction:", "9 contexts × 2 appearances each = 9 = 2 × (sum of truth values), impossible since 9 is odd.", "", "---\n", f"### Sorry status: {pr['sorry_count']} open obligations\n", f"> {pr['sorry_detail']}\n", "", "These are **tracked open obligations**, not silent gaps.", "Each sorry is annotated in the source with the proof strategy and a follow-on PR reference.", "", "---\n", "### Sources\n", "- Plofker, K. (2009). *Mathematics in India*. Princeton UP, §7.4.", "- Joseph, G. G. (2010). *The Crest of the Peacock*, 3rd ed. Princeton UP, ch. 9.", "- Cabello, A., Estebaranz, J. M., & García-Alcaine, G. (1996).", " Bell-Kochen-Specker theorem: A proof with 18 vectors. *Phys. Lett. A* 212(4), 183–187.", "- Peres, A. (1991). Two simple proofs of the Kochen-Specker theorem. *J. Phys. A* 24, L175.", ] src = "" if t is not None: src = _read_source(t) elif name: # Try to find MadhavaBound or TwoWitness directly for fname in ["MadhavaBound", "TwoWitness"]: candidate = _get_by_name(fname) if candidate: src = _read_source(candidate) break return src, "\n".join(md) def build_pr_panel_static() -> str: _, md = build_pr_panel("") return md # --------------------------------------------------------------------------- # Tab 6 — Open-problem axioms # --------------------------------------------------------------------------- def build_axioms_panel() -> str: total = sum(len(a["axioms"]) for a in DECLARED_AXIOMS) parts = [ f"## Declared Axioms: {total} across {len(DECLARED_AXIOMS)} files\n", "These are **honest declared axioms** (`axiom` keyword in Lean 4), not `sorry` placeholders.", "Each represents a mathematical claim accepted without proof — either because the", "Lean/Mathlib proof is an open engineering task, or because the claim is a standard", "result not yet formalised in Mathlib at the theorem's Mathlib version (v4.13.0).", "", "---\n", ] for entry in DECLARED_AXIOMS: parts.append(f"### `{entry['file']}`\n") parts.append(f"**Axioms:** {', '.join(f'`{a}`' for a in entry['axioms'])} ") parts.append(f"**Note:** {entry['note']}\n") parts += [ "---\n", "## Residual sorry (1)\n", f"**File:** `{RESIDUAL_SORRY_FILE}` line {RESIDUAL_SORRY_LINE} ", "**Name:** `canonicalEncoding_injective` ", "**Type:** `theorem` (not an axiom — no `sorryAx` is asserted as doctrine-clean) ", "**Status:** structural framing proof, open obligation, tracked in follow-on PR ", "**Impact:** no published theorem depends on this sorry\n", "---\n", "## Distinction: axiom vs sorry\n", "| Kind | Lean keyword | Meaning | Count |\n", "|------|-------------|---------|-------|\n", "| Declared axiom | `axiom name : Type` | Accepted without proof; extends the logical foundation | 13 |\n", "| Sorry | `sorry` in proof body | Open obligation; kernel accepts via `sorryAx` | varies by file |\n", "| Lake-verified | zero `sorry` in file | Kernel-checked proof with no sorry | 134 theorem decls |\n", "\n", "**SchurConcave note:** `lambda_schur_concave_n_axis` is declared `axiom`, not `theorem`.", "The mathematical claim is established in Hardy–Littlewood–Pólya (1952);", "the full Lean 4 / Mathlib proof is an open engineering task.", "It is labelled axiom rather than sorry because it is a permanent mathematical foundation", "rather than a temporary proof placeholder.\n", "---\n", f"**GitHub:** [{GITHUB_URL}]({GITHUB_URL}) \n", f"**Thesis DOI:** [{DOIS[1]['doi']}]({DOIS[1]['url']})", ] return "\n".join(parts) AXIOMS_PANEL_TEXT = build_axioms_panel() # --------------------------------------------------------------------------- # Dependency graph (Tab 3 / reused in viewer) # --------------------------------------------------------------------------- MATHLIB_COLORS: dict[str, str] = { "Mathlib.Analysis": "#4C72B0", "Mathlib.Algebra": "#DD8452", "Mathlib.Data": "#55A868", "Mathlib.Topology": "#C44E52", "Mathlib.MeasureTheory": "#8172B2", "Mathlib.NumberTheory": "#937860", "Mathlib.Combinatorics": "#DA8BC3", "Mathlib.Logic": "#8C8C8C", "Mathlib.Order": "#CCB974", "Mathlib.CategoryTheory": "#64B5CD", "Mathlib.Tactic": "#E8735A", "Mathlib.LinearAlgebra": "#2D6A4F", "Mathlib.RingTheory": "#74C476", "Lutar": "#FFD700", } def _mod_color(mod: str) -> str: for prefix, color in MATHLIB_COLORS.items(): if mod.startswith(prefix): return color return "#AAAAAA" def build_dep_graph(name: str) -> go.Figure: empty = go.Figure() empty.update_layout( paper_bgcolor="#0F1117", plot_bgcolor="#0F1117", font_color="white", height=420, xaxis=dict(showgrid=False, zeroline=False, showticklabels=False), yaxis=dict(showgrid=False, zeroline=False, showticklabels=False), ) if not name: empty.add_annotation(text="Select a theorem file to see its import graph", xref="paper", yref="paper", x=0.5, y=0.5, showarrow=False, font=dict(size=14, color="white")) return empty t = _get_by_name(name) if t is None or not t.get("imports"): empty.add_annotation(text=f"No imports found in {name}", xref="paper", yref="paper", x=0.5, y=0.5, showarrow=False, font=dict(size=14, color="white")) return empty imports = t["imports"] n = len(imports) cx, cy, r = 0.5, 0.5, 0.38 nx_list = [cx] + [cx + r * math.cos(2 * math.pi * i / n) for i in range(n)] ny_list = [cy] + [cy + r * math.sin(2 * math.pi * i / n) for i in range(n)] labels = [name] + [imp.split(".")[-1] for imp in imports] colors = ["#FFD700"] + [_mod_color(imp) for imp in imports] sizes = [28] + [15] * n hovers = [name] + imports ex, ey = [], [] for i in range(1, n + 1): ex += [nx_list[0], nx_list[i], None] ey += [ny_list[0], ny_list[i], None] # Sibling edges within same top-2 prefix group groups: dict[str, list[int]] = {} for idx, imp in enumerate(imports): parts = imp.split(".") key = ".".join(parts[:2]) if len(parts) >= 2 else parts[0] groups.setdefault(key, []).append(idx + 1) for members in groups.values(): for j in range(len(members) - 1): i1, i2 = members[j], members[j + 1] ex += [nx_list[i1], nx_list[i2], None] ey += [ny_list[i1], ny_list[i2], None] fig = go.Figure(data=[ go.Scatter(x=ex, y=ey, mode="lines", line=dict(color="#444466", width=1), hoverinfo="none", showlegend=False), go.Scatter(x=nx_list, y=ny_list, mode="markers+text", text=labels, textposition="top center", textfont=dict(size=9, color="white"), marker=dict(size=sizes, color=colors, line=dict(color="white", width=1)), hovertext=hovers, hoverinfo="text", showlegend=False), ]) fig.update_layout( title=dict(text=f"Import graph: {name} ({n} imports)", font=dict(size=13, color="white")), paper_bgcolor="#0F1117", plot_bgcolor="#0F1117", font=dict(color="white"), xaxis=dict(showgrid=False, zeroline=False, showticklabels=False, range=[-0.08, 1.08]), yaxis=dict(showgrid=False, zeroline=False, showticklabels=False, range=[-0.08, 1.08]), height=460, margin=dict(l=10, r=10, t=40, b=10), hoverlabel=dict(bgcolor="#222", font_color="white"), ) return fig # --------------------------------------------------------------------------- # Citation builder (used in Tab 4) # --------------------------------------------------------------------------- def build_citation(name: str) -> str: if not name: return "Select a theorem." t = _get_by_name(name) if t is None: return f"Not found: {name}" thm_list = ", ".join(t["theorem_names"][:4]) or name key = f"lutar_{t['name'].lower()}" status = "lake-verified" if t["lake_verified"] else f"skeleton ({t['sorry_count']} sorry)" return ( f"```bibtex\n" f"@misc{{{key},\n" f" title = {{{{Lean 4 proof: {name} — Lutar Thesis}}}},\n" f" author = {{Lutar, Stephen P.}},\n" f" year = {{2026}},\n" f" howpublished = {{\\url{{{DOIS[1]['url']}}}}},\n" f" note = {{Theorem(s): {thm_list}. Status: {status}. " f"Chapter: {t['chapter']}. File: {t['file']}. " f"GitHub: {GITHUB_URL}. Playground: {SPACE_URL}}}\n" f"}}\n```" ) # --------------------------------------------------------------------------- # App layout # --------------------------------------------------------------------------- CSS = """ body { background: #0F1117; color: #E0E0E0; } .tab-nav button { font-weight: 600; letter-spacing: 0.02em; } footer { display: none !important; } .sorry-banner { background: #2a1a0a; border-left: 3px solid #FF8C00; padding: 8px 12px; border-radius: 4px; font-family: monospace; font-size: 0.85em; color: #FFB347; margin-bottom: 8px; } """ HEADER = f"""
lean-proof-playground SZLHOLDINGS · Apache-2.0 · Doctrine V6 Strict
{CANON_LAKE_VERIFIED} lake-verified · {CANON_SKELETONS} skeletons · {CANON_THESIS_THMS} thesis theorems · 13 declared axioms · 1 residual sorry (SBOMProvenance.lean:109, tracked) — Thesis DOI · GitHub · Catalog browser
""" SORRY_BANNER = """
Honest disclosure: 1 residual sorry in Lutar/SBOMProvenance.lean line 109 (canonicalEncoding_injective — structural framing, tracked, no published theorem depends on it). 13 declared axioms across 8 files. See Tab 6 for full list.
""" def create_app() -> gr.Blocks: names = _all_names() chapters = _all_chapters() statuses = _all_statuses() # Separate MadhavaBound / TwoWitness names for Tab 5 pr_names = [n for n in names if n in {"MadhavaBound", "TwoWitness"}] pr_default = pr_names[0] if pr_names else (names[0] if names else None) with gr.Blocks( title="Lean Proof Playground — SZL Thesis", css=CSS, theme=gr.themes.Base( primary_hue="blue", secondary_hue="yellow", neutral_hue="slate", ).set( body_background_fill="#0F1117", body_text_color="#E0E0E0", block_background_fill="#1a1a2e", block_border_color="#2a2a4a", input_background_fill="#0d1b2a", ), ) as demo: gr.HTML(HEADER) gr.HTML(SORRY_BANNER) with gr.Tabs(): # ─── Tab 1: Theorem Index Browser ───────────────────────────── with gr.Tab("Theorem Index"): gr.Markdown( f"All **{len(THEOREMS)} files** ({CANON_LAKE_VERIFIED} lake-verified theorem decls, " f"{CANON_SKELETONS} skeleton decls). Filter by chapter, status, or keyword." ) with gr.Row(): t1_search = gr.Textbox(label="Search", placeholder="name, chapter, theorem…", scale=3) t1_status = gr.Dropdown(choices=statuses, value="All", label="Status", scale=1) t1_chapter = gr.Dropdown(choices=chapters, value="All", label="Chapter", scale=2) t1_table = gr.Dataframe( headers=LIB_HEADERS, value=build_library(), interactive=False, wrap=False, row_count=(20, "dynamic"), col_count=(len(LIB_HEADERS), "fixed"), ) t1_stats = gr.Markdown( f"**{len(THEOREMS)} entries** | " f"Lake-verified files: {sum(1 for t in THEOREMS if t['lake_verified'])} | " f"Sorry files: {sum(1 for t in THEOREMS if not t['lake_verified'])}" ) def refresh_lib(search, status, chapter): rows = build_library(search, status, chapter) return rows, f"**Showing {len(rows)} entries** | search=`{search or 'all'}` status=`{status}` chapter=`{chapter}`" for w in [t1_search, t1_status, t1_chapter]: w.change(refresh_lib, inputs=[t1_search, t1_status, t1_chapter], outputs=[t1_table, t1_stats]) # ─── Tab 2: Proof Viewer + Tactic Explanation ───────────────── with gr.Tab("Proof Viewer"): gr.Markdown( "Select a file to view its **Lean 4 source** and a " "step-by-step explanation of each tactic used." ) with gr.Row(): t2_sel = gr.Dropdown(choices=names, value=names[0] if names else None, label="Theorem file", filterable=True, scale=4) t2_btn = gr.Button("Load", variant="primary", scale=1) t2_meta = gr.Markdown() with gr.Row(): t2_src = gr.Code(label="Lean 4 source", language=None, interactive=False, lines=28, scale=3) t2_walk = gr.Markdown() t2_graph = gr.Plot(label="Import graph") def load_proof(name): src, walk = explain_proof(name) graph = build_dep_graph(name) return src, walk, graph t2_btn.click(load_proof, inputs=[t2_sel], outputs=[t2_src, t2_walk, t2_graph]) t2_sel.change(load_proof, inputs=[t2_sel], outputs=[t2_src, t2_walk, t2_graph]) if names: demo.load(lambda: load_proof(names[0]), outputs=[t2_src, t2_walk, t2_graph]) # ─── Tab 3: Static Analysis + Lean4Web ──────────────────────── with gr.Tab("Proof Analysis"): gr.Markdown( "Static analysis of proof structure: declarations, imports, sorry locations, " "tactic counts, complexity estimate. " "Generates a [live.lean-lang.org](https://live.lean-lang.org/) " "link so you can check the proof in a browser-based Lean 4 WASM IDE." ) gr.Markdown( "> No server-side Lean is running in this Space. " "All analysis is static (file parsing). " "Live type-checking uses the external Lean 4 WASM IDE." ) with gr.Row(): t3_sel = gr.Dropdown(choices=names, value=names[0] if names else None, label="Theorem file", filterable=True, scale=4) t3_btn = gr.Button("Analyse", variant="primary", scale=1) t3_out = gr.Markdown() t3_btn.click(static_analysis, inputs=[t3_sel], outputs=[t3_out]) t3_sel.change(static_analysis, inputs=[t3_sel], outputs=[t3_out]) if names: demo.load(lambda: static_analysis(names[0]), outputs=[t3_out]) # ─── Tab 4: DOI / Zenodo Panel ───────────────────────────────── with gr.Tab("DOI Register"): gr.Markdown(DOI_PANEL_TEXT) gr.Markdown("---\n\n### Theorem citation builder\n\nSelect a theorem to generate a BibTeX entry.") with gr.Row(): t4_sel = gr.Dropdown(choices=names, value=names[0] if names else None, label="Theorem", filterable=True, scale=4) t4_btn = gr.Button("Generate BibTeX", variant="secondary", scale=1) t4_cite = gr.Markdown() t4_btn.click(build_citation, inputs=[t4_sel], outputs=[t4_cite]) t4_sel.change(build_citation, inputs=[t4_sel], outputs=[t4_cite]) if names: demo.load(lambda: build_citation(names[0]), outputs=[t4_cite]) # ─── Tab 5: MadhavaBound + TwoWitness PR status ──────────────── with gr.Tab("PR Status"): gr.Markdown( f"Status of PR [#{PR_MADHAVA['number']}]({PR_MADHAVA['url']}) — " f"MadhavaBound and TwoWitness. " f"**{PR_MADHAVA['sorry_count']} tracked sorry placeholders** — " f"open obligations, not silent gaps." ) with gr.Row(): t5_sel = gr.Dropdown( choices=names, value=pr_default, label="View source (MadhavaBound / TwoWitness)", filterable=True, scale=4, ) t5_btn = gr.Button("Load", variant="secondary", scale=1) with gr.Row(): t5_src = gr.Code(label="Source", language=None, interactive=False, lines=25, scale=3) t5_md = gr.Markdown(value=build_pr_panel_static()) def load_pr(name): src, _ = build_pr_panel(name) return src t5_btn.click(load_pr, inputs=[t5_sel], outputs=[t5_src]) t5_sel.change(load_pr, inputs=[t5_sel], outputs=[t5_src]) if pr_default: demo.load(lambda: load_pr(pr_default), outputs=[t5_src]) # ─── Tab 6: Axioms (open problems) ───────────────────────────── with gr.Tab("Axioms and Open Problems"): gr.Markdown(AXIOMS_PANEL_TEXT) gr.HTML( f"""
lean-proof-playground · SZLHOLDINGS · Apache-2.0 · Doctrine V6 Strict · DOI 10.5281/zenodo.20434276 · GitHub · ORCID 0009-0001-0110-4173
""" ) return demo # --------------------------------------------------------------------------- # Entry point # --------------------------------------------------------------------------- if __name__ == "__main__": app = create_app() app.launch(server_name="0.0.0.0", server_port=7860, show_error=True)