MathCode: a terminal coding agent that checks Lean proofs while you write them

What MathCode actually solves for Lean users

An LLM writing Lean has a specific failure mode: it produces proof text that looks plausible and does not compile. The usual workaround is copy, paste, run lake build, read the error, paste it back. MathCode removes that loop by giving the agent tools that talk to a Lean process directly. The README describes the agent as able to "inspect goals, check candidates, search declarations, and verify a finished proof interactively." That is the whole pitch, and it is a narrow one.

The audience is correspondingly narrow. If you write Lean proofs and already have a working Lean and Mathlib setup, the value is obvious: the agent gets ground truth from the compiler rather than from its own confidence. If you do not write Lean, the bundled Lean toolchain is dead weight. The repository is a Shell project, and the setup script is the centre of gravity. There is no library to import and no API surface for embedding MathCode in another program.

How the agent, the runtime and the Lean workspace fit together

Three pieces are shipped together. The first is a runtime bundle: setup.sh downloads a matching mathcode-vX.Y.Z-<os>-<arch>.tar.gz asset and restores ./mathcode, ./mathcode-webui and vendor/ripgrep/ from it. That bundle also contains a ripgrep binary, which MathCode uses for its internal search paths rather than relying on whatever rg is on your PATH. The second piece is configuration: setup.sh creates .env from .env.example and installs a user-local launcher, by default into ~/.local/bin/. The third is the Lean workspace under lean-workspace/, which carries a versioned lake-manifest.json.

That manifest is the interesting design decision. Setup materializes the locked dependency graph without running lake update and without rewriting the manifest, so the Lean and Mathlib versions you get are the ones the release was tested against. The README is explicit that a local MathCodeLean readiness build follows the optional Mathlib cache fetch, that cache skips and download failures fall back to that build, and that a build failure aborts setup. In other words, setup will not hand you a half-installed Lean environment and call it success. It also materializes an empty managed VaultLibs/UserVaultLibs/ skeleton; source-host vault mirrors, test fixtures and scratch Lean files are deliberately not packaged.

The model backend is separate from all of this. The default route is OpenAI or Codex OAuth, with MATHCODE_USE_OPENAI=0 switching to an Anthropic backend or to OpenRouter through the OpenAI-compatible Responses API. Atomic Lean tools use whatever the active agent route is, and the .env.example notes they have no separate model or retry controller. So the Lean integration is not a distinct model; it is a tool layer on top of the same agent.

Installing MathCode and running a first proof prompt

The README quick start is four commands. The first two are a normal clone and cd. The third runs setup with Lean support enabled, which is the slow part because it bootstraps the Lean workspace and fetches Mathlib caches. The fourth logs in to the default Codex backend, and then mathcode starts the agent.

git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh --with-lean
codex auth login
mathcode

If you want to try the agent without the Lean toolchain, bash setup.sh --without-lean skips it. You can add it later with bash setup.sh --install-lean, and the README notes that the first approved local Lean feature call also offers to install it. Running bash setup.sh with no flag asks interactively and defaults to the full installation.

On Linux there is a prerequisite the quick start does not inline: setup requires bwrap (package bubblewrap) and socat before bootstrapping the Lean workspace. If your current shell has not reloaded its profile and mathcode is not found, ./run is the bundle-local fallback.

Once the agent is running, the CLI takes a prompt with -p. The README gives this example:

mathcode -p "prove that the square of an even number is even"

It also documents reading the prompt from stdin, so piping works:

echo "hello" | mathcode -p

What you should expect to see is not a single block of proof text. The agent has Lean-facing tools, so a session on a real proof involves goal inspection and candidate checking before anything is accepted. mathcode --help lists the rest of the CLI surface, and bash setup.sh --status reports whether the binary, the WebUI helper, the bundled rg and the optional Lean support are healthy.

The platform constraints are stricter than the README headline suggests

The requirements section is short and worth reading twice. MathCode supports macOS on arm64 and glibc-based Linux on x86_64 with AVX2, built on Ubuntu 22.04. There is no Windows target in the requirements, though setup does accept lean.exe and lake.exe pairs from Git Bash or MSYS, which implies a Git Bash workflow on Windows is at least partially contemplated. Alpine and other musl distributions are not covered by the glibc requirement.

