From Prompts to Protocols

The workflow is a bottleneck we can control

LLM coding agents are already useful Lean copilots. For large formalizations, model intelligence is not the only bottleneck. One bottleneck we can control is the workflow: knowing when to search, inspect, edit, checkpoint, review, and stop.

After the fundamentals

• You have already seen Lean and Mathlib, tactics, blueprints, and AI-assisted formalization. I’ll assume you know what goals and tactics look like.
• So this is not “what is Lean?” It is: how do we engineer a human–agent–Lean workflow that survives a real project, one that lasts weeks or months?
• Lean makes AI assistance unusually attractive: there is an external judge. The model proposes edits; Lean checks whether the proof term exists.
• But Lean checks a proof against a statement. It does not tell you whether the statement is the theorem you meant, whether the API is maintainable, or whether the proof survives a Mathlib update.

Contents

1. A formalization story: de Finetti in Lean.
2. Why good models still need workflow.
3. How lean4-skills turns prompts into a protocol.
4. Demo: a real captured session.
5. Evaluation: how do we know it improved?
6. What you can use on your own projects.

de Finetti’s theorem

The Lean formalization is the standard-Borel, measure-theoretic version of this story. This involves kernels, conditional laws, and uniqueness of product measures.

de Finetti–Ryll-Nardzewski in Lean 4

Informally: an infinite exchangeable sequence (one whose joint law is invariant under finite permutations of coordinates) is conditionally i.i.d., given a directing random probability measure.

Ryll-Nardzewski’s formulation packages this as an equivalence involving contractability; exchangeability is one side of that equivalence.

The library’s headline theorem, stated in Lean:

theorem deFinetti_RyllNardzewski_equivalence
    [StandardBorelSpace Ω]
    {α : Type*} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
    {μ : Measure Ω} [IsProbabilityMeasure μ]
    (X : ℕ → Ω → α) (hX_meas : ∀ i, Measurable (X i)) :
    Contractable μ X ↔ Exchangeable μ X ∧ ConditionallyIID μ X

The proof engineering involves standard Borel spaces, conditional laws as kernels, conditional independence, product-measure uniqueness, and L¹/L² convergence.

2.5 pages of math → tens of thousands of lines of Lean

• The blow-up is not just verbosity. It is bridging informal math to existing Mathlib APIs: conditional expectation, kernels, σ-algebras, product-measure uniqueness, L¹/L² transport.
• Since the ITP artifact, the project has shrunk by ~37% through paper-review cleanup: more Mathlib reuse, proof golfing, dead-code removal, and stronger model-assisted refactoring.
• Formalization is library and interface engineering, and it keeps evolving: as Mathlib grows and tooling improves, the artifact gets smaller.

Three roads to the same theorem

Three independent routes discharge one shared interface.

One common ending

All three routes had to produce the same intermediate interface: finite conditional factorization relative to a sub-σ-algebra. From there a single shared “common ending” builds:

1. a directing probability kernel;
2. the right measurability package;
3. the conditionally i.i.d. conclusion.

100+ files converging on a shared interface. The common ending is both a mathematical interface and a workflow guardrail.

The common ending as supervision

Three independent routes feeding one interface gave continual cross-checks. They caught:

• route-specific definitions creeping into shared APIs;
• missing measurability hypotheses;
• overly specialized helper lemmas;
• statement drift: locally convenient but globally wrong interfaces.

For AI-assisted formalization this matters: the agent gets a hard, reusable target, and divergence between routes is immediately visible.

Predictable failures without guardrails

Coding agents are often surprisingly useful at Lean. But without guidance, agents do not automatically follow the discipline that Lean developers learn over time. Common failure modes (stated charitably):

• Reprove a lemma Mathlib already has.
• Ignore Lean diagnostics or the goal state.
• Change the theorem statement to make the proof easier.
• Add brittle local adapters instead of using Mathlib idioms.
• Paper over typeclass problems by adding more instances.
• Loop on the same stalled proof path.
• Produce code that compiles but is slow, obscure, or hard to upstream.

These operational failures are predictable consequences of optimizing locally without enough process.

From a prompt file to a protocol layer

lean4-skills grew out of the de Finetti project. When an agent hit a rough spot (a bad instance, a skipped Mathlib search, mishandled conditional-expectation bookkeeping), I often moved the relevant context into a separate skill-development session. That session folded in the new knowledge, keeping enough of the real example to stay concrete, and turned it into reusable guidance.

