A command that translates a Lean declaration—a formally checked mathematical statement—into standard mathematical language. It can show the statement and a paragraph-length proof outline in the terminal or export it in other formats.

Use it to explain one declaration, include its dependencies, process a Lean file, print Markdown or Verso markup, or append the result to a project blueprint.

Formal Lean code can be hard to read as mathematics. This provides a human-readable explanation without requiring a mathematics renderer.

unformalise — Command for coding agents by CBirkbeck: A command that translates a Lean declaration

Install

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.

agentmods

npx agentmods add commands/cbirkbeck/mathlib-quality/unformalise

Clone the repo

git clone --depth 1 https://github.com/CBirkbeck/mathlib-quality

Or install mathlib-quality, the plugin that ships this one along with the rest of its 2 skills, 23 commands, 6 agents, 2 hooks.

Wrote 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.

README.md

[![agentmods](https://agentmods.dev/badge/commands/cbirkbeck/mathlib-quality/unformalise.svg)](https://agentmods.dev/commands/cbirkbeck/mathlib-quality/unformalise)

Your own site

<a href="https://agentmods.dev/commands/cbirkbeck/mathlib-quality/unformalise"><img src="https://agentmods.dev/badge/commands/cbirkbeck/mathlib-quality/unformalise.svg" alt="Measured on agentmods" height="20"></a>

Per session 155 Only the description is in the session, so the agent can decide to use it. The body loads when it is invoked.

When invoked 4,943 The whole file, excluding the scripts and references it only reads on demand.

Security scan A 0 findings. Scan, not verified.

Origin original No closer match found in the catalogue.

Token cost

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.00155	$0.04943
Opus 5	$0.00077	$0.02472
Sonnet 5	$0.00031	$0.00989
Haiku 4.5	$0.00015	$0.00494

Measured 4d ago against content hash 3ac57b9bbf8f, method: parsed. Prices are Anthropic first-party input rates as of 2026-08-30, from the pricing page.

Security

Grade A, and why

unformalise scanned grade A with 0 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 4d 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.

Nothing flagged

None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.

commands/unformalise.md · 487 lines

How it starts

The opening of the file, as written. The whole thing — 487 lines — stays where its author put it; the contents beside it link to each section on GitHub.

/unformalise — Turn Lean into mathematics

Take a Lean declaration and render its mathematical statement plus a paragraph-level proof sketch in standard mathematical English. Default output is Unicode in the terminal — readable directly in chat, without a LaTeX renderer.

This is the conversational front-door for the same unformalisation logic that /blueprint Phase 4 uses to author whole-project blueprints. Use /unformalise when you want to see the math first; use /blueprint when you want to commit the math to the project artifact.

Usage

/unformalise <Foo.bar>                  # single declaration, Unicode in terminal (default)
/unformalise <Foo.bar> --closure        # decl + dependency closure (every {uses} target)
/unformalise <file.lean>                # every public declaration in the file
/unformalise <Foo.bar> --verso          # print Verso directives to stdout (no blueprint write)
/unformalise <Foo.bar> --md             # print GitHub-flavoured Markdown to stdout
/unformalise <Foo.bar> --blueprint      # append to <Project>/Chapters/ as Verso (same as /blueprint --decl)
/unformalise <Foo.bar> --statement-only # skip the proof sketch

After the terminal Unicode render, the command asks what you want next (blueprint / Verso / Markdown / nothing). The --verso / --md / --blueprint flags skip that prompt — useful when wiring this into a pipeline or another command.

Prerequisites

Project is a Lean 4 project that builds clean (lake build exits 0). The skill uses lean_local_search / Grep to locate declarations; a broken build leaves the LSP unable to resolve names.
For --blueprint output: the verso-blueprint scaffold exists at the project root (the project_template/ layout from leanprover/verso-blueprint has been copied in — <Project>/Chapters/, <Project>/Blueprint.lean, <Project>Main.lean, scripts/ci-pages.sh). See /blueprint Phase 0 for bootstrap instructions.
For best quality: .mathlib-quality/references/ directory of source-paper notes and/or a .mathlib-quality/blueprint/prose_context.md from a prior /blueprint run. The skill works without them but leans more heavily on Lean docstrings.

Read the full file on GitHub · 487 lines

Changes

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.

4d ago First seen · 487 lines · 155 tokens per session scan A 3ac57b9bbf8f

Subscribe to this mod's changes

unformalise is a command published in the GitHub repository CBirkbeck/mathlib-quality (32 stars, last pushed 16d ago), licensed MIT. It adds 155 tokens to every session and 4,943 once invoked, about $0.0008 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.

Scientific

unformalise

Getting it into your agent

Wrote this? Show the measurements

What it costs to keep this loaded

Grade A, and why

Nothing flagged

How it starts

/unformalise — Turn Lean into mathematics

Usage

Prerequisites

What this file has done since we first saw it

Other commands, from other repositories

master_analysis

render-figures

replication-package

diff

arg-diagram

simulation-calibrator