lean-interaction-mcp-course

# Lean Interaction MCP Course Demo This project contains runnable demos for a lecture on programmatic interaction with Lean: - command-line Lean and Python subprocess - Lean metaprogramming - Lean LSP access from Python - MCP concepts and Lean MCP-style tool calls The Lean/mathlib project is in: ```text lean_interact_demo ``` ## Requirements Install Lean using `elan`: ```bash curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh ``` Restart your shell, then check: ```bash lean --version lake --version ``` Python 3 and Jupyter are needed for the notebooks: ```bash python3 --version python3 -m pip install notebook ``` ## Setup Clone the repository and enter the Lean project: ```bash cd lean_interact_demo ``` The Lean toolchain is pinned in: ```text lean-toolchain ``` Download dependencies and build: ```bash lake update lake exe cache get lake build ``` `lake exe cache get` downloads prebuilt mathlib artifacts when available, which avoids building all of mathlib locally. ## Run Demos ### 01 CLI ```bash cd lean_interact_demo bash demos/01_cli/run_bash.sh jupyter notebook demos/01_cli/lean_cli_subprocess_demo.ipynb ``` ### 02 Metaprogramming ```bash cd lean_interact_demo bash demos/02_metaprogramming/run.sh ``` ### 03 LSP ```bash cd lean_interact_demo jupyter notebook demos/03_lsp/lean_lsp_demo.ipynb ``` This notebook starts `lake serve` and queries Lean LSP for diagnostics, hover, proof goals, symbols, and definitions. ### 04 MCP ```bash cd lean_interact_demo jupyter notebook demos/04_mcp/lean_mcp_demo.ipynb ``` This notebook shows MCP-style Lean tool call results, including diagnostics, hover, get-goal, try-tactic, and a candidate tactic loop. ## Project Layout ```text student.md README.md lean_interact_demo/ lean-toolchain lakefile.toml lake-manifest.json demos/ 01_cli/ 02_metaprogramming/ 03_lsp/ 04_mcp/ ``` `teacher.md` is intentionally not part of the public repository. ## Useful Checks From `lean_interact_demo`: ```bash lake build lake env lean demos/03_lsp/LspDemo.lean lake env lean demos/04_mcp/McpDemo.lean ```