- Published on
MathCode, Mathematical Coding Agent
- Authors
- Name
- DeepHorus
MathCode, a new terminal-based artificial intelligence coding assistant with a built-in mathematical formalization engine, has been released by Team Math-AI on GitHub. The tool accepts math problems in plain language, converts them into Lean 4 theorems, and automatically attempts formal proofs. It is designed for researchers and developers working with proof assistants.
The release comes amid growing interest in using AI to streamline formal mathematics. Formalization, the process of converting informal proofs into machine-checkable ones, remains labor-intensive. Lean 4 has gained traction as a proof assistant, but it requires significant expertise and time.
MathCode's key innovation is a persistent Lean language server that reduces compile checks to roughly 0.4 seconds after a one-time warmup, compared with about 30 seconds in typical setups. Every proved theorem is auto-named, stored, and made importable for reuse by both the prover and planner. Conversational assumptions can also be stored as persistent, compile-checked declarations.
The assistant searches Leansearch.net and Loogle for verified Mathlib lemmas, using structured LSP diagnostics to guide repairs. It decomposes complex theorems into independent subgoals that can be proven in parallel before being stitched together. Multiple planners run concurrently to explore diverse proof strategies, with the prover selecting the best approach.
Another distinctive feature is the generation of an Obsidian vault, which visualizes theorem-to-lemma dependencies as an interactive knowledge graph. This helps users understand the logical structure and dependencies of their proofs. Each proof session becomes an interactive process where the agent writes candidates, reads errors, and recompiles.
The project's implications are significant for the future of mathematical verification. By reducing proof-checking latency and enabling parallel proving, MathCode could make formalization feasible for larger research projects. Its open-source nature allows community contributions and adaptation.
Team Math-AI has requested citation for academic use, noting that the pipeline is based on the AUTOLEAN project. While no external reactions are yet available, the project aligns with broader efforts to integrate AI with formal reasoning. It is expected to attract attention from mathematicians and computer scientists.
MathCode currently supports macOS arm64 and Linux x86_64, with the codex CLI as the default backend. Interested users can install it via a setup script, and a browser UI is available for convenience. As the tool evolves, it may become a standard part of the formal mathematics toolkit, accelerating research and proof development.
