Prove
Prove mode — fill the `sorry`/`admit` placeholders in an existing Lean file with real proofs, using the Mem0-g plan graph + compile-fix subagent. Run in the MAIN context. Use when asked to "prove the sorries", complete unfinished declarations, or formalize a stubbed Lean file. Success is mechanical: clean build with no residual sorry/admit/axiom.
Formalize
Orchestrate formalizing a paper (or filling sorries) into verified Lean 4, using the Mem0-g plan graph as the statement store. Run this in the MAIN context. It dispatches compile-fix as a SUBAGENT (separate context) and performs plan edits (the update agent) plus all faithfulness/paper checks IN the main context. Use when asked to formalize a paper, build a Lean library from a plan, or drive the…
Auto Research
Auto-research mode — take an OPEN QUESTION in informal natural language and resolve it end-to-end in Lean 4, SELF-CONTAINED — formalize it into a faithful statement `:= by sorry`, then RELENTLESSLY prove or disprove it. FULLY AUTONOMOUS (never asks the user; ambiguous formalizations decided by canonical reading, loudly documented and banked), no axioms ever, direction pivots only on independently…
Formalizeproblem
Turn an INFORMAL mathematical problem into faithful, type-checking Lean 4 statement(s) with `:= by sorry` — translation only, no proving. Careful with ill-posed problems — it surfaces inequivalent readings and asks before committing. Run in the MAIN context. Use when asked to "formalize this problem", "translate this statement to Lean", "state this in Lean", or to prepare a statement for prove mo…
Plan Graph
Read, edit, and SEMANTICALLY SEARCH the formalization statement plan stored in the Mem0-g plan graph (the replacement for statements.json). Use whenever you need to inspect, query, or modify statements, dependencies, status, or informal notes; run the Lean dependency sync; or find statements/notes by MEANING (LeanSearch-v2-style two-stage retrieval: OpenAI embedding recall → LLM rerank) — e.g. to…
Init Merlean
Set up the MerLEAN system in this repo (replaces the old src/deploy.sh) — build the shared Python .venv from src/requirements.txt, write the root .mcp.json for the lean-lsp MCP server, ensure an OpenAI key in .env, and prepare the root Lean + Mathlib workspace (lake update / cache get / build). Use when asked to install, set up, initialize, or (re)deploy MerLEAN, or when a fresh clone needs its r…