Maithilee Patawar

LAMP: Lean-based Agentic framework with MCP and Proof Repair

Santhana Srinivasan R, Maithilee Patawar

Large language models are increasingly capable of mathematical reasoning, but the proofs they generate are often unreliable and hard to verify. Interactive theorem provers such as Lean 4 address this by accepting only kernel-checked proofs; however, their reach is bounded by the…Read more