The Math-AI team has released version 0.2.0 of MathCode, an AI agent for formal mathematics and theorem proving. The big news? It uses prefix cache request reshaping and policy controls to slash API costs by up to 90%.
In theorem proving, models frequently need to read massive code bases and axiom libraries. MathCode 0.2.0 introduces a mechanism called prefix-cache request-shape diagnostics and policy controls. The system masks prompt header attribution to ensure structural stability, and adds multi-breakpoint caching (MATHCODE_CACHE_MULTI_BREAKPOINT), an explicit minimum prefix gateway, and idle-aware TTL strategies. By aligning underlying request shapes, it maximizes provider native cache hit rates, cutting long-session bills to one-tenth of their original cost.
The new version also tightens task management and thinking depth control. To prevent overspending on long-running tasks, you can now set a token budget cap via MATHCODE_GOAL_MAX_TOKEN_BUDGET. It also limits nested slash commands to avoid infinite loops. Proof sessions support dynamic thinking depth adjustment with --effort or /effort, offering low, medium, high, and max levels, and you can revert to default settings at any time.
On the compilation and deployment front, MathCode 0.2.0 supports an external compiler — Kimina Lean Server, developed by Project Numina — running as a persistent subprocess, routing compilation check requests to the /verify endpoint. The setup.sh installation script has been refactored, adding --status and --clean commands, along with release checksum auto-verification and reuse of the system's Lean/Lake environment, lowering the deployment barrier.