MathCode v0.4.0

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

• Setup installs the CLI and WebUI without Lean/Mathlib by default; 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

git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh
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. No-argument bash setup.sh skips
Lean/Mathlib without prompting in both terminals and scripts. Existing Lean
installations are preserved.

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.

Packaging update — 2026-10-05

The macOS and Linux archives now skip Lean/Mathlib by default and include the
updated installation documentation. The CLI, WebUI, and ripgrep binaries are
unchanged. Archive checksums have been regenerated; use the current
SHA256SUMS.txt with the refreshed downloads.

Use the platform .tar.gz assets for this update. GitHub-generated source
archives remain tied to the original v0.4.0 tag.