// HACKER NEWS — CYBERSECURITY

MathCode, Mathematical Coding Agent

Published: 08/16/2026, 06:17 PM

MathCode is a terminal AI coding assistant with a built-in math formalization engine. Give it a math problem in plain language and it will automatically convert it into a Lean 4 theorem and attempt a formal proof — with a persistent Lean REPL, reusable theorem and axiom libraries, agentic proving, and an Obsidian knowledge graph. Requires macOS (arm64) or Linux (x86_64), plus the codex CLI for the default backend. setup.sh prepares the release checkout, downloads the bundled runtime and Lean toolchain, and installs a user-local mathcode launcher. Try it with: Outputs are written to LeanFormalizations/. A browser UI is available via ./run webui. The math formalization and proving pipeline is based on the AUTOLEAN project. Overview • Quick Start • Features • Citation • GitHub • Discord • Yifan's Blog