MathCode v0.4.0

MathCode v0.4.0 ships the terminal assistant and browser WebUI for macOS Apple Silicon (arm64) and Linux x86_64. Linux requires an AVX2-capable CPU. Download the matching archive and verify it against SHA256SUMS.txt from GitHub Releases.

Highlights

• Install the CLI and WebUI without Lean/Mathlib, then add the pinned Lean runtime when needed. Approved local Lean operations can install deferred support on first use; remote search and caller-owned projects do not trigger this installation.
• System-Lean setup resolves Elan launchers to concrete Lean and Lake binaries, verifies both against the workspace pin, and falls back to bundle-local Lean when validation fails.
• Tool validation errors, warnings, and structured result diagnostics preserve actionable details consistently, including Unicode text at output limits.

Install or upgrade

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

For an existing checkout, run git pull --ff-only and rerun setup. Use bash setup.sh --with-lean for a complete installation or bash setup.sh --install-lean to add Lean/Mathlib later. Allow about 10 GiB of additional disk space for Lean support. Interactive bash setup.sh asks which mode to use; non-interactive setup defaults to the complete installation.

Start the browser interface with ./run webui --no-browser and open the local URL printed in the terminal. Setup also installs the mathcode command for new shells. Existing configuration is preserved.