• Recurring situations became reference files.
• Repeated action sequences became command workflows.
• Tool-use lessons became Lean LSP MCP guidance.

The shift: from wording a single prompt to structuring the whole interaction: search, inspect, bound, checkpoint, review, replan, hand off.

Protocol countermeasures

Each row is a failure observed in real agent work, paired with the protocol response.

Stopping with a clear obstruction is a success, not a failure. It lets the user replan, and keeps the coding agent from going in circles.

The lean4-skills architecture

The skill does not bypass Lean. Lean and Mathlib feedback stays external and authoritative.

Anatomy: a skill is not one prompt

lean4-skills is a layered Lean workflow pack. The current plugin distribution targets Claude Code, but the core skill content is mostly host-agnostic. The model sees a short contract first, and pulls in detail only when the situation calls for it.

• SKILL.md: a short, always-visible contract.
• commands/ (11): /draft, /formalize, /autoformalize, /prove, /autoprove, /checkpoint, /review, /refactor, /golf, /learn, /doctor.
• agents/ (4): proof-repair, proof-golfer, sorry-filler-deep, axiom-eliminator.
• references/ (39): cycle engine, LSP tools, Mathlib search, compilation errors, measure theory, instance pollution, golfing, performance, and more.
• Scripts and hooks: sorry analysis, axiom checks, search wrappers, import minimization, a command-argument parser, UserPromptSubmit validation, and shell guardrails.

Durable rules stay in front of the model; specialized advice loads only when it is relevant.

Progressive disclosure: the always-visible contract

SKILL.md is deliberately short and normative: a small constitution the agent sees on every task.

• Search before prove.
• Build incrementally (the type-checker is the test suite).
• Respect scope: one sorry, a file, or everything (ask if unclear).
• Use Lean / Mathlib conventions; 100-character lines.
• Never change declaration headers, theorem statements, or signatures, or add axioms, without permission.
• Prefer LSP goal / diagnostic / search tools before script fallback.
• Use commands for multi-cycle work; finish with checks (build, no stray sorries, standard axioms, statements preserved).

A routing layer: pick the workflow first, then disclose the right details.

SKILL.md: the contract, from the source

## Core Principles

**Search before prove.** …
**Build incrementally.** …
**Respect scope.** …
**Use 100-character line width for Lean files.** …
**Never change statements or add axioms without explicit permission.** …

This is the part the model sees every time: a small operational constitution, not one clever paragraph.

Where each lesson goes

Rule of thumb: universal invariant → SKILL.md; detailed Lean lore → reference; repeated procedure → command; bounded specialist task → subagent or script.

How it grew: patterns and antipatterns → references → workflows → contracts

• Oct 2025: During the de Finetti project I wrote down the failures that cost me time (conditional expectation, σ-algebra bookkeeping, instance pollution, elaboration timeouts, Mathlib-search misses, statement drift) into a reference library; progressive disclosure appeared almost immediately.
• Oct 2025: Repeated manual workflows became slash commands.
• Jan–Feb 2026: Lean LSP MCP guidance; guided /prove split from autonomous /autoprove; a shared cycle engine; build-verification ladder; /learn.
• Mar 2026: MCP-first subagents, header fences, capability profiles, and /refactor.
• Apr–May 2026: Hardening: stop budgets, one-editor-per-file rules, scratch-file policy, portability, CI, and community PRs.

When a failure repeated often enough, I wrote it down as a reference, promoted it to a workflow, or hardened it into a contract.

Where the protocol is actually enforced

Not every rule is enforced at the same layer. Part of building the skill was deciding whether a rule should be a prompt, a tool habit, a script, a hook, or a build gate. Sorry-freedom and standard-axiom checks are separate gates.

The bounded proof loop

/lean4:prove in detail

A slash command constrains the process, not just the final answer. /prove runs that bounded loop one cycle at a time, asking before each new cycle:

• Plan: discover sorries via LSP; search Mathlib (up to 3 tools, ~30s); show the plan and confirm.
• Work: refresh the goal, search, generate 2–3 candidates, test with lean_multi_attempt, validate diagnostics, apply Lean’s “Try this” code actions, then edit.
• Checkpoint: stage only accepted files; build the agreed scope.
• Review: read-only quality gate (drift, API, performance).
• Replan: split, refactor, escalate to deep mode, or mark stuck.
• Continue? ask the human before the next cycle.

