AgentQED
AgentQED is an AI agent that verifies mathematical proofs.
Core trick
Gemini translates a typed, spoken, or photographed proof into Lean 4, then the Lean compiler checks it in a sandbox and feeds errors back for self-correction.
Description
AgentQED is an AI agent that verifies mathematical proofs. You give it a proof — typed, spoken, or handwritten on paper — and it tells you whether your proof is actually correct by running it through a real theorem prover.
README excerpt
# AgentQED — AI-Powered Mathematical Proof Verification
> Write a proof in plain English, speak it aloud, or photograph handwritten math. AgentQED translates it to Lean 4 and formally verifies it using the Lean compiler in an isolated sandbox.
**Live:** [proof-agent.vercel.app](https://proof-agent.vercel.app)
**Repo:** [github.com/gsankar967/AgentQED](https://github.com/gsankar967/AgentQED)
Built at the [Zero to Agent Hackathon](https://cerebralvalley.ai) (Vercel x Deepmind) — March 21, 2026, Shack15, SF.
---
## What It Does
AgentQED is a self-correcting AI agent that bridges informal mathematical reasoning and formal verification:
1. **You describe a proof** — type it, speak it, photograph handwritten math, or upload a PDF
2. **Gemini 3.1 Pro** reads your input, translates it into Lean 4 code
3. **Vercel Sandbox** spins up an isolated Firecracker microVM, installs Lean 4, and compiles the proof
4. **If verification fails**, the agent reads the compiler errors, fixes the code, and retries (up to 12 attempts)
5. **Once verified**, you get a structured result: Key Insight first, Proof Structure tree, then collapsible details
```
User: "Prove that for all natural numbers n, 0 + n = n"
|
v
Gemini 3.1 Pro translates to Lean 4:
theorem zero_add (n : Nat) : 0 + n = n := by
induction n with
| zero => rfl
| succ n ih => simp [Nat.add_succ, ih]
|
v
Vercel Sandbox runs `lean Proof.lean`
|
v
Proof verified by Lean 4 compiler
```
---
## Features
| Feat