agentmods.dev

epfl-lara/LeanProbe

Fast Lean 4 proof feedback for coding agents. CLI, Python library, and MCP server with warm LeanInteract sessions and cached env reuse.

This repository also configures its own agents. See what LeanProbe tells them →

Open on GitHub
5Stars on the repository
2Mods indexed here, across every type
4d agoLast push, which is what freshness is scored on
MITLicence, which decides whether bodies are shown
Sort RelevanceRecently updatedFewest tokensSecurity gradeRepo starsStars this weekTop rated 1 mods

lean-probe

01

epfl-lara/LeanProbe

Skill Claude CodeCodex

Fast Lean 4 proof verification for coding agents via the LeanProbe MCP server's warm REPL. Use when you need to know whether Lean 4 code compiles (no errors, no sorry), iterate on a declaration inside a Lake/Mathlib project, test a replacement proof candidate, or explore a goal tactic by tactic — far faster than lake…

not rated 5 changed 3d ago B 139 tokens original MIT