Download
MathCode is a terminal-based AI coding assistant focused on mathematical formalization and theorem proving. It is designed to transform plain-language mathematical reasoning into verified Lean 4 code and formal proofs. The project combines AI agents with Lean Language Server Protocol integration, allowing it to inspect compiler feedback, search for lemmas, and iteratively repair failed proof attempts. It supports an agentic proving workflow where the system behaves more like an interactive mathematical engineer than a one-shot text generator. MathCode also includes visualization-oriented tooling such as theorem graph generation for Obsidian knowledge workflows. Its main value is bridging natural-language mathematics with formal verification systems in a way that is more automated, inspectable, and iterative than traditional theorem-proving pipelines.
Features
- Plain-language to Lean 4 formalization workflow
- Lean LSP integration for structured proof feedback
- Agentic iterative theorem proving mode
- Automatic theorem graph generation for Obsidian
- Parallel planner architecture for proof exploration
- Terminal-based AI coding assistant interface
Project Samples
