A new open-source agent tries to close the gap between a confident-sounding math answer and a verified one. MathCode, built by a team called Math-AI, is a terminal coding assistant that takes a math problem written in ordinary language and translates it into a theorem in Lean 4, a proof assistant that checks each logical step of an argument by machine. It then attempts to construct a formal proof of that theorem.
Turning a claim into a machine-checkable theorem is the step that separates a plausible-looking proof from a genuinely verified one, a property large language model math has generally lacked. MathCode keeps a running Lean session open so checks execute quickly after the tool warms up, and it maintains growing libraries of proven theorems and stored assumptions that later sessions can reuse. It also generates an Obsidian graph mapping dependencies between theorems and lemmas, and it can split a hard theorem into smaller subgoals proved independently.
The project credits its formalization and proving pipeline to the earlier AUTOLEAN project. The documentation lists no benchmark scores, adoption numbers, or comparisons against rival provers.
According to the MathCode project page, published in August 2026.
