Theorem Proving Agent
Connect natural-language reasoning with machine-checked Lean proofs — with Infoview feedback, Mathlib navigation, MCP-powered completion, and readable explanations.
Demo Video
Highlights
- Write problems in Markdown; obtain natural-language proofs written back to the file.
- Formalize statements and proofs in Lean with online compilation and live Infoview.
- Hover info, Go to Definition into Mathlib, and natural-language theorem search.
- Agent reads compiler feedback to continue modifying and completing proofs.
- Select Lean snippets and ask for natural-language explanations in TeX or Markdown.