README.md

metadata

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, kernel-certified proofs
tags:
  - track:wood
  - sponsor:modal
  - achievement:offbrand
  - achievement:best-demo
  - gradio
  - lean4
  - formal-verification
  - agents
  - build-small-hackathon
  - llama.cpp

⊢ 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: https://huggingface.co/spaces/build-small-hackathon/QED/blob/main/Demo.mkv]

🐦 [SOCIAL POST: https://www.reddit.com/r/LocalLLaMA/comments/1u6xo0t/hf_hackathon_submission/]

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 so you can paste it into Lean's web kernel and see "Goals accomplished!" yourself.