Summary

MathCode is a terminal AI assistant designed to bridge natural language mathematical problems with formal theorem proving. It automatically converts plain-language math statements into Lean 4 theorems and attempts to generate formal proofs, targeting researchers and developers who need to formalize mathematical concepts or verify proofs.

How It Works

The system leverages the AUTOLEAN project's formalization pipeline. Users input mathematical problems in natural language, which MathCode translates into Lean 4 code. It then employs an AI agent to iteratively construct formal proofs, utilizing tools like Loogle for lemma discovery and structured LSP diagnostics for error feedback. Proof sessions can be interactive, with the agent reading compile errors and attempting fixes. The project also generates an Obsidian knowledge graph to visualize theorem dependencies.

Quick Start & Requirements

Installation involves cloning the repository (git clone https://github.com/math-ai-org/mathcode.git), navigating into the directory, and running bash setup.sh. This script downloads the appropriate MathCode binary from GitHub Releases, sets up the environment, and bootstraps Lean. Subsequent use requires codex auth login and running ./run. Prerequisites include macOS (arm64) or Linux (x86_64), Python 3.12+, sufficient disk space for the bundle and caches, and the codex CLI for the default backend.

Highlighted Details

• Lean LSP Integration: Enhances lemma discovery and provides structured error feedback during proving. Initial Mathlib loading takes approximately 60 seconds.
• Obsidian Theorem Graph: Automatically generates an Obsidian vault visualizing theorem dependencies, aiding knowledge management and exploration.
• Agent-Mode Proving: Enables interactive, iterative proof sessions where the AI agent uses tools, reads compiler errors, and attempts repairs.
• Multi-Planner: Allows running multiple proof strategy planners in parallel to explore diverse proof approaches.

Maintenance & Community

The provided README does not detail specific contributors, sponsorships, or community channels (e.g., Discord, Slack).

Licensing & Compatibility

The repository's license is not explicitly stated in the README. This absence requires further investigation for commercial use or integration into closed-source projects.

Limitations & Caveats

The project is currently limited to macOS (arm64) and Linux (x86_64) platforms. Users may encounter startup errors if the incorrect binary is downloaded for their platform. The default backend relies on the codex CLI, and initial LSP operations have a notable startup latency.