Lean Proof Auto MCP

Example Use Cases

• 1

  Analyze and triage Lean 4 theorem files and targets.

• 2

  Probe and measure automation success on Lean theorems.

• 3

  Search, validate, and verify automated proof attempts in Lean projects.

Description

This MCP server provides tools for static and deep analysis of Lean 4 theorem files, automation probing, proof validation, and context extraction. It supports workflows for discovering, ranking, probing, searching, and validating automated proofs within Lean projects. The server enables integration with Lean 4 toolchains to facilitate proof automation and validation in a deterministic and normalized manner.