Acerca de
Lean Proof Auto is a Model Context Protocol (MCP) server designed to streamline and enhance the process of working with Lean 4 proof automation. It provides a suite of tools for static theorem-level analysis, deep analysis of specific theorems, objective-based ranking, and robust Lean validation. Developers can use it to measure baseline automation efficiency, search for candidate automated proofs using hint sets, and validate concrete proof attempts, all while extracting relevant theorem context. Its deterministic nature ensures consistent results, making it an invaluable resource for developing and verifying Lean 4 proofs.
