Q.E.D — initial submission

README.md

@@ -0,0 +1,94 @@
+---
+title: Q.E.D
+emoji: ⊢
+colorFrom: green
+colorTo: gray
+sdk: gradio
+app_file: front.py
+pinned: true
+license: mit
+short_description: LLM-guided formal verification — AI proposes tactics, Lean's kernel certifies the proof
+tags:
+  - track:wood
+  - sponsor:modal
+  - achievement:offbrand
+  - achievement:best-demo
+  - gradio
+  - lean4
+  - formal-verification
+  - agents
+  - build-small-hackathon
+---
+
+# ⊢ Q.E.D
+
+An LLM-guided formal verification agent. You give it a theorem statement in Lean 4; it finds a proof that **Lean's kernel certifies as formally correct**.
+
+Unlike a chatbot saying "yes, that's true," Lean's kernel is a proof-checker that either accepts or rejects every logical step against its axioms. No hallucinations. No approximations. The result is machine-checked mathematics.
+
+## Demo
+
+📹 **[DEMO VIDEO: paste URL here]**
+
+🐦 **[SOCIAL POST: paste URL here]**
+
+## What it does
+
+The agent runs a propose → verify → learn loop, using a 27B LLM (well under the 32B limit) to propose Lean 4 proof tactics, Lean's kernel to verify each one, and the kernel's error messages fed back verbatim into the next prompt:
+
+```
+theorem
+  → propose 3 tactic candidates (27B LLM via Modal)
+  → verify each in live Lean 4 REPL (Modal container)
+  → kernel rejects? → error text fed back to LLM
+  → kernel accepts? → advance proof state
+  → repeat until complete or stuck
+```
+
+Key behaviours:
+
+- **Fallback layer** — deterministic tactics (`rfl`, `norm_num`, `simp`, `omega`, `contradiction`, `assumption`) are tried at each step before the LLM is called.
+- **Stuck-state detector** — if the same proof state recurs 3 times, or 3 consecutive steps all fail, the agent concludes "not provable as stated" and returns a clean verdict instead of looping indefinitely. This correctly identifies false theorems.
+- **No cache on demo runs** — every run executes the full live loop so the propose→verify→learn steps are always visible.
+
+**Model**: one model, Qwen3-27B quantized (Q4_K_M GGUF) served via llama.cpp. 27B < 32B. ✓
+
+## Best Use of Modal
+
+Two Modal deployments power the app:
+
+| App | What it runs |
+|---|---|
+| `lean-proof-agent` | FastAPI app with a persistent Lean 4 REPL. `min_containers=1` keeps it warm so there is zero cold-start delay. Runs the full agent loop and orchestrates the LLM calls. |
+| `llama-server` | llama.cpp HTTP server running **Qwen3-27B (Q4_K_M)** on a Modal GPU. Receives the current proof state as context, returns tactic candidates. |
+
+Why Modal specifically:
+
+- Lean 4 requires a **persistent REPL process** with the full toolchain installed and pre-warmed — not something you can spin up per-request. Modal containers hold that state across calls.
+- `min_containers=1` means the Lean server is **always alive**, which is critical for a live demo with ~30-second proof runs.
+- The LLM needs a GPU. Modal's on-demand GPU allocation means no dedicated hardware to maintain.
+- The two apps are **independently scaled**: REPL is CPU-bound, LLM is GPU-bound.
+
+## Off Brand — custom UI
+
+The frontend is not stock Gradio. Every proof run produces a **live-rendered SVG proof tree** built from the agent's search trace: goal-state nodes connected by tactic edges, failed branches in red, the accepted path in green, a terminal QED node. It runs in the browser with zero JS dependencies — generated server-side and injected as HTML.
+
+The overall aesthetic is a dark mathematical terminal: JetBrains Mono, GitHub-dark palette (`#0d1117` background, `#2ea043` green accent), styled to match the proof tree's colour scheme.
+
+## Best Agent — agent loop design
+
+The proof search is a genuine multi-step agentic loop with external tool use and error-driven self-correction:
+
+- **Propose**: LLM generates 3 tactic candidates given the current proof state and the previous kernel error (if any)
+- **Verify**: Lean's formal kernel checks each candidate — this is ground truth, not a heuristic
+- **Learn**: the exact kernel error message is injected back into the next LLM prompt
+- **Decide**: best partial-progress result is selected; all-failed steps increment a failure counter
+- **Conclude**: stuck-state detector fires a deliberate "not provable" verdict rather than hitting the step limit
+
+The agent correctly proves true theorems and correctly identifies false ones — both happen live on every run.
+
+## Try it
+
+Load any example theorem and click **⊢ Prove**. The step walkthrough shows every LLM candidate, which ones the kernel rejected, the error fed back, and the tactic that advanced the proof.
+
+Each completed proof includes a pre-filled link to [live.lean-lang.org](https://live.lean-lang.org/) so you can paste it into Lean's web kernel and see "Goals accomplished!" yourself.

back.py

@@ -0,0 +1,264 @@
+import modal
+import hashlib
+from fastapi import FastAPI
+from pydantic import BaseModel
+
+app = modal.App("lean-proof-agent")
+
+image = (
+    modal.Image.debian_slim()
+    .apt_install("curl", "git", "build-essential")
+    .pip_install("lean-interact", "requests", "fastapi")
+    .run_commands(
+        "curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:v4.14.0",
+    )
+    .env({"PATH": "/root/.elan/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin"})
+
+    .run_commands(
+        'python -c "from lean_interact import LeanREPLConfig; LeanREPLConfig()"'
+    )
+)
+
+
+
+
+
+LLAMA_ENDPOINT = "https://no-name13--llama-server-serve.modal.run/v1/chat/completions"
+
+web_app = FastAPI()
+
+class ProveRequest(BaseModel):
+    theorem: str
+    max_steps: int = 20
+    use_fallbacks: bool = True
+    show_reasoning: bool = True  # when True, skip cache read so the full agent loop always runs
+
+class StepLog(BaseModel):
+    step: int
+    goal: str
+    candidates: list[str]
+    chosen: str
+    status: str
+    error: str | None = None
+
+class ProveResponse(BaseModel):
+    success: bool
+    stuck: bool = False
+    tactics: list[str]
+    steps: list[StepLog]
+    message: str
+
+
+@app.function(
+    image=image,
+    timeout=300,
+    min_containers=1,
+)
+@modal.asgi_app()
+def fastapi_app():
+    from lean_interact import LeanServer, LeanREPLConfig, Command, ProofStep
+    from lean_interact.interface import LeanError
+    import requests
+
+    config = LeanREPLConfig()
+    server = LeanServer(config)
+
+    FALLBACK_TACTICS = ["rfl", "norm_num", "simp", "omega", "contradiction", "assumption"]
+    NUM_CANDIDATES = 3
+    lemma_cache: dict[str, list[str]] = {}
+
+
+    def ask_model(goal_state, last_error=None, num_candidates=3):
+        error_context = ""
+        if last_error:
+            error_context = (
+                f"\nThe previous tactic failed with this error:\n{last_error}\n"
+                f"IMPORTANT: if the error says 'major premise type is not an inductive type', "
+                f"it means you must use `intro` to bring variables into context BEFORE using `induction`.\n"
+            )
+        prompt = (
+            f"You are a Lean 4 theorem prover. Given this proof state:\n\n{goal_state}\n"
+            f"{error_context}\n"
+            f"Suggest the next single tactic. Output ONLY the tactic, no backticks, no explanation.\n"
+            f"RULES:\n"
+            f"- do NOT use `omega`, `decide`, `tauto`\n"
+            f"- do NOT use `apply Nat.add_comm` (using a named library lemma as a shortcut)\n"
+            f"- ALLOWED closing tactics — use these freely when they fit:\n"
+            f"  `exact h` or `exact ⟨h1, h2⟩` (provide a proof term directly)\n"
+            f"  `contradiction` (when context contains P and ¬P)\n"
+            f"  `assumption` (when goal matches a hypothesis exactly)\n"
+            f"  `absurd h1 h2` (derive False from h1 : P and h2 : ¬P)\n"
+            f"- always use fresh, distinct variable names when introducing (e.g. `intro n`, `intro P`, `intro Q`) — never reuse a name already present in the context\n"
+            f"- if the goal starts with `∀`, always use `intro` first before anything else\n"
+            f"- when using induction, always provide full case syntax:\n"
+            f"  induction n with\n  | zero => simp\n  | succ n ih => simp [ih]"
+        )
+
+        tactics = []
+        for _ in range(num_candidates):
+            try:
+                payload = {
+                    "model": "any",
+                    "messages": [{"role": "user", "content": prompt}],
+                    "max_tokens": 200,
+                    "stream": False,
+                    "temperature": 0.8,
+                    "chat_template_kwargs": {"enable_thinking": False}
+                }
+                resp = requests.post(LLAMA_ENDPOINT, json=payload, timeout=30)
+                resp.raise_for_status()
+                tactic = resp.json()["choices"][0]["message"]["content"].strip().strip("`").strip()
+                if tactic and tactic not in tactics:
+                    tactics.append(tactic)
+            except Exception:
+                break
+        return tactics
+
+    def try_tactic(tactic, proof_state_id):
+        result = server.run(ProofStep(tactic=tactic, proof_state=proof_state_id))
+        if isinstance(result, LeanError):
+            return None, result.message
+        return result, None
+
+    def try_fallbacks(proof_state_id, enabled):
+        if not enabled:
+            return None, None
+        for tactic in FALLBACK_TACTICS:
+            result, _ = try_tactic(tactic, proof_state_id)
+            if result is not None and "sorry" not in result.proof_status:
+                return result, tactic
+        return None, None
+
+    @web_app.post("/prove", response_model=ProveResponse)
+    def prove(req: ProveRequest):
+        steps = []
+        response = server.run(Command(cmd=f"{req.theorem} := by sorry"))
+
+        if not response.sorries:
+            if any(m.data == "Goals accomplished!" for m in response.messages):
+                return ProveResponse(success=True, tactics=[], steps=[], message="Proved trivially!")
+            return ProveResponse(success=False, tactics=[], steps=[], message="Could not get initial proof state")
+
+        proof_state_id = response.sorries[0].proof_state
+        current_goals = [response.sorries[0].goal]
+
+        goal_hash = hashlib.md5(current_goals[0].encode()).hexdigest()
+        if not req.show_reasoning and goal_hash in lemma_cache:
+            cached = lemma_cache[goal_hash]
+            return ProveResponse(
+                success=True, tactics=cached, steps=[],
+                message=f"Proved from cache ({len(cached)} tactic(s))!"
+            )
+
+        tactics = []
+        last_error = None
+        visited = set()
+        llm_ever_responded = False
+        consecutive_failures = 0  # all_failed steps in a row
+        goal_seen: dict[str, int] = {}  # goal text → times seen
+        STUCK_THRESHOLD = 3
+
+        for step in range(req.max_steps):
+            goal_text = "\n".join(current_goals)
+            if not goal_text.strip():
+                break
+
+            # Stuck-state detection: same goal returning, or consecutive dead ends
+            goal_seen[goal_text] = goal_seen.get(goal_text, 0) + 1
+            if goal_seen[goal_text] >= STUCK_THRESHOLD or consecutive_failures >= STUCK_THRESHOLD:
+                return ProveResponse(
+                    success=False, stuck=True, tactics=tactics, steps=steps,
+                    message=(
+                        "Search stuck — the same goal state recurred with no progress. "
+                        "This theorem is likely not provable in the current theory: "
+                        "it may require classical logic (Law of Excluded Middle), "
+                        "or a tactic the agent is constrained from using."
+                    ),
+                )
+
+            result, fallback_tactic = try_fallbacks(proof_state_id, req.use_fallbacks)
+            if result is not None:
+                tactics.append(fallback_tactic)
+                steps.append(StepLog(
+                    step=step, goal=goal_text,
+                    candidates=[fallback_tactic], chosen=fallback_tactic,
+                    status=result.proof_status
+                ))
+                if result.proof_status == "Completed":
+                    lemma_cache[goal_hash] = list(tactics)
+                    return ProveResponse(success=True, tactics=tactics, steps=steps,
+                                        message=f"Proved in {step+1} steps!")
+                proof_state_id = result.proof_state
+                current_goals = result.goals
+                last_error = None
+                consecutive_failures = 0
+                continue
+
+            candidates = ask_model(goal_text, last_error=last_error, num_candidates=NUM_CANDIDATES)
+            if not candidates:
+                steps.append(StepLog(
+                    step=step, goal=goal_text,
+                    candidates=[], chosen="",
+                    status="model_unavailable", error="LLM endpoint cold/unavailable — retrying"
+                ))
+                continue  # don't count toward stuck-state; just burn a step and retry
+
+            llm_ever_responded = True
+            best_result = None
+            best_tactic = None
+            step_error = None
+
+            for tactic in candidates:
+                key = (proof_state_id, tactic)
+                if key in visited:
+                    continue
+                visited.add(key)
+                result, error = try_tactic(tactic, proof_state_id)
+                if result is None:
+                    last_error = error
+                    step_error = error
+                    continue
+                if "sorry" in result.proof_status:
+                    last_error = "That tactic left sorry holes. Provide the full proof of each case inline."
+                    continue
+                if result.proof_status == "Completed":
+                    tactics.append(tactic)
+                    steps.append(StepLog(
+                        step=step, goal=goal_text,
+                        candidates=candidates, chosen=tactic,
+                        status="Completed"
+                    ))
+                    lemma_cache[goal_hash] = list(tactics)
+                    return ProveResponse(success=True, tactics=tactics, steps=steps,
+                                        message=f"Proved in {step+1} steps!")
+                if best_result is None or len(result.goals) < len(best_result.goals):
+                    best_result = result
+                    best_tactic = tactic
+
+            if best_result is not None:
+                tactics.append(best_tactic)
+                steps.append(StepLog(
+                    step=step, goal=goal_text,
+                    candidates=candidates, chosen=best_tactic,
+                    status=best_result.proof_status
+                ))
+                proof_state_id = best_result.proof_state
+                current_goals = best_result.goals
+                last_error = None
+                consecutive_failures = 0
+            else:
+                consecutive_failures += 1
+                steps.append(StepLog(
+                    step=step, goal=goal_text,
+                    candidates=candidates, chosen="",
+                    status="all_failed", error=step_error
+                ))
+
+        fail_msg = (
+            "LLM endpoint warming up — fallback tactics only. Failed within max steps."
+            if not llm_ever_responded
+            else "Failed within max steps"
+        )
+        return ProveResponse(success=False, tactics=tactics, steps=steps, message=fail_msg)
+
+    return web_app

back_modal.py

@@ -0,0 +1,145 @@
+import modal
+import subprocess
+
+app = modal.App("llama-server")
+
+MINUTES = 60
+GPU_CONFIG = "A100-40GB"
+cache_dir = "/root/.cache/llama.cpp"
+
+#REPO_ID = "google/gemma-4-31B-it-qat-q4_0-gguf"
+#MODEL_FILE = "gemma-4-31B_q4_0-it.gguf"
+#MMPROJ_FILE = "gemma-4-31B-it-mmproj.gguf"
+
+
+REPO_ID = "unsloth/Qwen3.6-27B-GGUF"
+MODEL_FILE = "Qwen3.6-27B-Q4_K_M.gguf"
+
+
+cuda_tag = "12.4.0-devel-ubuntu22.04"
+
+model_cache = modal.Volume.from_name("llamacpp-cache", create_if_missing=True)
+
+image = (
+    modal.Image.from_registry(f"nvidia/cuda:{cuda_tag}", add_python="3.11")
+    .apt_install(
+        "git",
+        "build-essential",
+        "cmake",
+        "curl",
+        "libcurl4-openssl-dev",
+        "libssl-dev",
+    )
+    .run_commands("git clone https://github.com/ggerganov/llama.cpp && cd llama.cpp && git pull origin master")
+    .run_commands(
+        "cmake llama.cpp -B llama.cpp/build "
+        "-DBUILD_SHARED_LIBS=OFF -DGGML_CUDA=ON -DLLAMA_CURL=ON -DLLAMA_OPENSSL=ON"
+    )
+    .run_commands(
+        "cmake --build llama.cpp/build --config Release -j "
+        "--target llama-server "
+    )
+    .run_commands("cp llama.cpp/build/bin/llama-server /usr/local/bin/")
+    .entrypoint([])
+)
+
+download_image = (
+    modal.Image.debian_slim(python_version="3.11")
+    .pip_install("huggingface_hub[hf_transfer]==0.26.2")
+    .env({"HF_HUB_ENABLE_HF_TRANSFER": "1"})
+)
+
+
+@app.function(
+    image=download_image,
+    volumes={cache_dir: model_cache},
+    timeout=20 * MINUTES,
+)
+def download_model():
+    from huggingface_hub import hf_hub_download
+
+    for filename in [MODEL_FILE]: #, MMPROJ_FILE 
+        hf_hub_download(
+            repo_id=REPO_ID,
+            filename=filename,
+            local_dir=cache_dir,
+        )
+
+    model_cache.commit()
+
+
+@app.function(
+    image=image,
+    gpu=GPU_CONFIG,
+    volumes={cache_dir: model_cache},
+    timeout=60 * MINUTES,
+    max_containers=1,
+    min_containers=1, #← for judging so that judges can start with a warm container
+)
+
+@modal.web_server(port=8080, startup_timeout=5 * MINUTES)
+def serve():
+     import shutil
+     import os
+     import urllib.request
+     import json
+     import time
+
+     local_model = f"/tmp/{MODEL_FILE}"
+     #local_mmproj = f"/tmp/{MMPROJ_FILE}"
+
+     if not os.path.exists(local_model):
+        print("Copying model to local storage...", flush=True)
+        shutil.copy2(f"{cache_dir}/{MODEL_FILE}", local_model)
+
+        #shutil.copy2(f"{cache_dir}/{MMPROJ_FILE}", local_mmproj)
+        print("Copy complete.", flush=True)
+
+     subprocess.Popen([
+        "llama-server",
+        "-m",local_model ,
+       # "--mmproj", local_mmproj, 
+        "--host", "0.0.0.0",
+        "--port", "8080",
+        "--ctx-size", "4096",
+        "-ngl", "999",
+        "--flash-attn","on", 
+        "-np","1",
+        "-b", "2048",
+        "-ub", "512",
+        "--cache-type-k", "q8_0",
+        "--cache-type-v", "q8_0",
+        "-t", "8",
+        #"--no-mmap",  ← loads weight into ram/not needed because of tmp 
+        #"--no-warmup",  skip empty run 
+    ])
+
+        # wait for server ready
+     for _ in range(60):
+            try:
+                urllib.request.urlopen("http://localhost:8080/health")
+                break
+            except Exception:
+                time.sleep(5)
+
+        # fire a real request to compile actual CUDA graphs
+     payload = json.dumps({
+            "model": "any",
+            "messages": [{"role": "user", "content": "hi"}],
+            "max_tokens": 10,
+            "chat_template_kwargs": {"enable_thinking": False}
+        }).encode()
+     req = urllib.request.Request(
+            "http://localhost:8080/v1/chat/completions",
+            data=payload,
+            headers={"Content-Type": "application/json"}
+        )
+     urllib.request.urlopen(req)
+     print("Warmup complete.", flush=True)
+
+
+
+
+@app.local_entrypoint()
+def main():
+    download_model.remote()

front.py

@@ -0,0 +1,572 @@
+import urllib.parse
+import gradio as gr
+import requests
+
+MODAL_ENDPOINT = "https://no-name13--lean-proof-agent-fastapi-app.modal.run"
+
+# ── Example theorems ──────────────────────────────────────────────────────────
+# Lead with add_comm_nat (induction / multi-step) so the agent loop is visible.
+# Keep zero_add as the simple contrast. False theorem always last.
+EXAMPLES = [
+    (
+        "theorem add_comm_nat : ∀ n m : Nat, n + m = m + n",
+        "∀ n m · n + m = m + n — addition is commutative",
+        "provable",
+    ),
+    (
+        "theorem reverse_reverse : ∀ (α : Type) (l : List α), l.reverse.reverse = l",
+        "∀ α l · reverse(reverse l) = l — reversing a list twice is identity",
+        "provable",
+    ),
+    (
+        "theorem zero_add : ∀ n : Nat, 0 + n = n",
+        "∀ n · 0 + n = n — zero is the left identity for addition",
+        "provable",
+    ),
+    (
+        "theorem currying : ∀ P Q R : Prop, (P ∧ Q → R) ↔ (P → Q → R)",
+        "∀ P Q R · (P∧Q→R) ↔ (P→Q→R) — currying",
+        "provable",
+    ),
+    (
+        "theorem de_morgan_and : ∀ P Q : Prop, ¬(P ∧ Q) ↔ ¬P ∨ ¬Q",
+        "∀ P Q · ¬(P∧Q) ↔ ¬P∨¬Q — De Morgan's law",
+        "provable",
+    ),
+    # FALSE theorem — the stuck detector concludes "not provable" within a few steps.
+    (
+        "theorem cannot_prove : ∀ n : Nat, n + 1 = n",
+        "∀ n · n+1 = n — FALSE: the agent correctly cannot prove this ✗",
+        "unprovable",
+    ),
+]
+
+EXAMPLE_LOOKUP = {lean.strip(): (desc, kind) for lean, desc, kind in EXAMPLES}
+
+TACTIC_EXPLANATIONS = {
+    "intro": "introduces a universally quantified variable or hypothesis into the local context",
+    "induction": "applies structural induction — splits into base case (zero) and inductive step (succ)",
+    "simp": "simplifies the goal using a library of known equalities and lemmas",
+    "rfl": "closes the goal when both sides are definitionally equal",
+    "omega": "decision procedure for linear arithmetic — automatically solves goals about integers/naturals",
+    "rw": "rewrites the goal using an equation",
+    "exact": "closes the goal by providing an exact proof term",
+    "apply": "applies a lemma whose conclusion matches the goal",
+    "constructor": "splits a conjunction (∧) or iff (↔) goal into its two parts",
+    "cases": "case-splits on a hypothesis or value",
+    "norm_num": "solves numeric goals like 2 + 2 = 4 or 3 ∣ 6",
+    "contradiction": "closes the goal when context contains P and ¬P (a direct contradiction)",
+    "assumption": "closes the goal when it matches a hypothesis in the local context exactly",
+    "tauto": "closes propositional tautologies automatically",
+}
+
+# ── Dark theme — mathematical / formal-proof terminal aesthetic ───────────────
+# Wraps in try/except so a theme API mismatch never breaks the app.
+CUSTOM_CSS = """
+/* ── Base ───────────────────────────────────────────────── */
+body, .gradio-container { background: #0d1117 !important; color: #c9d1d9 !important; }
+.contain, .gap, .row { background: #0d1117 !important; }
+
+/* ── Panels ─────────────────────────────────────────────── */
+.block.padded, .block {
+    background: #161b22 !important;
+    border: 1px solid #30363d !important;
+    border-radius: 8px !important;
+}
+.form { background: #161b22 !important; }
+
+/* ── All text — catch-all first, then specifics ──────────── */
+* { color: #c9d1d9; }
+
+/* ── Headings ────────────────────────────────────────────── */
+h1, h2, h3, h4 { color: #e6edf3 !important; }
+h1 { border-bottom: 1px solid #21262d; padding-bottom: 6px; }
+
+/* ── Labels (component titles, slider/checkbox labels) ────── */
+label, .label-wrap, .label-wrap span,
+span.text-gray-500, span.text-sm,
+.block > .label-wrap > span { color: #b0bec5 !important; }
+
+/* ── Body text, lists, paragraphs ───────────────────────── */
+p, li, em, span { color: #c9d1d9 !important; }
+a { color: #58a6ff !important; }
+strong, b { color: #e6edf3 !important; }
+
+/* ── Slider ──────────────────────────────────────────────── */
+input[type=range] { accent-color: #2ea043 !important; }
+.range-input span, .range-input output,
+input[type=range] + span, .slider-container span { color: #c9d1d9 !important; }
+
+/* ── Checkbox ─────────────────────────��──────────────────── */
+input[type=checkbox] { accent-color: #2ea043 !important; }
+.checkbox-label, .checkbox-label span { color: #c9d1d9 !important; }
+
+/* ── Inputs ──────────────────────────────────────────────── */
+textarea, input[type=text], input[type=number] {
+    background: #0d1117 !important;
+    color: #e6edf3 !important;
+    border: 1px solid #30363d !important;
+    border-radius: 6px !important;
+    font-family: 'JetBrains Mono', 'Fira Code', ui-monospace, monospace !important;
+}
+textarea::placeholder { color: #484f58 !important; }
+
+/* ── Primary button ──────────────────────────────────────── */
+button.primary {
+    background: #1a3a1a !important;
+    border: 1px solid #2ea043 !important;
+    color: #3fb950 !important;
+    font-weight: bold !important;
+    letter-spacing: 0.05em !important;
+    transition: all 0.15s ease !important;
+}
+button.primary:hover {
+    background: #2ea043 !important;
+    color: #fff !important;
+    box-shadow: 0 0 10px #2ea04355 !important;
+}
+
+/* ── Secondary / example buttons ────────────────────────── */
+button.secondary, button[variant=secondary] {
+    background: #21262d !important;
+    border: 1px solid #30363d !important;
+    color: #c9d1d9 !important;
+    font-size: 0.8em !important;
+    transition: all 0.12s ease !important;
+}
+button.secondary:hover { border-color: #3fb950 !important; color: #3fb950 !important; }
+
+/* ── Code blocks ─────────────────────────────────────────── */
+code {
+    background: #161b22 !important;
+    color: #79c0ff !important;
+    border: 1px solid #30363d !important;
+    border-radius: 4px !important;
+    padding: 2px 5px !important;
+}
+pre {
+    background: #161b22 !important;
+    border: 1px solid #30363d !important;
+    border-radius: 6px !important;
+}
+pre code { color: #c9d1d9 !important; border: none !important; padding: 0 !important; }
+
+/* ── Markdown output ─────────────────────────────────────── */
+.output-markdown, .output-markdown * { color: #c9d1d9 !important; }
+.output-markdown h1, .output-markdown h2,
+.output-markdown h3 { color: #e6edf3 !important; }
+.output-markdown strong, .output-markdown b { color: #e6edf3 !important; }
+.output-markdown a { color: #58a6ff !important; }
+.output-markdown code { color: #79c0ff !important; }
+.output-markdown hr { border-color: #30363d !important; }
+
+/* ── Description italic below theorem input ──────────────── */
+.prose em, .prose i, em, i { color: #8fb8d8 !important; }
+"""
+
+try:
+    _theme = gr.themes.Base(
+        primary_hue=gr.themes.colors.green,
+        neutral_hue=gr.themes.colors.zinc,
+        font=[gr.themes.GoogleFont("JetBrains Mono"), "ui-monospace", "monospace"],
+        font_mono=[gr.themes.GoogleFont("JetBrains Mono"), "ui-monospace", "monospace"],
+    )
+except Exception:
+    _theme = None
+
+
+# ── Verdict banner — three states, dark-theme colours ────────────────────────
+
+def build_verdict_banner(success: bool, stuck: bool, english_desc: str = "") -> str:
+    font = "font-family:'JetBrains Mono','Fira Code',ui-monospace,monospace;"
+
+    if success:
+        desc_html = (
+            f'<div style="font-size:1.0em;color:#7ee787;margin:6px 0 10px;">'
+            f'<em>{english_desc}</em></div>'
+        ) if english_desc else ""
+        return (
+            f'<div style="background:#0d2818;border:2px solid #2ea043;border-radius:8px;'
+            f'padding:16px 22px;margin:10px 0;{font}">'
+            f'<div style="font-size:1.8em;font-weight:bold;color:#3fb950;letter-spacing:2px;margin-bottom:6px;">'
+            f'&#10003; FORMALLY VERIFIED</div>'
+            f'{desc_html}'
+            f'<div style="font-size:0.82em;color:#7ee787;line-height:1.75;'
+            f'border-top:1px solid #1a4a1a;padding-top:10px;margin-top:8px;">'
+            f'The AI proposed proof tactics. <strong style="color:#a0e8a0;">Lean 4\'s formal kernel</strong> '
+            f'checked every logical step against its axioms and accepted the proof.<br><br>'
+            f'<strong style="color:#3fb950;">This cannot be faked.</strong> '
+            f'Unlike a chatbot saying "yes, that\'s true," Lean\'s kernel rejects any gap in reasoning '
+            f'— no exceptions, no hallucinations. The proof below is machine-checked mathematics.'
+            f'</div></div>'
+        )
+
+    if stuck:
+        desc_html = (
+            f'<div style="font-size:1.0em;color:#e3b341;margin:6px 0 10px;">'
+            f'<em>{english_desc}</em></div>'
+        ) if english_desc else ""
+        return (
+            f'<div style="background:#1c1400;border:2px solid #d29922;border-radius:8px;'
+            f'padding:16px 22px;margin:10px 0;{font}">'
+            f'<div style="font-size:1.7em;font-weight:bold;color:#e3b341;letter-spacing:1px;margin-bottom:6px;">'
+            f'&#9888; NOT PROVABLE AS STATED</div>'
+            f'{desc_html}'
+            f'<div style="font-size:0.82em;color:#c9a227;line-height:1.75;'
+            f'border-top:1px solid #3a2800;padding-top:10px;margin-top:8px;">'
+            f'The agent detected it was stuck: the same goal state recurred with no progress.<br><br>'
+            f'<strong style="color:#e3b341;">This is a deliberate conclusion, not a failure.</strong> '
+            f'The claim as written cannot be proven — it may be mathematically false, '
+            f'or require axioms and tactics outside the current mode. '
+            f'Recognising when something is unprovable is part of what a formal proof agent does.'
+            f'</div></div>'
+        )
+
+    return (
+        f'<div style="background:#1c0a0a;border:2px solid #c62828;border-radius:8px;'
+        f'padding:16px 22px;margin:10px 0;{font}">'
+        f'<div style="font-size:1.6em;font-weight:bold;color:#f85149;margin-bottom:8px;">'
+        f'&#10007; SEARCH INCOMPLETE</div>'
+        f'<div style="font-size:0.82em;color:#c9d1d9;line-height:1.7;">'
+        f'The agent exhausted its step budget without completing the proof. '
+        f'Partial progress is shown below — try increasing the step limit or picking a simpler theorem.'
+        f'</div></div>'
+    )
+
+
+# ── SVG proof tree — DO NOT MODIFY ───────────────────────────────────────────
+
+def build_proof_tree_svg(steps: list, tactics: list, success: bool,
+                         stuck: bool = False, claim: str = "") -> str:
+    if not steps:
+        return ""
+
+    NODE_W, NODE_H = 300, 44
+    STEP_H = 140
+    SVG_W = 820
+    CX = SVG_W // 2
+
+    n = len(steps)
+    title_h = 72 if claim else 52
+    SVG_H = title_h + (n + (1 if (success or stuck) else 0)) * STEP_H + NODE_H + 20
+
+    def esc(s):
+        return str(s).replace('&', '&amp;').replace('<', '&lt;').replace('>', '&gt;').replace('"', '&quot;')
+
+    def trunc(s, maxn=36):
+        s = str(s).replace('\n', ' ').strip()
+        return s[:maxn] + '…' if len(s) > maxn else s
+
+    out = []
+    out.append(f'<svg xmlns="http://www.w3.org/2000/svg" width="{SVG_W}" height="{SVG_H}">')
+    out.append(f'<rect width="{SVG_W}" height="{SVG_H}" fill="#030c04" rx="8"/>')
+    out.append('<defs>')
+    for mid, col in [('ahg', '#00e639'), ('ahr', '#f38ba8'), ('ahgr', '#6c7086'), ('aha', '#e6a817')]:
+        out.append(
+            f'<marker id="{mid}" markerWidth="8" markerHeight="6" refX="7" refY="3" orient="auto">'
+            f'<polygon points="0 0,8 3,0 6" fill="{col}"/></marker>'
+        )
+    out.append('</defs>')
+
+    if success:
+        title, tc = "Proof Tree — ✓ Verified", "#00e639"
+    elif stuck:
+        title, tc = "Proof Tree — ⚠ Concluded: Not Provable", "#e6a817"
+    else:
+        title, tc = "Proof Tree — ✗ Incomplete", "#f38ba8"
+
+    out.append(
+        f'<text x="{CX}" y="28" text-anchor="middle" '
+        f'font-family="monospace" font-size="14" font-weight="bold" fill="{tc}">{esc(title)}</text>'
+    )
+
+    if claim:
+        out.append(
+            f'<text x="{CX}" y="47" text-anchor="middle" '
+            f'font-family="monospace" font-size="10" fill="#70b870">'
+            f'Claim: {esc(trunc(claim, 74))}</text>'
+        )
+
+    legend_y = title_h - 10
+    for lx, col, label in [(20, '#00e639', 'successful path'), (168, '#f38ba8', 'failed attempt')]:
+        out.append(f'<line x1="{lx}" y1="{legend_y}" x2="{lx+20}" y2="{legend_y}" stroke="{col}" stroke-width="2"/>')
+        out.append(
+            f'<text x="{lx+24}" y="{legend_y+4}" font-family="monospace" font-size="9" fill="{col}">{label}</text>'
+        )
+
+    for i, step in enumerate(steps):
+        cy = title_h + i * STEP_H + NODE_H // 2
+        chosen = step.get('chosen', '')
+        candidates = step.get('candidates', [])
+        status = step.get('status', '')
+        goal = step.get('goal', '')
+        failed = [c for c in candidates if c != chosen]
+
+        on_path = bool(chosen) and status != 'all_failed'
+        if on_path and success:
+            bg, border = '#001a00', '#00e639'
+        elif status == 'all_failed':
+            bg, border = '#1a0000', '#f38ba8'
+        else:
+            bg, border = '#050f05', '#2a5a2a'
+
+        nx, ny = CX - NODE_W // 2, cy - NODE_H // 2
+        out.append(
+            f'<rect x="{nx}" y="{ny}" width="{NODE_W}" height="{NODE_H}" '
+            f'rx="5" fill="{bg}" stroke="{border}" stroke-width="1.5"/>'
+        )
+        out.append(
+            f'<text x="{CX}" y="{cy+5}" text-anchor="middle" '
+            f'font-family="monospace" font-size="10" fill="#98c898">'
+            f'{esc(trunc(f"Step {i}: {goal}"))}</text>'
+        )
+
+        for j, fc in enumerate(failed):
+            bx = CX + NODE_W // 2 + 55 + j * 75
+            by = cy + STEP_H // 3
+            out.append(
+                f'<line x1="{CX+NODE_W//2}" y1="{cy}" x2="{bx}" y2="{by}" '
+                f'stroke="#f38ba8" stroke-width="1.5" stroke-dasharray="4,3" marker-end="url(#ahr)"/>'
+            )
+            mx = (CX + NODE_W // 2 + bx) // 2 + 3
+            my = (cy + by) // 2 - 3
+            out.append(
+                f'<text x="{mx}" y="{my}" font-family="monospace" font-size="8" fill="#f38ba8">'
+                f'{esc(trunc(fc, 18))}</text>'
+            )
+            out.append(f'<circle cx="{bx}" cy="{by}" r="7" fill="#1a0000" stroke="#f38ba8" stroke-width="1"/>')
+            out.append(
+                f'<text x="{bx}" y="{by+4}" text-anchor="middle" '
+                f'font-family="monospace" font-size="9" fill="#f38ba8">✗</text>'
+            )
+
+        next_cy = title_h + (i + 1) * STEP_H + NODE_H // 2
+        if on_path:
+            color, mid = ('#00e639', 'ahg') if success else ('#6c7086', 'ahgr')
+            out.append(
+                f'<line x1="{CX}" y1="{cy+NODE_H//2}" x2="{CX}" y2="{next_cy-NODE_H//2}" '
+                f'stroke="{color}" stroke-width="2" marker-end="url(#{mid})"/>'
+            )
+            ly = (cy + NODE_H // 2 + next_cy - NODE_H // 2) // 2
+            out.append(
+                f'<text x="{CX+6}" y="{ly}" font-family="monospace" font-size="9" fill="{color}">'
+                f'{esc(trunc(chosen, 28))}</text>'
+            )
+        elif status == 'all_failed':
+            out.append(
+                f'<line x1="{CX}" y1="{cy+NODE_H//2}" x2="{CX}" y2="{cy+NODE_H//2+28}" '
+                f'stroke="#f38ba8" stroke-width="1.5" stroke-dasharray="4,3"/>'
+            )
+
+    if success or stuck:
+        cy = title_h + n * STEP_H + NODE_H // 2
+        nx, ny = CX - NODE_W // 2, cy - NODE_H // 2
+        if success:
+            node_fill, node_stroke = '#002800', '#00e639'
+            node_text, node_col = '✓ QED — Goals accomplished!', '#00ff41'
+        else:
+            node_fill, node_stroke = '#201000', '#e6a817'
+            node_text, node_col = '⚠ Concluded: not provable as stated', '#f5c842'
+        out.append(
+            f'<rect x="{nx}" y="{ny}" width="{NODE_W}" height="{NODE_H}" '
+            f'rx="5" fill="{node_fill}" stroke="{node_stroke}" stroke-width="2"/>'
+        )
+        out.append(
+            f'<text x="{CX}" y="{cy+5}" text-anchor="middle" '
+            f'font-family="monospace" font-size="11" font-weight="bold" fill="{node_col}">'
+            f'{esc(node_text)}</text>'
+        )
+
+    out.append('</svg>')
+    return f'<div style="overflow-x:auto;padding:8px">{"".join(out)}</div>'
+
+
+# ── Step walkthrough ──────────────────────────────────────────────────────────
+
+def explain_tactic(tactic: str) -> str:
+    for key, explanation in TACTIC_EXPLANATIONS.items():
+        if tactic.strip().startswith(key):
+            return f"*`{key}` — {explanation}*"
+    return ""
+
+
+def make_playground_url(theorem_stmt: str, tactics: list) -> str:
+    proof_lines = [f"{theorem_stmt} := by"] + [
+        f"  {line}" for t in tactics for line in t.strip().split("\n")
+    ]
+    code = "\n".join(proof_lines)
+    return "https://live.lean-lang.org/#code=" + urllib.parse.quote(code)
+
+
+def format_steps(steps: list, tactics: list, stuck: bool = False,
+                 theorem_stmt: str = "") -> str:
+    if not steps:
+        return ""
+    out = ["### Agent loop: propose → verify → learn\n"]
+    for s in steps:
+        goal = s['goal']
+        chosen = s.get('chosen', '')
+        candidates = s.get('candidates', [])
+        status = s.get('status', '')
+        error = s.get('error', '')
+        step_num = s['step']
+
+        out.append(f"---\n**Step {step_num}** — current goal:")
+        out.append(f"```\n{goal}\n```")
+
+        if not candidates:
+            out.append("⚠️ *LLM endpoint warming up — no candidates available at this step*")
+        else:
+            rejected = [c for c in candidates if c != chosen]
+            out.append(f"\U0001f916 **LLM proposed:** `{'`, `'.join(candidates)}`")
+            for r in rejected:
+                out.append(f"- ❌ `{r}` — Lean kernel rejected")
+            if error and rejected:
+                short_err = error.replace('\n', ' ')[:120]
+                out.append(f"- \U0001f4e2 *Kernel error fed back to agent:* `{short_err}`")
+            if chosen and status != 'all_failed':
+                exp = explain_tactic(chosen)
+                out.append(f"- ✅ `{chosen}` — Lean kernel accepted")
+                if exp:
+                    out.append(f"  {exp}")
+                out.append(f"- *Result:* `{status}`")
+            elif status == 'all_failed':
+                out.append("- ❌ All candidates rejected — feeding errors back, trying next step")
+
+        out.append("")
+
+    if stuck:
+        out.append(
+            "---\n⚠️ **Search concluded** — the same goal state recurred with no progress.\n"
+            "The claim could not be proven. It may be mathematically false, "
+            "or require axioms and tactics outside the current mode."
+        )
+    elif tactics:
+        proof_lines = ["by"] + [f"  {line}" for t in tactics for line in t.strip().split("\n")]
+        proof_block = "\n".join(proof_lines)
+        out.append("---\n### Complete proof\n")
+        out.append("```lean4")
+        out.append(proof_block)
+        out.append("```")
+        out.append("\n---\n### Verify it yourself")
+        if theorem_stmt:
+            url = make_playground_url(theorem_stmt, tactics)
+            out.append(
+                f"[**▶ Open in Lean 4 web playground ↗**]({url})\n\n"
+                "The proof is pre-filled and ready to run. "
+                "The kernel outputs **\"Goals accomplished!\"** or rejects it if anything is wrong. "
+                "**It cannot be convinced. It cannot be fooled.**"
+            )
+        else:
+            out.append(
+                "Paste the proof above into [live.lean-lang.org ↗](https://live.lean-lang.org/). "
+                "The kernel outputs **\"Goals accomplished!\"** — or rejects it if anything is wrong."
+            )
+
+    return "\n".join(out)
+
+
+# ── Main proof handler ────────────────────────────────────────────────────────
+
+def prove_theorem(theorem: str, max_steps: int, use_fallbacks: bool):
+    if not theorem.strip():
+        yield "Please enter a theorem statement.", "", ""
+        return
+
+    yield "⏳ Sending to proof agent on Modal…", "", ""
+
+    lookup = EXAMPLE_LOOKUP.get(theorem.strip())
+    english_desc = lookup[0] if lookup else ""
+
+    try:
+        resp = requests.post(
+            f"{MODAL_ENDPOINT}/prove",
+            json={
+                "theorem": theorem,
+                "max_steps": max_steps,
+                "use_fallbacks": use_fallbacks,
+                "show_reasoning": True,   # always run live loop, skip cache read
+            },
+            timeout=280,
+        )
+        data = resp.json()
+    except requests.exceptions.Timeout:
+        yield "❌ Request timed out. Try a simpler theorem or fewer max steps.", "", ""
+        return
+    except Exception as e:
+        yield f"❌ Error contacting proof agent: {e}", "", ""
+        return
+
+    warmup_note = ""
+    msg = data.get("message", "")
+    if "warming up" in msg.lower() or "unavailable" in msg.lower():
+        warmup_note = "⚠️ LLM endpoint warming up (cold start) — proof attempted with fallback tactics only.\n\n"
+
+    success = data["success"]
+    stuck = data.get("stuck", False)
+
+    banner = build_verdict_banner(success, stuck, english_desc)
+    details = format_steps(
+        data["steps"], data["tactics"],
+        stuck=stuck, theorem_stmt=theorem.strip()
+    )
+    svg_html = build_proof_tree_svg(
+        data["steps"], data["tactics"], success, stuck=stuck, claim=english_desc
+    )
+    yield warmup_note + banner, details, svg_html
+
+
+# ── UI ────────────────────────────────────────────────────────────────────────
+
+_blocks_kwargs: dict = dict(title="Q.E.D", css=CUSTOM_CSS)
+if _theme is not None:
+    _blocks_kwargs["theme"] = _theme
+
+with gr.Blocks(**_blocks_kwargs) as demo:
+    gr.Markdown("""
+# ⊢ Q.E.D
+**∀ theorem → ∃ proof** — LLM-guided formal verification, powered by Modal.
+
+Enter a theorem in Lean 4 syntax (∀ ∃ ¬ ∧ ∨ → ↔ ℕ ℤ α all supported).
+The agent proposes tactics, Lean's kernel verifies each step, and kernel errors feed back into the next proposal.
+Watch it **prove** a true theorem — or **correctly conclude** a false one is unprovable.
+""")
+
+    with gr.Row():
+        with gr.Column(scale=2):
+            theorem_input = gr.Textbox(
+                label="Theorem statement",
+                placeholder="theorem my_thm : ∀ n : Nat, 0 + n = n",
+                value=EXAMPLES[0][0],
+                lines=3,
+            )
+            desc_display = gr.Markdown(
+                value=f"*{EXAMPLES[0][1]}*",
+                label="",
+            )
+            with gr.Row():
+                max_steps = gr.Slider(5, 30, value=20, step=1, label="Max steps")
+                use_fallbacks = gr.Checkbox(value=True, label="Use fallback tactics (ω, simp…)")
+            prove_btn = gr.Button("⊢ Prove", variant="primary")
+
+        with gr.Column(scale=1):
+            gr.Markdown("**Examples** — click to load\n\n*∀ provable ones first, then a false one ↓*")
+            for lean_stmt, english_desc, kind in EXAMPLES:
+                btn = gr.Button(english_desc, size="sm")
+                btn.click(
+                    fn=lambda lean=lean_stmt, d=english_desc: (lean, f"*{d}*"),
+                    outputs=[theorem_input, desc_display],
+                )
+
+    banner_out = gr.HTML(label="Verdict")
+    steps_out = gr.Markdown(label="Agent loop walkthrough")
+    tree_out = gr.HTML(label="Proof search tree")
+
+    prove_btn.click(
+        fn=prove_theorem,
+        inputs=[theorem_input, max_steps, use_fallbacks],
+        outputs=[banner_out, steps_out, tree_out],
+    )
+
+demo.queue()
+demo.launch()

requirements.txt

@@ -0,0 +1,8 @@
+gradio==6.18.0
+requests==2.34.2
+modal==1.5.0
+fastapi==0.136.3
+uvicorn==0.49.0
+lean-interact==0.11.4
+pydantic==2.13.4
+huggingface-hub==1.19.0