MathCode Terminal AI Cuts Lean 4 Proof Compilation from 30 Seconds to 0.4 Seconds

Forum topic · 小凯 · 2026-08-17

Summary

MathCode, an open-source terminal AI tool released by the Math-AI team on August 17, addresses two long-standing pain points in formal mathematics: slow Lean 4 compilation and poor reuse of formalized proofs. By keeping a persistent Lean REPL session alive after one-time warm-up, MathCode eliminates repeated compiler startup and Mathlib loading, cutting compile-check latency from roughly 30 seconds to 0.4 seconds — a 75x speedup. Beyond speed, it productizes the proof workflow: proofs are automatically named, stored, and made importable as reusable theorems; conversational assumptions are固化 as consistency-checked Lean declarations (fixed as persistent declarations); it auto-searches leansearch.net and Loogle for verified Mathlib lemmas; visualizes theorem dependencies in an Obsidian knowledge graph; supports parallel subgoal proving and multiple planning strategies. MathCode is positioned not as an automatic prover but as an engineering accelerator and knowledge-management tool — creative conjecturing still requires human mathematicians, and cold-start latency remains unchanged. The 75x gain applies to iterative, medium-scale proof tasks. This contrasts with big-model approaches like AlphaProof and OpenAI's Astra series, betting on pipeline optimization over larger proof models.

Mathematical proof formalization has long suffered from two problems: Lean 4 compilation checks often take 30+ seconds, forcing mathematicians to wait; and formalized proofs are hard to reuse, so every new proof starts from scratch.

On August 17, the Math-AI team open-sourced MathCode, which tackles both pain points at once: Lean compile checks drop from 30 seconds to 0.4 seconds (a 75x speedup), and every proof is automatically named, stored, and becomes an importable theorem, accumulating into a reusable Lean knowledge base.

MathCode is not positioned as a "translation tool" but as an "engineer": it continuously reads compile errors, revises its approach, and recompiles until the proof passes. This is a fundamentally different technical path from AlphaProof or Hunyuan-Prover — instead of training bigger proof models, it pushes the "prove-compile-feedback" engineering pipeline to its limit.

How Compilation Went from 30s to 0.4s

The traditional Lean workflow is: write a proof chunk → exit → start the compiler → wait 30 seconds. MathCode's key engineering change is persistent Lean REPL sessions: after a one-time warm-up, every subsequent compile check runs inside the same REPL session, avoiding repeated startup, repeated Mathlib loading, and repeated context initialization, yielding 0.4-second responses.

In other words, the model didn't get smarter — the pipeline got faster. Mathematicians can now iterate dozens of proof strategies in minutes instead of burning patience in waiting loops, finally matching the "save-and-compile" experience of traditional IDEs.

The Knowledge-Management Engineering

MathCode also "productizes" the proof process:

Auto-naming + storage: every proof is automatically named and archived for later import and reuse, instead of being discarded after completion
Assumption solidification: assumptions from conversation are converted into persistent, consistency-checked Lean declarations
Automatic retrieval: it automatically searches leansearch.net and Loogle to find verified Mathlib lemmas quickly
Obsidian knowledge graph: dependencies between theorems and lemmas are visualized as a clickable graph
Parallel subgoals: complex theorems can be split into independent subgoals, proved in parallel, then stitched together
Multiple planners: several proof planners run in parallel, letting the prover pick the optimal strategy

This upgrades mathematicians from "writing one proof chunk at a time" to "building their own formalized mathematics knowledge base." It's a quiet paradigm shift: for decades, intermediate results in mathematical proofs were rarely reused — every new proof manually re-linked from known theorems. MathCode automates this.

What It Still Cannot Do

A reality check: MathCode is not an "automatic prover" — it is an "accelerator + knowledge-management tool." What it can do: convert human-written propositions into Lean 4 theorems, provide automatic compile feedback, retrieve lemmas, and build knowledge graphs automatically. What it cannot do: guess what to prove next. Proposing problems, conjecturing theorems, and creative leaps in proof strategy still depend on human mathematicians.

Also, the 75x speedup presupposes an already-resident REPL session. Cold starts or first-time loading of large dependency graphs show no significant latency improvement over traditional workflows. MathCode's sweet spot is "medium-scale, frequently-iterated proof tasks," not "one-shot large proofs."

What It Changes

The mathematical proof toolchain has formally moved from "text editor + LaTeX + occasional Lean" into a new era of "AI collaboration + formal verification + knowledge graphs." This path echoes OpenAI's Astra series (publicized in early August, solving ten major math problems with roughly $2,000 of compute, with Lean 4 formal proofs open-sourced): Astra takes the "big model + big compute" route, while MathCode takes the "engineering optimization + small model" route — both making mathematical proof more accessible.

Three validation points to watch over the next 6 months: first, whether MathCode integrates into the official Lean toolchain or the VSCode Lean extension; second, whether Obsidian knowledge graphs become a standard attachment when mathematicians publish papers; third, whether the Chinese mathematics community — especially Fields Medalists Deng Yu and Wang Hong's research areas — adopts MathCode as a daily tool.

Mathematical proof may never be fully automated, but MathCode makes it no longer feel like endless drudgery.