lean-mcp

Lean LSP via mcporter - Skill

This skill enables interactive inspection of Lean proof states using the Lean Language Server Protocol via mcporter.

When to use this skill

• You're stuck on a Lean proof and need to see the exact goal state after simplifications
• Your rw or simp commands aren't matching the expected pattern
• You want to understand what a tactic is actually doing
• You need to verify a proof compiles without waiting for full lake build

Setup (one-time)

npm install -g mcporter
# uv should already be installed (check with: which uv)

The config/mcporter.json in the repo is already configured for the lean-lsp MCP server.

Key Commands

1. View proof state at a line (MOST IMPORTANT)

mcporter call lean-lsp.lean_goal \
  file_path:/absolute/path/to/File.lean \
  line:123

Returns:

• goals_before: Goal state at the start of the line
• goals_after: Goal state at the end of the line (after tactic executes)
• Shows exactly how the tactic transforms the goal

Example:

cd /mnt/data-2tb/tmp/clean
mcporter call lean-lsp.lean_goal \
  file_path:/mnt/data-2tb/tmp/clean/Clean/Examples/FibonacciWithChannels.lean \
  line:728

2. Get diagnostics (errors/warnings)

mcporter call lean-lsp.lean_diagnostic_messages \
  file_path:/absolute/path/to/File.lean \
  start_line:100 end_line:150

3. Try multiple tactics without modifying the file

mcporter call lean-lsp.lean_multi_attempt \
  file_path:/path/to/File.lean \
  line:123 \
  'snippets:["simp", "rw [foo]", "exact bar"]'

Returns the goal state after each tactic, so you can see which one makes progress.

4. Get type/documentation for a symbol

mcporter call lean-lsp.lean_hover_info \
  file_path:/path/to/File.lean \
  line:123 column:10

Column should be at the START of the identifier you want to inspect.

5. Search for theorems/lemmas

# Natural language search via LeanSearch
mcporter call lean-lsp.lean_leansearch \
  query:"sum of two even numbers is even" \
  num_results:5

# Type signature search via Loogle  
mcporter call lean-lsp.lean_loogle \
  query:"(?a → ?b) → List ?a → List ?b" \
  num_results:8

# Semantic search via LeanFinder
mcporter call lean-lsp.lean_leanfinder \
  query:"I have h : n < m and need n + 1 < m + 1" \
  num_results:5