build-small-hackathon/QED

1---2title: Q.E.D3emoji: 🔬4colorFrom: green5colorTo: gray6sdk: gradio7app_file: front.py8pinned: true9license: mit10short_description: LLM-guided formal verification, kernel-certified proofs11tags:12  - track:wood13  - sponsor:modal14  - achievement:offbrand15  - achievement:best-demo16  - gradio17  - lean418  - formal-verification19  - agents20  - build-small-hackathon21  - llama.cpp22---23 24# ⊢ Q.E.D25 26An 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**.27 28Unlike 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.29 30## Demo31 32📹 **[DEMO VIDEO: https://huggingface.co/spaces/build-small-hackathon/QED/blob/main/Demo.mkv]**33 34🐦 **[SOCIAL POST: https://www.reddit.com/r/LocalLLaMA/comments/1u6xo0t/hf_hackathon_submission/]**35 36## What it does37 38The 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:39 40```41theorem42  → propose 3 tactic candidates (27B LLM via Modal)43  → verify each in live Lean 4 REPL (Modal container)44  → kernel rejects? → error text fed back to LLM45  → kernel accepts? → advance proof state46  → repeat until complete or stuck47```48 49Key behaviours:50 51- **Fallback layer** — deterministic tactics (`rfl`, `norm_num`, `simp`, `omega`, `contradiction`, `assumption`) are tried at each step before the LLM is called.52- **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.53- **No cache on demo runs** — every run executes the full live loop so the propose→verify→learn steps are always visible.54 55**Model**: one model, Qwen3-27B quantized (Q4_K_M GGUF) served via llama.cpp. 27B < 32B. ✓56 57## Best Use of Modal58 59Two Modal deployments power the app:60 61| App | What it runs |62|---|---|63| `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. |64| `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. |65 66Why Modal specifically:67 68- 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.69- `min_containers=1` means the Lean server is **always alive**, which is critical for a live demo with ~30-second proof runs.70- The LLM needs a GPU. Modal's on-demand GPU allocation means no dedicated hardware to maintain.71- The two apps are **independently scaled**: REPL is CPU-bound, LLM is GPU-bound.72 73## Off Brand — custom UI74 75The 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.76 77The 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.78 79## Best Agent — agent loop design80 81The proof search is a genuine multi-step agentic loop with external tool use and error-driven self-correction:82 83- **Propose**: LLM generates 3 tactic candidates given the current proof state and the previous kernel error (if any)84- **Verify**: Lean's formal kernel checks each candidate — this is ground truth, not a heuristic85- **Learn**: the exact kernel error message is injected back into the next LLM prompt86- **Decide**: best partial-progress result is selected; all-failed steps increment a failure counter87- **Conclude**: stuck-state detector fires a deliberate "not provable" verdict rather than hitting the step limit88 89The agent correctly proves true theorems and correctly identifies false ones — both happen live on every run.90 91## Try it92 93Load 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.94 95Each 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.96