Lean workflows

Proof tools

MathCode works directly on Lean files in the selected workspace. The agent chooses tools as needed; /lean provides optional guidance.

Tool	Use
`LeanGoal`	Inspect a goal at an explicit source position.
`LeanCheck`	Compile a file or temporary candidate for feedback.
`LeanSearch`	Search declarations through one selected provider.
`LeanVerify`	Strictly verify one fully qualified declaration.

Only a successful LeanVerify result with data.verified=true certifies completion. Its default timeout is 1,200 seconds; timeout_s can be set up to 3,600 seconds. Goal/check feedback alone is not a certificate.

The agent may use helper lemmas, subgoals, branching and theorem reuse. Atomic proof tools do not silently store theorems, add axioms, or update a vault.

Theorem library

/theorem-store store <file> <qualified-declaration>
/theorem-store sync
/theorem-store check
/theorem-store status

store verifies and stores one explicit theorem. It rechecks the source and dependencies, verifies the renamed declaration in Stored.lean, and builds an importable module. Failed publication rolls back the library update. Compilation and publication each have a 300-second build budget.

sync discovers candidates and asks which declarations to store. check compile-checks the assembled library; status reports stored count and vault information. LibSearch is available only with an active vault through MATHCODE_OBSIDIAN_VAULT or /obsidian on. Without one, use LeanSearch.

Axiom library

/axiomatize "A is faster than B"
/axiomatize list
/axiomatize check
/axiomatize remove <name>

Declarations are stored per vault with Lean compile checks and a consistency review. Import or reference them explicitly when they belong in the proof context. Atomic Lean calls do not inject stored assumptions automatically.

Obsidian

/obsidian on
/obsidian off
/obsidian generate

Use generate after changing proofs, then open the vault in Obsidian Graph View to inspect dependencies. Lemma notes include definitions queried from Mathlib. Generation updates MathCode-managed notes and recognized legacy projections; it preserves unrelated user notes and fails on conflicting filenames.

Paper catalog IDs must not collide. If another paper already has the ID derived from a title and authors, choose a distinct ID or another vault. Dependency-cycle errors identify the involved claims and how to repair the catalog.

Optional feedback backends

Eligible generic compile callers can use the in-process REPL with MATHCODE_LEAN_REPL=1. Atomic proof tools do not use that cache.

On macOS, an external Kimina Lean Server can provide LeanGoal and LeanCheck feedback:

MATHCODE_KIMINA_SERVER=1
MATHCODE_KIMINA_CMD="/absolute/path/to/kimina-lean-server/.venv/bin/python -m server"
MATHCODE_KIMINA_CWD=/absolute/path/to/kimina-lean-server
MATHCODE_KIMINA_PROJECT_ROOT=/absolute/path/to/served-lean-project

The declared project and Lean version must match the current project. Start Kimina directly with Python; any virtualenv must be below MATHCODE_KIMINA_CWD. MathCode launches it in a loopback-only sandbox without provider credentials, with writes limited to private scratch space. Setup, compatibility or transport failures fall back to the pinned subprocess and report a warning.

Kimina feedback is not a completion certificate. LeanVerify and isolated paper agents always use fresh isolated subprocesses. Linux and Windows use pinned subprocesses for this feedback path; the release archives themselves support only the platforms listed in the installation guide.