Lean Info

This Model Context Protocol (MCP) server bridges the gap for AI coding assistants working with Lean 4 proofs. While human users rely on the InfoView panel for interactive proof development, AI assistants typically lack this crucial visibility. Lean Info spawns a `lean --server` subprocess and exposes its Language Server Protocol (LSP) capabilities as MCP tools, enabling AI assistants to programmatically check files for errors, inspect proof goals at any tactic position, look up types, and search for declarations. This facilitates a more interactive and informed proof-writing process, allowing AI to operate with a similar understanding of the Lean environment as a human developer.

Key Features

Use Cases