mathcode

About

MathCode brings the agentic coding workflow to formal mathematics, where a proof is machine-checkable and verification is unambiguous. The agent inspects goals at explicit source positions, compiles candidate proofs with structured feedback, and treats only LeanVerify's verified flag as completion, with optional in-process REPL and Kimina Lean Server backends feeding the loop. Persistent theorem and axiom libraries store verified results transactionally, an Obsidian graph visualizes theorem dependencies, and three extension mechanisms (project-local skills, auto-discovered Python tools, plugin folders with commands/skills/agents/MCP servers/hooks) let formalization teams add domain tooling. Checksum-verified release binaries ship with a setup script that installs and health-checks Lean and Mathlib; mathematicians and formalization teams are the users.