MathCode Terminal AI Speeds Up Mathematical Proofs 75x: From 30 Seconds to 0.4 Seconds

Forum topic · 小凯 · 2026-08-17

Summary

MathCode, an open-source terminal AI tool released on August 17 by the Math-AI team, addresses two long-standing pain points in formal mathematics: slow Lean 4 compilation (often 30+ seconds) and poor reusability of formalized proofs. By keeping a persistent Lean REPL session alive after a one-time warm-up, MathCode cuts compile-check latency to 0.4 seconds—a 75x speedup—eliminating repeated startup, Mathlib loading, and context initialization. Beyond speed, it operates as an automated engineering pipeline: continuously reading compile errors, revising approaches, and recompiling until proofs pass. Every proof is automatically named, stored, and made importable as a reusable theorem, building a persistent Lean knowledge base. Features include solidifying conversational assumptions into consistency-checked Lean declarations, automatic lemma retrieval via leansearch.net and Loogle, an Obsidian knowledge graph visualizing theorem dependencies, parallel sub-goal proving, and multiple concurrent proof planners. MathCode is explicitly an accelerator and knowledge-management tool rather than an automatic prover—creative leaps and conjectures remain human tasks. The 75x speedup only applies with a warm REPL session; cold starts remain slow, making it best suited for medium-scale, iterative proof work. Its engineering-optimization path contrasts with large-model approaches like AlphaProof and OpenAI's Astra series.

Mathematical proof formalization has long suffered from two problems: Lean 4 compilation takes 30+ seconds at a time, forcing mathematicians to wait; and formalized theorems 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 made importable as a theorem, accumulating into a reusable Lean knowledge base.

Its positioning is not that of a "translation tool" but an "engineer": it continuously reads compile errors, revises its approach, and recompiles until the proof passes. This is a technical path entirely different from AlphaProof or Hunyuan-Prover—instead of training bigger proof models, it pushes the "proof–compile–feedback" engineering pipeline to its limits.

How Compilation Went from 30 Seconds to 0.4 Seconds

The traditional Lean workflow is "write a proof segment → exit → launch the compiler → wait 30 seconds." MathCode's key engineering change is keeping the Lean REPL persistent: after a one-time warm-up, every subsequent compile check runs in 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 iterate dozens of proof strategies in minutes instead of burning patience while waiting—finally aligning with the traditional IDE "save-and-compile" experience.

The Engineering of Knowledge Management

MathCode also "productizes" the proof process:

Automatic naming + storage: every proof is automatically named and archived for later import and reuse, rather than discarded after completion;
Assumption solidification: assumptions from conversation are turned into persistent, consistency-checked Lean declarations;
Automatic retrieval: it queries leansearch.net and Loogle to quickly locate verified Mathlib lemmas;
Obsidian knowledge graph: dependencies between theorems and lemmas are visualized as a clickable graph;
Parallel sub-goals: complex theorems can be split into independent sub-goals, proven in parallel, then stitched together;
Multiple planners: several proof planners run in parallel, letting the prover pick the best strategy.

This upgrades mathematicians from "writing one proof segment 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" but an "accelerator + knowledge management tool." What it can do: automatically convert human-written propositions into Lean 4 theorems, compile with feedback, retrieve lemmas, and build knowledge graphs. What it cannot do: guess what to prove next. Posing propositions, conjecturing theorems, and creative leaps in proof strategy still depend on human mathematicians.

Also, the 75x speedup presumes an already-persistent REPL session. Cold starts or first loads 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-off large proofs."

What Changes

The mathematical proof toolchain officially moves from "text editor + LaTeX + occasional Lean" into a new stage of "AI collaboration + formal verification + knowledge graphs." This path echoes OpenAI's Astra series (early August), which tackled ten major open math problems with roughly $2,000 of compute and open-sourced Lean 4 formal proofs—Astra is the "big model + big compute" path, MathCode the "engineering optimization + small model" path; both make formal proof more accessible.

Three things to watch over the next six months: whether MathCode integrates into the official Lean toolchain or the VSCode Lean extension; whether the Obsidian knowledge graph becomes a standard attachment for published papers; and whether the Chinese mathematics community—including the research fields of new Fields Medalists Yu Deng and Hong Wang—adopts MathCode as a daily tool.

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