Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
npx agentmods add skills/epfl-lara/leanprobe/skillnpx skills add epfl-lara/LeanProbe --skill skillgit clone --depth 1 https://github.com/epfl-lara/LeanProbeWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/epfl-lara/leanprobe/skill)<a href="https://agentmods.dev/skills/epfl-lara/leanprobe/skill"><img src="https://agentmods.dev/badge/skills/epfl-lara/leanprobe/skill.svg" alt="Measured on agentmods" height="20"></a>What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5 | $0.00139 | $0.02382 |
| Opus 5 | $0.00069 | $0.01191 |
| Sonnet 5 | $0.00028 | $0.00476 |
| Haiku 4.5 | $0.00014 | $0.00238 |
Grade B, and why
lean-probe scanned grade B with 1 finding against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 3d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Reads agent configuration directoriesmediumAgent snooping
.claude/, .codex/, .gemini/ hold keys, settings and other credentials a mod has no legitimate need for.
For Codex, add to `~/.codex/config.toml`: How it starts
The opening of the file, as written. The whole thing — 205 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Using LeanProbe
LeanProbe gives coding agents fast Lean 4 feedback through a warm
LeanInteract REPL. Use it in
the inner loop to verify Lean code far faster than lake build. LeanProbe never
edits files; apply accepted code yourself and run lake build as the final
whole-project gate before committing.
This skill is the usage contract for the LeanProbe MCP tools. It assumes the
lean-probe MCP server is connected to your client (see "Connecting the server"
at the bottom). The server also advertises a condensed version of this guide in
its instructions field, so a connected agent gets the essentials on connect.
Tool Selection
| Tool | Use When | Main Result |
|---|---|---|
lean_check |
You have a standalone Lean snippet (imports + code) and want to know if it is valid. The default tool. | Diagnostics and ok (valid, no sorry). |
lean_check_target |
Checking or replacing one named declaration inside a project file; you want the fast warm-environment path. | Pass/fail plus Lean messages; optional tactics/feedback_lean. |
lean_status |
Setup is uncertain, or you want to pay cold-start up front. | Readiness (project root, REPL, sessions); warm=true boots the REPL. |
lean_proof_state |
Exploring a goal from code containing sorry. |
A session_id and one proof-state id per sorry. |
lean_tactic |
Applying one tactic to a proof state. | New goals/proof state, or ok=true when Completed. |
lean_close_proof |
Finished with a proof-state session. | Releases the session's REPL process. |
lean_check is the low-friction default: no file path or declaration name
needed. Reach for lean_check_target when you are iterating on one declaration
inside a project file, because it reuses the file's warm prior environment and is
typically tens of milliseconds after the first call.
Reading Results
Every tool returns a JSON object. Read two fields, in order:
success: did the tool run.falsemeans an environment problem (no project root, file not found, timeout, REPL crash). Readerror_codeandhintand fix that first; do not interpret it as a Lean result.ok: did Lean accept the code.success=truewithok=falseis a real Lean rejection — inspectmessages.ok=truemeans it elaborated with no errors and nosorry; warnings alone do not flipok.
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 3d ago First seen · 205 lines · 139 tokens per session scan B eefa5ae26671
lean-probe is a skill published in the GitHub repository epfl-lara/LeanProbe (4 stars, last pushed 2mo ago), licensed MIT. It adds 139 tokens to every session and 2,382 once invoked, about $0.0007 per session on Opus 5. A static security scan graded it B with 1 finding (reads agent configuration directories). No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-31.
Other skills, from other repositories
formalize
Formalize a claim of ordinary mathematics as Lean 4 + Mathlib and drive the live compile loop to zero errors. Use whenever the user states a mathematical claim, conjecture, exercise or definition; asks to formalize, state, prove, check or Lean-ify something; corrects or refines a previous formalization; asks why a…
formalize-from-magma
Turn Magma code into a formalized Lean theorem. Use whenever the user pastes or points at Magma source, asks what a Magma routine is really proving, asks to formalize a computation or a computationally-discovered pattern, or wants a Magma experiment turned into a general statement. Covers running the code on…
lean-session
Bring up, check, or repair the live Lean session: the terminal watcher over Scratch/Current.lean, the browser dashboard, and the VS Code infoview. Use when the user says start a session, open the windows, show me the live view, is the watcher running, restart the dashboard, nothing is updating, or when a formalization…
mathlib-api
Evidence-driven workflow for designing a Mathlib definition and the API around it. Use when adding a new structure/def intended for mathlib; when choosing between design alternatives (index type as field vs parameter, Set vs indexed family, coarse set vs finer indexed structure and when the fine one should exist at…
paper-search
Search, download, and read academic papers from 20+ sources (arXiv, PubMed, Semantic Scholar, CrossRef, etc). Use when the user asks to find papers, search for research, look up academic literature, download a paper PDF, or extract text from a paper.
patent-diagram-generator
Create patent-style technical diagrams including flowcharts, block diagrams, and system architectures using Graphviz with reference numbering.