| """ |
| 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 |
|
|
| |
| |
| |
|
|
| 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" |
|
|
| |
| CANON_TOTAL_THMS = 375 |
| CANON_LAKE_VERIFIED = 134 |
| CANON_SKELETONS = 241 |
| CANON_THESIS_THMS = 76 |
| CANON_TOTAL_FILES = 6022 |
| CANON_LUTAR_FILES = 71 |
| RESIDUAL_SORRY_FILE = "Lutar/SBOMProvenance.lean" |
| RESIDUAL_SORRY_LINE = 109 |
|
|
| |
| 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_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 = [ |
| {"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"}, |
| ] |
|
|
| |
| |
| |
|
|
| 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"] |
|
|
|
|
| |
| |
| |
|
|
| 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 |
|
|
|
|
| |
| |
| |
|
|
| 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() |
|
|
| |
| found_order: list[tuple[str, int]] = [] |
| 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 = ( |
| 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) |
|
|
|
|
| |
| |
| |
|
|
| 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() |
|
|
| |
| 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 = build_lean4web_url(src) |
|
|
| |
| 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]) |
| return f"https://live.lean-lang.org/#code={encoded}" |
|
|
|
|
| |
| |
| |
|
|
| 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() |
|
|
|
|
| |
| |
| |
|
|
| def build_pr_panel(name: str) -> tuple[str, str]: |
| """Return (lean_source_or_empty, pr_status_markdown).""" |
| |
| t = _get_by_name(name) if name else None |
|
|
| |
| 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: |
| |
| 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 |
|
|
|
|
| |
| |
| |
|
|
| 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() |
|
|
|
|
| |
| |
| |
|
|
| 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] |
|
|
| |
| 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 |
|
|
|
|
| |
| |
| |
|
|
| 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```" |
| ) |
|
|
|
|
| |
| |
| |
|
|
| 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""" |
| <div style="background:linear-gradient(135deg,#0d1b2a,#1a1a2e); |
| border-left:4px solid #FFD700;padding:12px 16px;border-radius:6px;margin-bottom:8px;"> |
| <span style="color:#FFD700;font-size:1.3em;font-weight:700;">lean-proof-playground</span> |
| <span style="color:#9ECFFF;font-size:0.9em;margin-left:12px;"> |
| SZLHOLDINGS · Apache-2.0 · Doctrine V6 Strict |
| </span><br/> |
| <span style="color:#888;font-size:0.8em;"> |
| {CANON_LAKE_VERIFIED} lake-verified · {CANON_SKELETONS} skeletons · |
| {CANON_THESIS_THMS} thesis theorems · 13 declared axioms · |
| 1 residual sorry (SBOMProvenance.lean:109, tracked) |
| — |
| <a href="{THESIS_DOI}" target="_blank" style="color:#FFD700;">Thesis DOI</a> |
| · |
| <a href="{GITHUB_URL}" target="_blank" style="color:#FFD700;">GitHub</a> |
| · |
| <a href="{BROWSER_SPACE}" target="_blank" style="color:#FFD700;">Catalog browser</a> |
| </span> |
| </div> |
| """ |
|
|
| SORRY_BANNER = """ |
| <div class="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. |
| </div> |
| """ |
|
|
|
|
| def create_app() -> gr.Blocks: |
| names = _all_names() |
| chapters = _all_chapters() |
| statuses = _all_statuses() |
|
|
| |
| 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(): |
|
|
| |
| 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]) |
|
|
| |
| 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]) |
|
|
| |
| 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]) |
|
|
| |
| 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]) |
|
|
| |
| 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]) |
|
|
| |
| with gr.Tab("Axioms and Open Problems"): |
| gr.Markdown(AXIOMS_PANEL_TEXT) |
|
|
| gr.HTML( |
| f"""<div style="text-align:center;padding:8px;color:#555;font-size:0.78em; |
| border-top:1px solid #222;margin-top:8px;"> |
| lean-proof-playground · SZLHOLDINGS · Apache-2.0 · |
| Doctrine V6 Strict · |
| <a href="{THESIS_DOI}" target="_blank" style="color:#9ECFFF;"> |
| DOI 10.5281/zenodo.20434276</a> · |
| <a href="{GITHUB_URL}" target="_blank" style="color:#9ECFFF;">GitHub</a> · |
| <a href="{ORCID}" target="_blank" style="color:#9ECFFF;"> |
| ORCID 0009-0001-0110-4173</a> |
| </div>""" |
| ) |
|
|
| return demo |
|
|
|
|
| |
| |
| |
|
|
| if __name__ == "__main__": |
| app = create_app() |
| app.launch(server_name="0.0.0.0", server_port=7860, show_error=True) |
|
|
