MathCode, Mathematical Coding Agent

MathCode is a terminal AI coding assistant that converts plain language math problems into Lean 4 theorems and automatically attempts formal proofs using a persistent Lean REPL, reusable theorem libraries, and agentic proving capabilities. It features a persistent Lean language server for faster compilation (~0.4s), an Obsidian knowledge graph for visualizing theorem dependencies, and multi-planner agent-mode proving that decomposes complex theorems into subgoals. The tool is available for macOS (arm64) and Linux (x86_64) and can be tested with commands like `mathcode -p "prove that the square of an even number is even"`.