The fast path caps candidates per sorry, keeps diffs small, forbids cross-file refactors, and treats declaration headers as immutable; deep mode adds snapshot and rollback under a line budget.

/lean4:prove: the agent may not change the theorem

**Constraints:** … NO statement changes, … Declaration headers are immutable — if deep mode suggests a header change, it must stop and recommend `/lean4:formalize`.

…

## Stuck Definition

A sorry is **stuck** when: same failure 2-3x, same build error 2x, …

**When stuck:** … Handoff must include LSP queries attempted, top candidates, and `lean_multi_attempt` outcomes.

The agent does not get to prove a different theorem. When stuck, it stops with evidence.

Subagent: proof-repair

A subagent is a specialized prompt with a narrow input/output contract. proof-repair turns an antipattern (“after a local error, rewrite too much”) into an interface: structured error context in, a unified diff out.

## Constraints

- Output ONLY unified diff (no explanations)
- Change ONLY 1-5 lines per call
- Stay within stage budget
- May NOT rewrite entire functions
- May NOT try random tactics
- May NOT skip mathlib search
- May NOT modify declaration headers (header fence). …
…

Intentionally boring: classify the error, make the smallest plausible edit, return a diff. That is an antipattern promoted to a contract.

What kind of prompting is this?

Mostly operational and constraint-heavy: what evidence to collect, what not to touch, when to escalate, and what shape the output takes.

lean-lsp-mcp: the agent’s InfoView and Mathlib search

Humans use the Lean InfoView to read goals, hypotheses, errors, and types, and they search Mathlib for lemmas. lean-lsp-mcp gives the agent analogous feedback and search tools. Without it, the agent loses much of the feedback loop human Lean users rely on.

The protocol tells the agent when to reach for each: search before proving, inspect the goal before editing, verify before claiming done.

Demo transcript

One small Lean snippet, three easy sorries, captured with Claude Code / Opus 4.8. Prompt:

❯ let's work on these: example (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by sorry
  example [DecidableEq α] (s t : Finset α) (h : s ⊆ t) : s.card ≤ t.card := by sorry
  example (p q : Prop) : p ∧ q → q ∧ p := by sorry

The theorems are intentionally small so the workflow is visible. In a hard theorem the same loop is still there, just harder to see because the math dominates.

 ▐▛███▜▌   Claude Code v2.1.156
▝▜█████▛▘  Opus 4.8 (1M context) with xhigh effort · Claude Max
  ▘▘ ▝▝    ~/work/spherepacking-repos/Sphere-Packing-Lean


❯ let's work on these: example (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by sorry
  example [DecidableEq α] (s t : Finset α) (h : s ⊆ t) : s.card ≤ t.card := by sorry
  example (p q : Prop) : p ∧ q → q ∧ p := by sorry


● I'll start by invoking the Lean 4 skill since we're working on Lean proofs.

● Skill(lean4:lean4)
  ⎿  Successfully loaded skill

● These are three straightforward warm-up examples. Let me verify the proofs compile using the Lean REPL.

● Now let me verify all three proofs compile:

  Called lean-lsp (ctrl+o to expand)

● I need to prime the project path first. Let me check a file in the project.

  Searched for 1 pattern, called lean-lsp 2 times (ctrl+o to expand)

● The proofs are correct — the only errors are because autoImplicit is off in this project, so I need to explicitly bind α. Let me add the type variable:

  Called lean-lsp (ctrl+o to expand)

