Borrowing it
Nothing to install: this file belongs to nasqret/lean-interact. Take a copy, put it at the same path in your own repository, and replace the rules that are about this project with yours.
curl -O https://raw.githubusercontent.com/nasqret/lean-interact/main/.claude/skills/install/SKILL.mdgit clone --depth 1 https://github.com/nasqret/lean-interactWrote 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/nasqret/lean-interact/install)<a href="https://agentmods.dev/skills/nasqret/lean-interact/install"><img src="https://agentmods.dev/badge/skills/nasqret/lean-interact/install/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/nasqret/lean-interact/install"><img src="https://agentmods.dev/badge/skills/nasqret/lean-interact/install.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.00221 | $0.06658 |
| Opus 5.5 | $0.00088 | $0.02663 |
| Sonnet 5.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 2mo 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.
- 2mo ago First seen · 510 lines · 221 tokens per session scan C 85f81c7856c8
install is a skill published in the GitHub repository nasqret/lean-interact (11 stars, last pushed 2mo ago), licensed MIT. It adds 221 tokens to every session and 6,658 once invoked, about $0.0009 per session on Opus 5.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…
lean-expert
Lean 4 theorem-prover expertise for agents -- current versions, tactic cookbook, Mathlib search, compiler-error recoveries. Use when proving, debugging, or explaining Lean 4 proofs via leanforge-mcp.
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…
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…
omega
Omega Reasoning Protocol — changes how the LLM thinks. Three principles: FORCING (what is structurally inevitable), MINIMIZE (remove assumptions until something breaks), AUDIT (every conclusion traceable to premises). Searches github.com/the-omega-institute/automath for structural correspondences. Use when: deep…
pub-cycle
Publication Cycle — scans the main theory paper, identifies new paper extractions and existing paper gaps, then orchestrates the full review+fix pipeline. Workflow: Triage → Codex review+fix (2 rounds) → ChatGPT review → Codex fix → Claude review → Codex fix → ChatGPT journal-targeted acceptance gate. During wait…