Disk space is the second constraint, and it is not quantified. The requirements say only "enough disk space for the bundle, plus the Lean toolchain and Mathlib caches when Lean support is enabled." Anyone who has installed Mathlib knows that is not a small number, and the absence of a figure is a real gap in the documentation. The Lean workspace is also not something you can point at an existing installation by default: setup uses a complete bundle-local .local/elan Lean and Lake pair, and only uses system Lean and Lake when MATHCODE_SETUP_USE_SYSTEM_LEAN=1 is set and both tools are available. Even then it captures the system tools before changing into the bundle root and records their validated absolute paths in .env, so runtime resolution uses that exact pair regardless of a later PATH change. That is careful, but it also means switching toolchains is a setup-time decision, not something you flip mid-session.

Finally, the default math flow depends on the codex CLI. If you would rather not use that backend, .env.example documents the Anthropic and OpenRouter alternatives, but the quick start assumes Codex.

MathCode versus a general coding agent with a Lean MCP server

The obvious alternative is a general terminal coding agent wired to a Lean language server through MCP, or an editor plugin that already speaks to Lean. The difference is packaging and defaults, not capability in the abstract.

A general agent plus a Lean MCP server gives you one assistant for every language and a Lean integration you configure yourself. You control the Lean version, you control the server, and you can point it at an existing project. The cost is that you assemble it, and the quality of the Lean tooling depends on which server you picked.

MathCode inverts that. Lean support is the default, the toolchain is pinned by lean-workspace/lake-manifest.json, and setup repairs the runtime and the elan tool files for you. The README even documents that setup repairs partial local elan tool-file installs before bootstrapping the workspace. The cost is that MathCode is opinionated about its environment: bundle-local Lean unless you opt into system tools, a managed launcher, and a release-pinned dependency graph. If your work is 90 percent Lean, that trade is good. If Lean is one language among ten in your week, carrying a second agent and a second toolchain is hard to justify.

Maintenance, upgrades and what the Apache-2.0 licence means here

The last push to the repository was on 2026-09-09, and v0.3.0 was released on 2026-08-25. The project is not archived. It is also pre-1.0, and the setup script's behaviour reflects that: it downloads platform-specific runtime archives, verifies the current-platform SHA256SUMS.txt entry with shasum or sha256sum, validates downloaded files before replacing a working install, and records release metadata so later setup.sh and setup.sh --status runs can detect stale or unverified binaries. Upgrading is therefore a re-run of setup.sh against a new checkout rather than a package manager operation, and the release metadata is what tells you whether your local binaries still match the tag.

bash setup.sh --clean removes install artifacts but keeps proofs and vault data, and the README states it preserves user outputs in LeanFormalizations/, vault data and the release's locked Lake manifest. If setup previously recorded a managed launcher, later --status and --clean runs keep tracking it even when MATHCODE_INSTALL_BIN_DIR is unset. That is a sensible boundary, and it means the destructive option is less destructive than the name suggests.

The licence is Apache-2.0, which is permissive and includes a patent grant. The repository does not document redistribution obligations for the bundled runtime archive, the ripgrep binary under vendor/ripgrep/, or the Lean and Mathlib components pulled in during setup, and those components carry their own licences. If you plan to redistribute a MathCode bundle inside your organisation, that is the question to resolve before shipping anything, and it is a question for your own counsel rather than something the README answers.

Editorial conclusion

MathCode is worth adopting if you already write Lean and want an agent that can read the actual goal state instead of guessing at proof text. It is the wrong tool if you want a general-purpose coding assistant, if you work on Windows without Git Bash, or if you cannot spare the disk space for a Lean toolchain and Mathlib caches. Before committing, run bash setup.sh --status after installation and confirm that optional Lean support reports as ready rather than deferred or incomplete, because a deferred Lean install leaves the agent without the goal inspection and verification calls that distinguish it from a plain chat wrapper.

Frequently asked questions

Official sources

1. License: Apache-2.0
2. math-ai-org/mathcode on GitHub
3. Project website
4. README
5. Releases