● All three compile cleanly (the remaining message is just a whitespace-linter artifact from the snippet layout). Here are the proofs:

  example {α : Type*} (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by
    rw [List.length_append]

  example {α : Type*} [DecidableEq α] (s t : Finset α) (h : s ⊆ t) : s.card ≤ t.card :=
    Finset.card_le_card h

  example (p q : Prop) : p ∧ q → q ∧ p :=
    fun ⟨hp, hq⟩ => ⟨hq, hp⟩

  Notes:

  1. List length — List.length_append is the statement, so rw closes it. Even shorter: := List.length_append (term mode) or by simp.
  2. Finset card — Finset.card_le_card : s ⊆ t → s.card ≤ t.card applies directly. (DecidableEq isn't actually needed for this lemma, but it's harmless to keep.)
  3. Conjunction swap — pure term mode: destructure the hypothesis and rebuild swapped. Equivalent alternatives: fun h => ⟨h.2, h.1⟩ or And.comm.mp.

  One thing to flag: your originals wrote List α / Finset α without binding α. This project sets autoImplicit false, so I added {α : Type*} explicitly — without it the snippets don't compile
  here. If you're dropping these into a section that already has a variable {α : Type*}, you can omit the per-example binder.

  Want me to place these somewhere in the repo, or were they just warm-up exercises?

✻ Worked for 1m 30s

Transcript detail: Lean feedback changes the answer

 ▐▛███▜▌   Claude Code v2.1.156
▝▜█████▛▘  Opus 4.8 (1M context) with xhigh effort · Claude Max
  ▘▘ ▝▝    ~/work/spherepacking-repos/Sphere-Packing-Lean


❯ let's work on these: example (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by sorry
  example [DecidableEq α] (s t : Finset α) (h : s ⊆ t) : s.card ≤ t.card := by sorry
  example (p q : Prop) : p ∧ q → q ∧ p := by sorry


03:08 PM claude-opus-4-8
● I'll start by invoking the Lean 4 skill since we're working on Lean proofs.

● Skill(lean4:lean4)
  ⎿  Successfully loaded skill

03:08 PM claude-opus-4-8
● These are three straightforward warm-up examples. Let me verify the proofs compile using the Lean REPL.

03:08 PM claude-opus-4-8
● Now let me verify all three proofs compile:

● lean-lsp - Run Code (MCP)(code: "import Mathlib\n\nexample (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by\n  rw [List.length_append]\n\nexample [DecidableEq α] (s t :
  Finset α) (h : s ⊆ t) : s.card ≤ t.card :=\n  Finset.card_le_card h\n\nexample (p q : Prop) : p ∧ q → q ∧ p :=\n  fun ⟨hp, hq⟩ => ⟨hq, hp⟩")

03:09 PM claude-opus-4-8
● I need to prime the project path first. Let me check a file in the project.

● Bash(find /home/freer/work/spherepacking-repos/Sphere-Packing-Lean -name "*.lean" -path "*ContourEndpoints*" 2>/dev/null | head -5)
  ⎿  /home/freer/work/spherepacking-repos/Sphere-Packing-Lean/SpherePacking/MagicFunction/a/ContourEndpoints.lean

● lean-lsp - Diagnostics (MCP)(file_path: "/home/freer/work/spherepacking-repos/Sphere-Packing-Lean/SpherePacking/MagicFunction/a/ContourEndpoints.lean")
  ⎿  {
       "result": {
         "success": false,
         "timed_out": false,
         "items": [],
         "failed_dependencies": []
       }
     }

● lean-lsp - Run Code (MCP)(code: "import Mathlib\n\nexample (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by\n  rw [List.length_append]\n\nexample [DecidableEq α] (s t :
  Finset α) (h : s ⊆ t) : s.card ≤ t.card :=\n  Finset.card_le_card h\n\nexample (p q : Prop) : p ∧ q → q ∧ p :=\n  fun ⟨hp, hq⟩ => ⟨hq, hp⟩")
  ⎿  {
       "success": false,
       "timed_out": false,
       "diagnostics": [
         {
           "severity": "error",
           "message": "Unknown identifier `α`\n\nNote: It is not possible to treat `α` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.",
           "line": 3,
           "column": 23
         },
         {
           "severity": "error",
           "message": "Unknown identifier `α`\n\nNote: It is not possible to treat `α` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.",
           "line": 3,
           "column": 23
         },
         {
           "severity": "error",
           "message": "Unknown identifier `α`\n\nNote: It is not possible to treat `α` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.",
           "line": 6,
           "column": 22
         },
         {
           "severity": "error",
           "message": "Unknown identifier `α`\n\nNote: It is not possible to treat `α` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.",
           "line": 6,
           "column": 39
         },
         {
           "severity": "error",
           "message": "Unknown identifier `α`\n\nNote: It is not possible to treat `α` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.",
           "line": 6,
           "column": 39
         },
         {
           "severity": "warning",
           "message": "'' starts on column 26, but all commands should start at the beginning of the line.\n\nNote: This linter can be disabled with `set_option linter.style.whitespace
     false`",
           "line": 10,
           "column": 27
         }
       ]
     }

03:09 PM claude-opus-4-8
● The proofs are correct — the only errors are because autoImplicit is off in this project, so I need to explicitly bind α. Let me add the type variable:

● lean-lsp - Run Code (MCP)(code: "import Mathlib\n\nexample {α : Type*} (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by\n  rw [List.length_append]\n\nexample {α : Type*}
  [DecidableEq α] (s t : Finset α) (h : s ⊆ t) : s.card ≤ t.card :=\n  Finset.card_le_card h\n\nexample (p q : Prop) : p ∧ q → q ∧ p :=\n  fun ⟨hp, hq⟩ => ⟨hq, hp⟩")
  ⎿  {
       "success": true,
       "timed_out": false,
       "diagnostics": [
         {
           "severity": "warning",
           "message": "'' starts on column 26, but all commands should start at the beginning of the line.\n\nNote: This linter can be disabled with `set_option linter.style.whitespace
     false`",
           "line": 10,
           "column": 27
         }
       ]
     }

03:10 PM claude-opus-4-8
● All three compile cleanly (the remaining message is just a whitespace-linter artifact from the snippet layout). Here are the proofs:

  example {α : Type*} (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by
    rw [List.length_append]

  example {α : Type*} [DecidableEq α] (s t : Finset α) (h : s ⊆ t) : s.card ≤ t.card :=
    Finset.card_le_card h

  example (p q : Prop) : p ∧ q → q ∧ p :=
    fun ⟨hp, hq⟩ => ⟨hq, hp⟩

  Notes:

  1. List length — List.length_append is the statement, so rw closes it. Even shorter: := List.length_append (term mode) or by simp.
  2. Finset card — Finset.card_le_card : s ⊆ t → s.card ≤ t.card applies directly. (DecidableEq isn't actually needed for this lemma, but it's harmless to keep.)
  3. Conjunction swap — pure term mode: destructure the hypothesis and rebuild swapped. Equivalent alternatives: fun h => ⟨h.2, h.1⟩ or And.comm.mp.

  One thing to flag: your originals wrote List α / Finset α without binding α. This project sets autoImplicit false, so I added {α : Type*} explicitly — without it the snippets don't compile
  here. If you're dropping these into a section that already has a variable {α : Type*}, you can omit the per-example binder.

  Want me to place these somewhere in the repo, or were they just warm-up exercises?

✻ Worked for 1m 30s

/learn: keeping human understanding in the loop

When agents write more of the proof, humans can learn less, unless explanation is built into the workflow. /learn explores Mathlib around a topic, explains why a lemma applies, and grounds informal claims in checked definitions.

  Pedagogy: Socratic mode, starting from the user’s prior knowledge to calibrate depth.

  What does it mean for a function to be “measurable” between two measurable spaces?
  If someone hands you f : α → β and both carry a MeasurableSpace instance,
  what property must f satisfy?

How do we know it got better?

If I change the skill, how do I know the change helped? There is no single number.

Quality is layered, and a change can improve one layer while harming another:

• A change can be good because it makes the agent less aggressive: stop sooner, search first, hand off more clearly.
• A change can prove more toy theorems while making real projects worse by rewarding brittle hacks.

A practical evaluation harness

The evaluation stack

Kernel correctness is the floor; quality and workflow gates sit above it. A failed attempt can still improve the workflow if it stops earlier with a useful obstruction summary.

Why A/B testing skill changes is hard

• Model behavior is stochastic.
• Long Lean tasks branch heavily, with many hidden paths.
• Skill changes often affect tool-use patterns indirectly.
• A “successful” proof can be low quality; a “failed” one useful if its obstruction summary is accurate.
• One benchmark can reward brittle behavior a real project would reject.

So evaluation mixes:

regression tasks · build/sorry/axiom checks · trace review · qualitative failure analysis · project dogfooding · user reports · benchmark batches when available.

/lean4:golf: golfing is review, not line-count hacking

Score candidates by: correctness → directness → clarity/inference burden → performance/determinism → length. …

**Hard reject if:** introduces naked `;` · introduces `<;>` on non-identical goals (per semicolon policy) … collapsed term > ~80 chars or dot-chain > 2 …

A shorter proof can be worse; golfing is a win only if it stays at least as direct, clear, and deterministic.

/lean4:review: evaluation as a command

A review command makes quality checks repeatable. It reports the project’s state; it does not prove anything.

How skill changes evolve

Projects where I’ve refined or used lean4-skills

The workflow is portable (measure theory, combinatorics, logic, computation), but each domain needs its own interfaces and review norms.

E8 root system. (J. Gregory Moxness)

A cube has Rupert’s property. (David Renshaw / Quanta)

The Noperthedron does not. (David Renshaw)

Where this is heading

Some of this is already live; some is active design work, tracked in the open issues and PRs on lean4-skills and lean-lsp-mcp.