MathCode
MathCode is a terminal AI coding assistant with built-in Lean capabilities, letting the agent inspect proof goals, check candidate steps, search declarations and verify a finished proof interactively.
MathCode is a terminal-based AI coding agent focused on mathematical and formal-proof work, built with integrated support for the Lean theorem prover. It can inspect open goals, check candidate proof steps, search Lean declarations, and interactively verify a completed proof.
Its setup script downloads or repairs a bundled runtime, installs a local launcher, and can install the Lean and Mathlib toolchain either during setup or later, with a smaller installation available when Lean support is not needed. On Linux, Lean setup additionally requires bubblewrap and socat. Setup also creates local configuration and extension directories, plus a bundled skills directory that MathCode's own skills load from, and it verifies downloaded release archives against published checksums before installing them.
Authentication for the underlying model is handled through Codex's own login flow.