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:

lean_interact_demo

Requirements

Install Lean using elan:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

Restart your shell, then check:

lean --version
lake --version

Python 3 and Jupyter are needed for the notebooks:

python3 --version
python3 -m pip install notebook

Setup

Clone the repository and enter the Lean project:

cd lean_interact_demo

The Lean toolchain is pinned in:

lean-toolchain

Download dependencies and build:

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

cd lean_interact_demo
bash demos/01_cli/run_bash.sh
jupyter notebook demos/01_cli/lean_cli_subprocess_demo.ipynb

02 Metaprogramming

cd lean_interact_demo
bash demos/02_metaprogramming/run.sh

03 LSP

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

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

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:

lake build
lake env lean demos/03_lsp/LspDemo.lean
lake env lean demos/04_mcp/McpDemo.lean