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/nasqret/lean-interact/installnpx skills add nasqret/lean-interact --skill installgit clone --depth 1 https://github.com/nasqret/lean-interactWhat 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.00221 | $0.06658 |
| Opus 5 | $0.00111 | $0.03329 |
| Sonnet 5 | $0.00044 | $0.01332 |
| Haiku 4.5 | $0.00022 | $0.00666 |
Grade C, and why
install scanned grade C with 2 findings 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 2d 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.
Downloads and executes remote codehighSupply chain
curl | sh runs whatever the server returns today, which is not necessarily what it returned when this was reviewed.
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh Makes network callslowCapability
Not a fault in itself. Listed so you know the mod talks to something, and to what.
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh How it starts
The opening of the file, as written. The whole thing — 510 lines — stays where its author put it; the contents beside it link to each section on GitHub.
install
Bring a fresh clone of lean-interact to the point where the user can type a sentence of
ordinary mathematics and watch it compile. Repository root: /path/to/lean-interact — the
directory this clone lives in. Use absolute paths when reading and editing files, but run
every command below from the repository root with the repo-relative paths as written: that is
the form .claude/settings.json allows without a permission prompt.
Run the steps in order. Each step has a command and a stated correct result. Do not advance past a step whose result does not match. A half-installed harness fails later in ways that look like mathematics problems rather than install problems, which is expensive.
Standing rules for this procedure
- Report before you change. Do the whole of step 1 and tell the user what is missing before installing anything.
- Never start a Mathlib build from source. The pins exist precisely to prevent it. If
lakestarts compiling Mathlib, that is a stop-and-diagnose condition, not a wait. - One
lakeat a time.laketakes a lock on.lake/. Whilelake updateorlake exe cache getis in flight, run no otherlakecommand and read or write nothing under.lake/. - Do not run the elan installer for the user. See step 2 for why.
- No pip installs. All runtime tooling in
tools/is Python 3 standard library only. The only optional pip package anywhere near this project isjupyter-book, which buildsbook/and is not part of the harness.
Rough budget on a good link: minutes for steps 1-2, tens of minutes for step 3 (a few GB of
download), a few minutes for steps 4-6 (most of it lake build NtLean). Say this up front so the user knows what they
are committing to.
1. PRE-FLIGHT
Detect the platform and inventory the tools. Change nothing in this step.
uname -s # Darwin or Linux
uname -m # arm64, x86_64
command -v elan lean lake git python3 # the required set
python3 -c 'import sys; print(sys.version.split()[0], sys.version_info >= (3,10))'
command -v tmux jq ssh jupyter-book # the optional set
ls "/Applications/Visual Studio Code.app/Contents/Resources/app/bin/code" 2>/dev/null
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.
- 2d ago First seen · 510 lines · 221 tokens per session scan C 85f81c7856c8
install is a skill published in the GitHub repository nasqret/lean-interact (10 stars, last pushed 24d ago), licensed MIT. It adds 221 tokens to every session and 6,658 once invoked, about $0.0011 per session on Opus 5. A static security scan graded it C with 2 findings (downloads and executes remote code, makes network calls). No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-31.
Other skills, from other repositories
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…
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…
lean-probe
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…
audit-public-operation-contracts
Audit new or existing Jacobian mathematical operations for public-domain mismatches, hidden work expansion, evidence-backed scale or backend improvements, lossy exact results, source-unbound conclusions, and producer-consumer incompatibility. Use for operation-contract reviews, mathematical performance investigations…
learn-from-math-agent-trajectories
Review completed or paused mathematical agent transcripts, visible reasoning, code, searches, tool calls, corrections, and final claims to extract evidence-backed lessons for Jacobian operations, discovery, contracts, skills, evaluations, and documentation. Use for mathematical workflow retrospectives and "what should…
decompose-mathematical-solution-corpora
Decompose a bounded corpus of mathematical proofs, formalizations, scripts, and certificates into recurring solution techniques and the smallest reusable Jacobian postconditions. Use for repository- or corpus-level “what can Jacobian learn?” audits; do not use for one operation contract or one agent trajectory.