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 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/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/skills/epfl-lara/leanprobe/skill"><img src="https://agentmods.dev/badge/skills/epfl-lara/leanprobe/skill.svg" alt="Reviewed on agentmods" width="80" 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.1 | $0.00139 | $0.02926 |
| Opus 5.5 | $0.00056 | $0.01170 |
| Sonnet 5.5 | $0.00028 | $0.00585 |
| Haiku 4.5 | $0.00014 | $0.00293 |
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 7d 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 — 246 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.
- 7d ago Changed · +41 lines f3425d7d97da
- 1mo 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 (6 stars, last pushed 7d ago), licensed MIT. It adds 139 tokens to every session and 2,926 once invoked, about $0.0006 per session on Opus 5.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
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…
screen
Screen informal↔Lean 4 statement pairs for faithfulness defects. Use whenever writing, editing, translating, or reviewing Lean 4 theorem or definition statements that are meant to formalize informal mathematics: after drafting a statement, before committing formalizations, when auditing a benchmark file, or when the…
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.
paper-search
Search, download, and read academic papers through the paper-search MCP tools (mcppaper-search), covering arXiv, PubMed, bioRxiv, Semantic Scholar, Crossref, OpenAlex and 15+ other sources. Use when the user asks to find papers, search research literature, download a paper PDF, or extract text from a paper.
quantum-ground-state
A narrowly defined quantum solver for the ground-state energy of a two-quantum-bit Pauli Hamiltonian in a specified one-excitation sector. It uses a noiseless statevector VQE and checks the result against an exact calculation; VQE is a method that searches for a low-energy quantum state.
qmclaw-workbench
A local simulator for superconducting quantum-bit experiments, including measurements used to study and tune a qubit. It produces bounded synthetic results without connecting to laboratory hardware or quantum cloud services.