build-small-hackathon/QED
7
1import urllib.parse2import gradio as gr3import requests4 5MODAL_ENDPOINT = "https://no-name13--lean-proof-agent-fastapi-app.modal.run"6 7# ── Example theorems ──────────────────────────────────────────────────────────8# Lead with add_comm_nat (induction / multi-step) so the agent loop is visible.9# Keep zero_add as the simple contrast. False theorem always last.10EXAMPLES = [11 (12 "theorem add_comm_nat : ∀ n m : Nat, n + m = m + n",13 "∀ n m · n + m = m + n — addition is commutative",14 "provable",15 ),16 (17 "theorem reverse_reverse : ∀ (α : Type) (l : List α), l.reverse.reverse = l",18 "∀ α l · reverse(reverse l) = l — reversing a list twice is identity",19 "provable",20 ),21 (22 "theorem zero_add : ∀ n : Nat, 0 + n = n",23 "∀ n · 0 + n = n — zero is the left identity for addition",24 "provable",25 ),26 (27 "theorem currying : ∀ P Q R : Prop, (P ∧ Q → R) ↔ (P → Q → R)",28 "∀ P Q R · (P∧Q→R) ↔ (P→Q→R) — currying",29 "provable",30 ),31 (32 "theorem de_morgan_and : ∀ P Q : Prop, ¬(P ∧ Q) ↔ ¬P ∨ ¬Q",33 "∀ P Q · ¬(P∧Q) ↔ ¬P∨¬Q — De Morgan's law",34 "provable",35 ),36 # FALSE theorem — the stuck detector concludes "not provable" within a few steps.37 (38 "theorem cannot_prove : ∀ n : Nat, n + 1 = n",39 "∀ n · n+1 = n — FALSE: the agent correctly cannot prove this ✗",40 "unprovable",41 ),42]43 44EXAMPLE_LOOKUP = {lean.strip(): (desc, kind) for lean, desc, kind in EXAMPLES}45 46TACTIC_EXPLANATIONS = {47 "intro": "introduces a universally quantified variable or hypothesis into the local context",48 "induction": "applies structural induction — splits into base case (zero) and inductive step (succ)",49 "simp": "simplifies the goal using a library of known equalities and lemmas",50 "rfl": "closes the goal when both sides are definitionally equal",51 "omega": "decision procedure for linear arithmetic — automatically solves goals about integers/naturals",52 "rw": "rewrites the goal using an equation",53 "exact": "closes the goal by providing an exact proof term",54 "apply": "applies a lemma whose conclusion matches the goal",55 "constructor": "splits a conjunction (∧) or iff (↔) goal into its two parts",56 "cases": "case-splits on a hypothesis or value",57 "norm_num": "solves numeric goals like 2 + 2 = 4 or 3 ∣ 6",58 "contradiction": "closes the goal when context contains P and ¬P (a direct contradiction)",59 "assumption": "closes the goal when it matches a hypothesis in the local context exactly",60 "tauto": "closes propositional tautologies automatically",61}62 63# ── Dark theme — mathematical / formal-proof terminal aesthetic ───────────────64# Wraps in try/except so a theme API mismatch never breaks the app.65CUSTOM_CSS = """66/* ── Base ───────────────────────────────────────────────── */67body, .gradio-container { background: #0d1117 !important; color: #c9d1d9 !important; }68.contain, .gap, .row { background: #0d1117 !important; }69 70/* ── Panels ─────────────────────────────────────────────── */71.block.padded, .block {72 background: #161b22 !important;73 border: 1px solid #30363d !important;74 border-radius: 8px !important;75}76.form { background: #161b22 !important; }77 78/* ── All text — catch-all first, then specifics ──────────── */79* { color: #c9d1d9; }80 81/* ── Headings ────────────────────────────────────────────── */82h1, h2, h3, h4 { color: #e6edf3 !important; }83h1 { border-bottom: 1px solid #21262d; padding-bottom: 6px; }84 85/* ── Labels (component titles, slider/checkbox labels) ────── */86label, .label-wrap, .label-wrap span,87span.text-gray-500, span.text-sm,88.block > .label-wrap > span { color: #b0bec5 !important; }89 90/* ── Body text, lists, paragraphs ───────────────────────── */91p, li, em, span { color: #c9d1d9 !important; }92a { color: #58a6ff !important; }93strong, b { color: #e6edf3 !important; }94 95/* ── Slider ──────────────────────────────────────────────── */96input[type=range] { accent-color: #2ea043 !important; }97.range-input span, .range-input output,98input[type=range] + span, .slider-container span { color: #c9d1d9 !important; }99 100/* ── Checkbox ────────────────────────────────────────────── */101input[type=checkbox] { accent-color: #2ea043 !important; }102.checkbox-label, .checkbox-label span { color: #c9d1d9 !important; }103 104/* ── Inputs ──────────────────────────────────────────────── */105textarea, input[type=text], input[type=number] {106 background: #0d1117 !important;107 color: #e6edf3 !important;108 border: 1px solid #30363d !important;109 border-radius: 6px !important;110 font-family: 'JetBrains Mono', 'Fira Code', ui-monospace, monospace !important;111}112textarea::placeholder { color: #484f58 !important; }113 114/* ── Primary button ──────────────────────────────────────── */115button.primary {116 background: #1a3a1a !important;117 border: 1px solid #2ea043 !important;118 color: #3fb950 !important;119 font-weight: bold !important;120 letter-spacing: 0.05em !important;121 transition: all 0.15s ease !important;122}123button.primary:hover {124 background: #2ea043 !important;125 color: #fff !important;126 box-shadow: 0 0 10px #2ea04355 !important;127}128 129/* ── Secondary / example buttons ────────────────────────── */130button.secondary, button[variant=secondary] {131 background: #21262d !important;132 border: 1px solid #30363d !important;133 color: #c9d1d9 !important;134 font-size: 0.8em !important;135 transition: all 0.12s ease !important;136}137button.secondary:hover { border-color: #3fb950 !important; color: #3fb950 !important; }138 139/* ── Code blocks ─────────────────────────────────────────── */140code {141 background: #161b22 !important;142 color: #79c0ff !important;143 border: 1px solid #30363d !important;144 border-radius: 4px !important;145 padding: 2px 5px !important;146}147pre {148 background: #161b22 !important;149 border: 1px solid #30363d !important;150 border-radius: 6px !important;151}152pre code { color: #c9d1d9 !important; border: none !important; padding: 0 !important; }153 154/* ── Markdown output ─────────────────────────────────────── */155.output-markdown, .output-markdown * { color: #c9d1d9 !important; }156.output-markdown h1, .output-markdown h2,157.output-markdown h3 { color: #e6edf3 !important; }158.output-markdown strong, .output-markdown b { color: #e6edf3 !important; }159.output-markdown a { color: #58a6ff !important; }160.output-markdown code { color: #79c0ff !important; }161.output-markdown hr { border-color: #30363d !important; }162 163/* ── Description italic below theorem input ──────────────── */164.prose em, .prose i, em, i { color: #8fb8d8 !important; }165"""166 167try:168 _theme = gr.themes.Base(169 primary_hue=gr.themes.colors.green,170 neutral_hue=gr.themes.colors.zinc,171 font=[gr.themes.GoogleFont("JetBrains Mono"), "ui-monospace", "monospace"],172 font_mono=[gr.themes.GoogleFont("JetBrains Mono"), "ui-monospace", "monospace"],173 )174except Exception:175 _theme = None176 177 178# ── Verdict banner — three states, dark-theme colours ────────────────────────179 180def build_verdict_banner(success: bool, stuck: bool, english_desc: str = "") -> str:181 font = "font-family:'JetBrains Mono','Fira Code',ui-monospace,monospace;"182 183 if success:184 desc_html = (185 f'<div style="font-size:1.0em;color:#7ee787;margin:6px 0 10px;">'186 f'<em>{english_desc}</em></div>'187 ) if english_desc else ""188 return (189 f'<div style="background:#0d2818;border:2px solid #2ea043;border-radius:8px;'190 f'padding:16px 22px;margin:10px 0;{font}">'191 f'<div style="font-size:1.8em;font-weight:bold;color:#3fb950;letter-spacing:2px;margin-bottom:6px;">'192 f'✓ FORMALLY VERIFIED</div>'193 f'{desc_html}'194 f'<div style="font-size:0.82em;color:#7ee787;line-height:1.75;'195 f'border-top:1px solid #1a4a1a;padding-top:10px;margin-top:8px;">'196 f'The AI proposed proof tactics. <strong style="color:#a0e8a0;">Lean 4\'s formal kernel</strong> '197 f'checked every logical step against its axioms and accepted the proof.<br><br>'198 f'<strong style="color:#3fb950;">This cannot be faked.</strong> '199 f'Unlike a chatbot saying "yes, that\'s true," Lean\'s kernel rejects any gap in reasoning '200 f'— no exceptions, no hallucinations. The proof below is machine-checked mathematics.'201 f'</div></div>'202 )203 204 if stuck:205 desc_html = (206 f'<div style="font-size:1.0em;color:#e3b341;margin:6px 0 10px;">'207 f'<em>{english_desc}</em></div>'208 ) if english_desc else ""209 return (210 f'<div style="background:#1c1400;border:2px solid #d29922;border-radius:8px;'211 f'padding:16px 22px;margin:10px 0;{font}">'212 f'<div style="font-size:1.7em;font-weight:bold;color:#e3b341;letter-spacing:1px;margin-bottom:6px;">'213 f'⚠ NOT PROVABLE AS STATED</div>'214 f'{desc_html}'215 f'<div style="font-size:0.82em;color:#c9a227;line-height:1.75;'216 f'border-top:1px solid #3a2800;padding-top:10px;margin-top:8px;">'217 f'The agent detected it was stuck: the same goal state recurred with no progress.<br><br>'218 f'<strong style="color:#e3b341;">This is a deliberate conclusion, not a failure.</strong> '219 f'The claim as written cannot be proven — it may be mathematically false, '220 f'or require axioms and tactics outside the current mode. '221 f'Recognising when something is unprovable is part of what a formal proof agent does.'222 f'</div></div>'223 )224 225 return (226 f'<div style="background:#1c0a0a;border:2px solid #c62828;border-radius:8px;'227 f'padding:16px 22px;margin:10px 0;{font}">'228 f'<div style="font-size:1.6em;font-weight:bold;color:#f85149;margin-bottom:8px;">'229 f'✗ SEARCH INCOMPLETE</div>'230 f'<div style="font-size:0.82em;color:#c9d1d9;line-height:1.7;">'231 f'The agent exhausted its step budget without completing the proof. '232 f'Partial progress is shown below — try increasing the step limit or picking a simpler theorem.'233 f'</div></div>'234 )235 236 237# ── SVG proof tree — DO NOT MODIFY ───────────────────────────────────────────238 239def build_proof_tree_svg(steps: list, tactics: list, success: bool,240 stuck: bool = False, claim: str = "") -> str:241 if not steps:242 return ""243 244 NODE_W, NODE_H = 300, 44245 STEP_H = 140246 SVG_W = 820247 CX = SVG_W // 2248 249 n = len(steps)250 title_h = 72 if claim else 52251 SVG_H = title_h + (n + (1 if (success or stuck) else 0)) * STEP_H + NODE_H + 20252 253 def esc(s):254 return str(s).replace('&', '&').replace('<', '<').replace('>', '>').replace('"', '"')255 256 def trunc(s, maxn=36):257 s = str(s).replace('\n', ' ').strip()258 return s[:maxn] + '…' if len(s) > maxn else s259 260 out = []261 out.append(f'<svg xmlns="http://www.w3.org/2000/svg" width="{SVG_W}" height="{SVG_H}">')262 out.append(f'<rect width="{SVG_W}" height="{SVG_H}" fill="#030c04" rx="8"/>')263 out.append('<defs>')264 for mid, col in [('ahg', '#00e639'), ('ahr', '#f38ba8'), ('ahgr', '#6c7086'), ('aha', '#e6a817')]:265 out.append(266 f'<marker id="{mid}" markerWidth="8" markerHeight="6" refX="7" refY="3" orient="auto">'267 f'<polygon points="0 0,8 3,0 6" fill="{col}"/></marker>'268 )269 out.append('</defs>')270 271 if success:272 title, tc = "Proof Tree — ✓ Verified", "#00e639"273 elif stuck:274 title, tc = "Proof Tree — ⚠ Concluded: Not Provable", "#e6a817"275 else:276 title, tc = "Proof Tree — ✗ Incomplete", "#f38ba8"277 278 out.append(279 f'<text x="{CX}" y="28" text-anchor="middle" '280 f'font-family="monospace" font-size="14" font-weight="bold" fill="{tc}">{esc(title)}</text>'281 )282 283 if claim:284 out.append(285 f'<text x="{CX}" y="47" text-anchor="middle" '286 f'font-family="monospace" font-size="10" fill="#70b870">'287 f'Claim: {esc(trunc(claim, 74))}</text>'288 )289 290 legend_y = title_h - 10291 for lx, col, label in [(20, '#00e639', 'successful path'), (168, '#f38ba8', 'failed attempt')]:292 out.append(f'<line x1="{lx}" y1="{legend_y}" x2="{lx+20}" y2="{legend_y}" stroke="{col}" stroke-width="2"/>')293 out.append(294 f'<text x="{lx+24}" y="{legend_y+4}" font-family="monospace" font-size="9" fill="{col}">{label}</text>'295 )296 297 for i, step in enumerate(steps):298 cy = title_h + i * STEP_H + NODE_H // 2299 chosen = step.get('chosen', '')300 candidates = step.get('candidates', [])301 status = step.get('status', '')302 goal = step.get('goal', '')303 failed = [c for c in candidates if c != chosen]304 305 on_path = bool(chosen) and status != 'all_failed'306 if on_path and success:307 bg, border = '#001a00', '#00e639'308 elif status == 'all_failed':309 bg, border = '#1a0000', '#f38ba8'310 else:311 bg, border = '#050f05', '#2a5a2a'312 313 nx, ny = CX - NODE_W // 2, cy - NODE_H // 2314 out.append(315 f'<rect x="{nx}" y="{ny}" width="{NODE_W}" height="{NODE_H}" '316 f'rx="5" fill="{bg}" stroke="{border}" stroke-width="1.5"/>'317 )318 out.append(319 f'<text x="{CX}" y="{cy+5}" text-anchor="middle" '320 f'font-family="monospace" font-size="10" fill="#98c898">'321 f'{esc(trunc(f"Step {i}: {goal}"))}</text>'322 )323 324 for j, fc in enumerate(failed):325 bx = CX + NODE_W // 2 + 55 + j * 75326 by = cy + STEP_H // 3327 out.append(328 f'<line x1="{CX+NODE_W//2}" y1="{cy}" x2="{bx}" y2="{by}" '329 f'stroke="#f38ba8" stroke-width="1.5" stroke-dasharray="4,3" marker-end="url(#ahr)"/>'330 )331 mx = (CX + NODE_W // 2 + bx) // 2 + 3332 my = (cy + by) // 2 - 3333 out.append(334 f'<text x="{mx}" y="{my}" font-family="monospace" font-size="8" fill="#f38ba8">'335 f'{esc(trunc(fc, 18))}</text>'336 )337 out.append(f'<circle cx="{bx}" cy="{by}" r="7" fill="#1a0000" stroke="#f38ba8" stroke-width="1"/>')338 out.append(339 f'<text x="{bx}" y="{by+4}" text-anchor="middle" '340 f'font-family="monospace" font-size="9" fill="#f38ba8">✗</text>'341 )342 343 next_cy = title_h + (i + 1) * STEP_H + NODE_H // 2344 if on_path:345 color, mid = ('#00e639', 'ahg') if success else ('#6c7086', 'ahgr')346 out.append(347 f'<line x1="{CX}" y1="{cy+NODE_H//2}" x2="{CX}" y2="{next_cy-NODE_H//2}" '348 f'stroke="{color}" stroke-width="2" marker-end="url(#{mid})"/>'349 )350 ly = (cy + NODE_H // 2 + next_cy - NODE_H // 2) // 2351 out.append(352 f'<text x="{CX+6}" y="{ly}" font-family="monospace" font-size="9" fill="{color}">'353 f'{esc(trunc(chosen, 28))}</text>'354 )355 elif status == 'all_failed':356 out.append(357 f'<line x1="{CX}" y1="{cy+NODE_H//2}" x2="{CX}" y2="{cy+NODE_H//2+28}" '358 f'stroke="#f38ba8" stroke-width="1.5" stroke-dasharray="4,3"/>'359 )360 361 if success or stuck:362 cy = title_h + n * STEP_H + NODE_H // 2363 nx, ny = CX - NODE_W // 2, cy - NODE_H // 2364 if success:365 node_fill, node_stroke = '#002800', '#00e639'366 node_text, node_col = '✓ QED — Goals accomplished!', '#00ff41'367 else:368 node_fill, node_stroke = '#201000', '#e6a817'369 node_text, node_col = '⚠ Concluded: not provable as stated', '#f5c842'370 out.append(371 f'<rect x="{nx}" y="{ny}" width="{NODE_W}" height="{NODE_H}" '372 f'rx="5" fill="{node_fill}" stroke="{node_stroke}" stroke-width="2"/>'373 )374 out.append(375 f'<text x="{CX}" y="{cy+5}" text-anchor="middle" '376 f'font-family="monospace" font-size="11" font-weight="bold" fill="{node_col}">'377 f'{esc(node_text)}</text>'378 )379 380 out.append('</svg>')381 return f'<div style="overflow-x:auto;padding:8px">{"".join(out)}</div>'382 383 384# ── Step walkthrough ──────────────────────────────────────────────────────────385 386def explain_tactic(tactic: str) -> str:387 for key, explanation in TACTIC_EXPLANATIONS.items():388 if tactic.strip().startswith(key):389 return f"*`{key}` — {explanation}*"390 return ""391 392 393def make_playground_url(theorem_stmt: str, tactics: list) -> str:394 proof_lines = [f"{theorem_stmt} := by"] + [395 f" {line}" for t in tactics for line in t.strip().split("\n")396 ]397 code = "\n".join(proof_lines)398 return "https://live.lean-lang.org/#code=" + urllib.parse.quote(code)399 400 401def format_steps(steps: list, tactics: list, stuck: bool = False,402 theorem_stmt: str = "") -> str:403 if not steps:404 return ""405 out = ["### Agent loop: propose → verify → learn\n"]406 for s in steps:407 goal = s['goal']408 chosen = s.get('chosen', '')409 candidates = s.get('candidates', [])410 status = s.get('status', '')411 error = s.get('error', '')412 step_num = s['step']413 414 out.append(f"---\n**Step {step_num}** — current goal:")415 out.append(f"```\n{goal}\n```")416 417 if not candidates:418 out.append("⚠️ *LLM endpoint warming up — no candidates available at this step*")419 else:420 rejected = [c for c in candidates if c != chosen]421 out.append(f"\U0001f916 **LLM proposed:** `{'`, `'.join(candidates)}`")422 for r in rejected:423 out.append(f"- ❌ `{r}` — Lean kernel rejected")424 if error and rejected:425 short_err = error.replace('\n', ' ')[:120]426 out.append(f"- \U0001f4e2 *Kernel error fed back to agent:* `{short_err}`")427 if chosen and status != 'all_failed':428 exp = explain_tactic(chosen)429 out.append(f"- ✅ `{chosen}` — Lean kernel accepted")430 if exp:431 out.append(f" {exp}")432 out.append(f"- *Result:* `{status}`")433 elif status == 'all_failed':434 out.append("- ❌ All candidates rejected — feeding errors back, trying next step")435 436 out.append("")437 438 if stuck:439 out.append(440 "---\n⚠️ **Search concluded** — the same goal state recurred with no progress.\n"441 "The claim could not be proven. It may be mathematically false, "442 "or require axioms and tactics outside the current mode."443 )444 elif tactics:445 proof_lines = ["by"] + [f" {line}" for t in tactics for line in t.strip().split("\n")]446 proof_block = "\n".join(proof_lines)447 out.append("---\n### Complete proof\n")448 out.append("```lean4")449 out.append(proof_block)450 out.append("```")451 out.append("\n---\n### Verify it yourself")452 if theorem_stmt:453 url = make_playground_url(theorem_stmt, tactics)454 out.append(455 f"[**▶ Open in Lean 4 web playground ↗**]({url})\n\n"456 "The proof is pre-filled and ready to run. "457 "The kernel outputs **\"Goals accomplished!\"** or rejects it if anything is wrong. "458 "**It cannot be convinced. It cannot be fooled.**"459 )460 else:461 out.append(462 "Paste the proof above into [live.lean-lang.org ↗](https://live.lean-lang.org/). "463 "The kernel outputs **\"Goals accomplished!\"** — or rejects it if anything is wrong."464 )465 466 return "\n".join(out)467 468 469# ── Main proof handler ────────────────────────────────────────────────────────470 471def prove_theorem(theorem: str, max_steps: int, use_fallbacks: bool):472 if not theorem.strip():473 yield "Please enter a theorem statement.", "", ""474 return475 476 yield "⏳ Sending to proof agent on Modal…", "", ""477 478 lookup = EXAMPLE_LOOKUP.get(theorem.strip())479 english_desc = lookup[0] if lookup else ""480 481 try:482 resp = requests.post(483 f"{MODAL_ENDPOINT}/prove",484 json={485 "theorem": theorem,486 "max_steps": max_steps,487 "use_fallbacks": use_fallbacks,488 "show_reasoning": True, # always run live loop, skip cache read489 },490 timeout=280,491 )492 data = resp.json()493 except requests.exceptions.Timeout:494 yield "❌ Request timed out. Try a simpler theorem or fewer max steps.", "", ""495 return496 except Exception as e:497 yield f"❌ Error contacting proof agent: {e}", "", ""498 return499 500 warmup_note = ""501 msg = data.get("message", "")502 if "warming up" in msg.lower() or "unavailable" in msg.lower():503 warmup_note = "⚠️ LLM endpoint warming up (cold start) — proof attempted with fallback tactics only.\n\n"504 505 success = data["success"]506 stuck = data.get("stuck", False)507 508 banner = build_verdict_banner(success, stuck, english_desc)509 details = format_steps(510 data["steps"], data["tactics"],511 stuck=stuck, theorem_stmt=theorem.strip()512 )513 svg_html = build_proof_tree_svg(514 data["steps"], data["tactics"], success, stuck=stuck, claim=english_desc515 )516 yield warmup_note + banner, details, svg_html517 518 519# ── UI ────────────────────────────────────────────────────────────────────────520 521_blocks_kwargs: dict = dict(title="Q.E.D", css=CUSTOM_CSS)522if _theme is not None:523 _blocks_kwargs["theme"] = _theme524 525with gr.Blocks(**_blocks_kwargs) as demo:526 gr.Markdown("""527# ⊢ Q.E.D528**∀ theorem → ∃ proof** — LLM-guided formal verification, powered by Modal.529 530Enter a theorem in Lean 4 syntax (∀ ∃ ¬ ∧ ∨ → ↔ ℕ ℤ α all supported).531The agent proposes tactics, Lean's kernel verifies each step, and kernel errors feed back into the next proposal.532Watch it **prove** a true theorem — or **correctly conclude** a false one is unprovable.533""")534 535 with gr.Row():536 with gr.Column(scale=2):537 theorem_input = gr.Textbox(538 label="Theorem statement",539 placeholder="theorem my_thm : ∀ n : Nat, 0 + n = n",540 value=EXAMPLES[0][0],541 lines=3,542 )543 desc_display = gr.Markdown(544 value=f"*{EXAMPLES[0][1]}*",545 label="",546 )547 with gr.Row():548 max_steps = gr.Slider(5, 30, value=20, step=1, label="Max steps")549 use_fallbacks = gr.Checkbox(value=True, label="Use fallback tactics (ω, simp…)")550 prove_btn = gr.Button("⊢ Prove", variant="primary")551 552 with gr.Column(scale=1):553 gr.Markdown("**Examples** — click to load\n\n*∀ provable ones first, then a false one ↓*")554 for lean_stmt, english_desc, kind in EXAMPLES:555 btn = gr.Button(english_desc, size="sm")556 btn.click(557 fn=lambda lean=lean_stmt, d=english_desc: (lean, f"*{d}*"),558 outputs=[theorem_input, desc_display],559 )560 561 banner_out = gr.HTML(label="Verdict")562 steps_out = gr.Markdown(label="Agent loop walkthrough")563 tree_out = gr.HTML(label="Proof search tree")564 565 prove_btn.click(566 fn=prove_theorem,567 inputs=[theorem_input, max_steps, use_fallbacks],568 outputs=[banner_out, steps_out, tree_out],569 )570 571demo.queue()572demo.launch()573