Zulip Chat Archive

Stream: new members

Topic: Claude Code, MCP, LSP, and Lean

Dan Abramov (Jul 04 2025 at 13:56):

I'm an AI noob but I've started playing with Claude Code and enjoying it.

I was wondering if there's a way to hook up Claude Code to Lean somehow. I want it to be able to access the InfoView during the proof and also to be able to get the build output without running lake build on that file every time.

Maybe there's an MCP/LSP setup that works with Lean?

Dan Abramov (Jul 04 2025 at 14:14):

Currently testing https://github.com/oOo0oOo/lean-lsp-mcp, it seems to work

Chris Bailey (Jul 04 2025 at 14:20):

There's also this thing but the readme sort of expects you to know what all of the tools it interfaces with do (which I do not).

Dan Abramov (Jul 04 2025 at 15:48):

So far it seems to work decently if I:

use the Opus model
explicitly remind it to read CLAUDE.md
and have this in CLAUDE.md:

# CLAUDE.md

This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.

## CRITICAL

- Read "How to Solve Problems" below and apply it religiously, or you'll be fired. (Sorry.)

## How to Solve Problems

- Say "woof" to acknowledge you've read this before every edit.
- Plan every change!  This is mathematics. You *need* to plan. Don't just rush with edits. Make every edit meaningful.
- Always restate the problem before any change to the code.
- If something didn't work out, summarize *why* it didn't work out first.
- Keep track of whether your *high-level* approach makes sense.
- When "fixing" the code, always determine whether you're sticking with the previous high-level approach or if there was a flaw in it. If there was a flaw, write down the flaw clearly, and how much you need to repair.
- Use the LSP tools like a human would. Examine the goal state on different lines, see what theorems are avaiable, hover on things to learn their types. Use all of this information when planning the next step.
- Try to keep the file green. It's better to add `sorry`s than bad solutions. If you see a bunch of diagnostic failures, make a smaller change, then fix `sorry`s.
- It's okay to get diagnostic errors. Just go through them methodically and determine for each whether it signals a flaw in the big strategy or a small mistake. Use that when planning the next change.
- Try to `rw` things, `apply` things, `simp` things, see what completions are available inside and which ones fix the diagnostics.
- Remind yourself to be methodical all the time.

## Before Completing a Task

- You can use `lake build` with specific filename to check for final errors.
- Remove excessive comments and see if you can simplify the proof once you know its shape.

## Essential LSP Tools

### lean_goal
**MOST IMPORTANT TOOL** - Always use this before making any edit to understand what you need to prove.

### lean_diagnostic_messages
Check for errors, warnings, and infos. Read these BEFORE continuing.

### lean_completions
Find available constants, tactics, and lemmas. Essential for discovering the right method names.

### lean_hover_info
Get documentation and type information for symbols.

Dan Abramov (Jul 04 2025 at 15:49):

One problematic thing is that the "completions" LSP is kind of returning shit results. I'm not sure if it's worse than VS Code or not. They just feel... never relevant.

Screenshot 2025-07-04 at 16.47.13.png
Screenshot 2025-07-04 at 16.47.20.png

I wonder if it's a known problem in general. I wish there were getting filtered down to "matching" types somehow, or if "matching" types were prioritized.

Oliver Dressler (Jul 04 2025 at 16:46):

Yes, the completion tool is quite weak. It is directly based on the code completion via LSP. E.g. in VS Code type import Mathlib. and you should get the same results.

In general the external search tools, like loogle, are quite a bit better:
https://github.com/oOo0oOo/lean-lsp-mcp#external-search-tools

I can also recommend using the LeanExplore MCP for an additional set of search tools.

Dan Abramov (Jul 04 2025 at 16:47):

I think it's actually worse than VS Code because it doesn't seem to do sorting. VS Code sorts on the client. The options seem to be (1) add sorting to the tool, or (2) fix the server to do its own preliminary sort.