lean4-skills: Protocols for Inspectable AI-Assisted Lean Formalisation

Mathematical values worth preserving

The Leiden Declaration on AI and Mathematics frames the field around values worth preserving:

• proof confers “the highest degree of certainty” and “understanding of why”, supporting the “scientific integrity” of mathematics;
• results are “attributable to specific authors” who “take credit” and “assume responsibility for their correctness”;
• arguments are “transparent and subject to independent verification”, with “no proprietary knowledge or equipment” required;
• evaluation against “shared standards of depth, difficulty, and significance”;
• doing mathematics builds “understanding, clarity, and judgment” in communities of mathematicians;
• mathematicians autonomously shape research directions and the methods used to pursue them.

Protocols for Lean coding agents provide a partial answer

Where should trust live?

The workflow is also a trust boundary

LLM coding agents are already useful Lean copilots. For large formalisations, model intelligence is not the only bottleneck. The controllable bottleneck is the workflow: when to search, inspect, edit, checkpoint, ask the human, and stop. Making those moments explicit preserves human agency.

One risk: gradual disempowerment

Lean is an external judge, but only relative to a statement. A tool can make you faster while making you less informed.

So the protocol must preserve statement ownership, search visibility, proof-trace review, explanation on demand, and meaningful stop points.

Contents

1. Values worth preserving, where trust should live, and how the workflow protects agency.
2. Why capable models still need workflow guardrails.
3. What lean4-skills is: an inspectable protocol layer.
4. Mathlib search as a protocol.
5. de Finetti as origin story and stress test.
6. Evaluation: did the human end up understanding more?

Predictable failures without guardrails

Without guidance, agents do not automatically follow the discipline that Lean developers learn over time. The failures are familiar from human Lean users too; the difference is that agents repeat them faster, and without the same contextual judgement.
Common failure modes:

• 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 optimising locally without enough process. Each gets a specific protocol countermeasure.

What lean4-skills is: four perspectives

• To the coding agent: an always-visible contract, plus Lean lore loaded on demand: search first, test before editing, stop with evidence.
• To the human formaliser: control surfaces: statement fences, bounded attempts, checkpoints, reviewable traces.
• To the Lean community: a shared, versioned repository of agent-facing practice, the lore humans pick up from Zulip and review.
• To the field: a workflow layer over existing coding agents, complementing retrieval, premise selection, and proof-step systems.

From a prompt file to a protocol layer

lean4-skills grew out of a large formalisation I was working on, of de Finetti’s theorem for exchangeable sequences of real random variables.

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 is from wording a single prompt to structuring the whole interaction: search, inspect, bound, checkpoint, review, replan, and hand off.

Control surfaces

Each control problem above maps to a specific, inspectable interface.

The agent asks before touching a signature

From a recent cleanup session in the exchangeability repo, captured with Claude Code (Fable 5):

While that builds, the Step 2b question the plan requires me to ask before touching
the signature:

● User answered Claude's questions:
  · Step 2b: the new ~8-line proof of `eLpNorm_two_sq_eq_integral_sq` (LpNormHelpers.lean)
    via `MemLp.eLpNorm_eq_integral_rpow_norm` doesn't need `[IsFiniteMeasure μ]`.
    Drop the hypothesis (signature weakening, own commit), or keep it?
    → Drop it (Recommended):

Protocol countermeasures

Each row is a recurring failure mode 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: the layers of a skill

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 loads the contract when a Lean task matches the short trigger description; details then load as the situation calls for them (progressive disclosure).

• Frontmatter trigger description: the only part always in context; says when to invoke (.lean edits, build errors, Mathlib search) and when not to (Rocq, Agda, Isabelle, …).
• SKILL.md body: a short contract, loaded when a Lean task triggers it.
• 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 minimisation, a command-argument parser, UserPromptSubmit validation, and shell guardrails.

Durable rules stay in front of the model; specialised 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 and Mathlib conventions; wrap Lean lines at 100 characters.
• 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.

The SKILL.md contract

This is the part the model sees on every task: a short operational contract.

Mathlib search as agency and attribution

Searching before proving is not only an efficiency rule. It forces the agent to ask:

• What has the community already proved?
• What names and abstractions does Mathlib use?
• Which theorem should be cited by dependency, not duplicated locally?
• Which local lemma is really a wrapper around existing work?

Search has to be operationalised

A useful search protocol specifies:

1. what evidence to collect from the goal;
2. which search tool to try first;
3. how to rephrase when results are weak;
4. how to inspect candidate declarations;
5. how to test candidates before editing;
6. when to stop and report what was tried.

Humans do this implicitly: look at the goal, recall naming conventions, search, inspect a type, adapt, test. The agent needs that turned into a checklist.

A staged Mathlib search procedure

An escalation order, not a checklist: start local (unlimited, instant), climb only while the question is unanswered, and skip rungs that do not match it (premise suggestions only matter when simp/aesop/grind is planned). Each rung answers a different question; the last rung turns a candidate into evidence.

Demo: one definition, five ways to ask

Wanted: the Mathlib operation that maps a measure forward along a function.

By short name
  lean_loogle("Measure.map")
    → ✗ no results

By type shape, as first written
  lean_loogle("Measure ?X -> (?X -> ?Y) -> Measure ?Y")
    → ✗ no results   (Loogle resolves constants by full name: rephrase)

By type shape, qualified
  lean_loogle("MeasureTheory.Measure ?X -> (?X -> ?Y) -> MeasureTheory.Measure ?Y")
    → ✓ exactly one hit
      MeasureTheory.Measure.map (f : α → β) (μ : Measure α) : Measure β
      [Mathlib.MeasureTheory.Measure.Map]

By qualified name
  lean_loogle("MeasureTheory.Measure.map")
    → ✓ the constant, plus every lemma mentioning it:
      MeasureTheory.Measure.map · .map_id · .map_id' · MeasurableEmbedding.map_injective …

By natural language
  lean_leansearch("pushforward of a measure along a function")
    → the neighbourhood, not the target:
      Measure.mapₗ · ProbabilityMeasure.map · FiniteMeasure.map

By mathematical meaning
  lean_leanfinder("the pushforward (image) of a measure under a map")
    → ✓ MeasureTheory.Measure.map, informal name "Pushforward measure"
      (returns the formal type paired with an informal description)

Captured with lean-lsp-mcp (lean_loogle, lean_leansearch, lean_leanfinder), 9-11 June 2026.

The search protocol

The search policy is written down as agent-facing reference, rather than improvised per session.

Search → test → apply

1. lean_goal(file, line)           # What to prove?
2. lean_local_search("keyword")    # Find candidates
3. lean_multi_attempt(file, line, snippets=[  # Test them all
     "  apply candidate1",
     "  exact candidate2",
     "  simp [candidate3]"
   ])
4. [Edit with winner]
5. lean_diagnostic_messages(file)  # Confirm

When does a note become infrastructure?

Universal invariant → SKILL.md
Detailed Lean lore → reference
Repeated procedure → command
Bounded specialist task → subagent or script
The development pattern: write down the pain, then promote it only when it repeats.

How it grew: lean4-skills is a memory of mistakes

I didn’t start by designing a general system; rather, I began by writing down the repeated failures that cost me time in exchangeability:

• missed Mathlib APIs;
• σ-algebra and conditional-expectation bookkeeping;
• instance pollution and elaboration timeouts;
• statement drift;
• proof paths that had stopped making progress.

Then the pattern was simple: record the lesson; reuse it in the next session; promote it to a command or subagent if it kept recurring; harden it into checks where failure was costly. (Oct 2025 through May 2026: references, then commands, then subagents and fences, then stop budgets, CI, and community PRs.)

Not every rule should be a prompt

Some rules are advice, some are evidence, some are gates. The recurring design question: which layer should enforce this rule?

A proof attempt needs stop points

/lean4:prove is allowed to fail

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, check diagnostics, take Lean’s “Try this” suggestions when offered, 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 (slower; snapshot and rollback under a line budget), 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. The command constrains the process; it does not promise a proof.

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

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

proof-repair: local error, local diff

A subagent is a specialised 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.

Deliberately boring: classify the error, make the smallest plausible edit, return a diff. A repair agent should repair, not redesign.

The prompts specify work habits

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

Lean feedback has to enter the loop

A human Lean user has the InfoView: goals, hypotheses, types, diagnostics, hover, search. An agent needs the same feedback loop, but also needs to show how it used it. lean-lsp-mcp supplies the tools; the protocol supplies when to use them and what evidence to report back.

The protocol tells the agent when to reach for each: search before proving, inspect the goal before editing, verify before claiming done. Without this, the agent edits without the feedback loop a human Lean user relies on.

Evidence trace: search → test → verify

Goal
  ⊢ s.card ≤ t.card        (h : s ⊆ t)

Search   (goal shape + naming conventions → name fragment)
  lean_local_search("card_le_card")
    → Finset.card_le_card · Multiset.card_le_card · Set.card_le_card · Ordinal.card_le_card …
    → the goal is about a Finset: try Finset.card_le_card

Test  lean_multi_attempt
    exact Finset.card_le_card h          ✓
    simpa using Finset.card_le_card h    ✓
    exact card_le_card h                 ✗ Unknown identifier `card_le_card`

Edit
  apply the winner: exact Finset.card_le_card h

Verify
  lean_diagnostic_messages → no errors

Review
  statement unchanged · no new imports · no local adapter ·
  proof uses a recognisable Mathlib API

Tool outputs captured with lean-lsp-mcp against Mathlib, 9 June 2026.

What disclosure looks like

Three easy sorries. The proofs were right immediately, and still failed in this project (autoImplicit is off); Lean’s diagnostics, not the model’s confidence, produced the working version. (Full version in the appendix.)

 ▐▛███▜▌   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

/learn: proof as understanding, not just closure

Proof should confer not just certainty but understanding of why: /learn explains the definitions, checks its claims against Lean, and quizzes the human along the way.

❯ let's /learn how the calculation avoided rounding issues in real arithmetic

● Skill(lean4:learn)   ⎿  Successfully loaded skill

  Searched for 1 pattern, read 2 files, listed 1 directory, ran 2 shell commands

● This is already the heart of it. Let me check the two remaining pieces — how the √ comparisons
  are done and how the Taylor remainder is bounded.

  Searched for 1 pattern, ran 4 shell commands

● I have the full picture now. Here's the tour.

  How the calculation avoids rounding: exact ℚ everywhere, errors paid for by proof

  The computational step (the 40-hour exists_solution_table check and the Checker/ machinery
  behind it) never performs approximate real arithmetic at all. There is no floating point
  anywhere in the trusted path, so there is no rounding to go wrong. Instead, four techniques
  work together:

  1. The checker computes only in ℚ, which is exact

  Checker/Local.lean opens with its design contract: "A computable, pure-ℚ checker… Everything
  here is computable." Rational numbers in Lean are arbitrary-precision integer pairs, so
  decide/native_decide on a ℚ comparison is an exact computation — 355/113 < 22/7 either holds
  or it doesn't, with no representation error. Every quantity in a Row (angles, radii like
  Row.r := r' / 1000, matrix entries) is a literal rational.

  2. Transcendental functions are replaced by polynomial surrogates, with the error bounded
  analytically, once

  sin and cos of a rational are irrational, so the checker never uses them. It uses Taylor
  partial sums instead (RationalApprox/Basic.lean:27):

  def sinℚ {k : Type} [Field k] := sin_psum (k := k) 13   -- x - x³/3! + … + x²⁵/25!

  A polynomial with rational coefficients is exactly computable on ℚ. Two lemmas then connect
  it to the real world:

  - Commutation with casting (sinℚ_match): computing sinℚ in ℚ and casting to ℝ equals
    computing the same polynomial in ℝ — proved by push_cast; rfl. The ℚ→ℝ cast is a ring
    homomorphism, so it loses nothing; this is the only "conversion" step, and it's exact.
    [verified — proof is rfl in source]
  - Distance to the true function (TrigLemmas.lean:129): |Real.sin x - sinℚ x| ≤ κ/7 on
    [-4, 4], from the Lagrange remainder |x|²⁷/27!. This is a theorem about real analysis,
    proved once — not a numerical estimate.

  So instead of "compute sin approximately and hope the rounding is small," the structure is
  "compute a polynomial exactly, and carry a proven bound on its distance from sin."

  3. Square roots are never computed — only one-sided bounds and the squaring trick

  Two complementary tricks handle radicals:

  Directional rational sqrt (Checker/ApproxSqrt.lean): computable sqrtℚLow/sqrtℚUp with
  theorems (sqrtℚLow x)² ≤ x ≤ (sqrtℚUp x)². This is rounding made explicit and one-sided: each
  use site picks the direction that makes its inequality conservative, and the
  LowerSqrt/UpperSqrt structures in RationalApprox/Basic.lean:181 carry the proof obligation in
  their type. (Similarly sqrt_twoℚ := 142/100 is just an upper bound for √2, with
  upper_sqrt_two_gt_sqrt_two as a proof field — nobody needs √2 itself.)

  The squaring trick (sq_trick_sound, SolutionTable/SoundnessStep3.lean on
  feat/fill-computational-step): to certify the real inequality dot > √2·ε + t, the checker
  verifies two pure-ℚ inequalities instead:

  theorem sq_trick_sound (dot t ε : ℚ)
      (hpos : t < dot) (hsq : 2 * ε ^ 2 < (dot - t) ^ 2) :
      (dot : ℝ) > √2 * (ε : ℝ) + (t : ℝ)

  Squaring eliminates the radical entirely; the soundness theorem (closed by nlinarith with
  sq_nonneg and √2² = 2) is proved once, and then every row check is radical-free.
  [verified — no-sorry proof in source]

  4. All residual error is absorbed by strict inequalities with an explicit κ-budget

  The pieces that genuinely can't be exact — real vertices vs. their rational approximations,
  the true rotation matrices vs. rotMℚ_mat — are bounded in operator norm by κ = 10⁻¹⁰
  (κApproxMat, X_difference_norm_bounded, the BoundsKappa* files). The checker then tests
  against inflated thresholds: per the proof-chain comment in SoundnessStep3.lean, the ℚ inner
  products must exceed √2ε + 3κ + (1+κ)κ, not merely √2ε. Soundness lemmas like
  aeq_real_of_aeq_approx_strict then transfer the conclusion from approximate data to the real
  geometry: the verified margin is strictly larger than the worst-case accumulated error.

  The pattern in one sentence

  This is verified interval arithmetic done at the proof level: exact rational computation +
  once-and-for-all analytic error bounds + strict thresholds wide enough to swallow the error
  budget, with exact_mod_cast/push_cast as the lossless bridge from the ℚ world the kernel
  computes in to the ℝ world the theorem lives in. Rounding never "happens" — every place a
  numerical method would round, this development instead either (a) stays exact, (b) makes the
  rounding one-sided and proves it, or (c) pays a κ out of a proven slack budget.

  ---
  Where to next?
  - show proof — walk through sq_trick_sound's nlinarith step or the Lagrange-remainder proof
    of sinℚ_approx
  - go deeper — how sqrtℚLow's fuel-based search (shiftUpAux/shiftDownAux, scaling by 100 to
    keep digit pairs) achieves ~20 digits of guaranteed precision
  - broaden scope — how the κ-budget is allocated across the whole soundness chain
    (BoundsKappa → BoundsKappa4)
  - switch mode — compare with how constructValidTable.lean / the Python verifier do the same
    check executably

✻ Churned for 2m 20s

Noperthedron formalisation, Claude Code (Fable 5), June 2026.

/learn, Socratic mode

❯ show proof socratically

Pedagogy: Switching to Socratic mode on sq_trick_sound — you built this proof's neighborhood, so
I'll start with the question whose answer carries the whole design insight rather than walking the
tactics linearly.

  Here's the statement and the proof we're examining, for reference:

  theorem sq_trick_sound (dot t ε : ℚ)
      (hpos : t < dot) (hsq : 2 * ε ^ 2 < (dot - t) ^ 2) :
      (dot : ℝ) > √2 * (ε : ℝ) + (t : ℝ) := by
    have hpos_r : (t : ℝ) < (dot : ℝ) := by exact_mod_cast hpos
    have hsq_r : 2 * (ε : ℝ) ^ 2 < ((dot : ℝ) - (t : ℝ)) ^ 2 := by exact_mod_cast hsq
    by_contra h'
    push_neg at h'
    nlinarith [sq_nonneg (√2 * (ε : ℝ) - ((dot : ℝ) - (t : ℝ))),
               Real.sq_sqrt (show (2:ℝ) ≥ 0 by norm_num)]

  Abbreviate d := dot − t, so the claim is: from 0 < d and 2ε² < d² in ℚ, conclude d > √2·ε in ℝ.

  First question. The squared inequality 2ε² < d² looks like it carries all the content — squaring
  is where the radical disappears, after all. So why is the hypothesis hpos : t < dot there at all?
  Concretely: can you give values of dot, t, ε where 2ε² < (dot − t)² holds but the conclusion is
  false?

❯ t could be > dot but by more than sqrt(2)epsilon in magnitude

Pedagogy: Answer is correct — I'll anchor it with one concrete instance, then push on the
follow-up they haven't engaged yet, narrowing it to "which two facts must be multiplied" since
that's the heart of the nlinarith certificate.

● Exactly right. Squaring forgets sign: d² > 2ε² only says |d| > √2·|ε|. Concrete witness:
  dot = 0, t = 10, ε = 1 — then 2ε² = 2 < 100 = d², but the conclusion 0 > √2 + 10 is false. So
  hpos is what restores the sign information that squaring destroyed. The checker pays for this:
  it must verify two ℚ inequalities per use, not one.

  Now the follow-up, sharpened. After by_contra; push_neg, the hypothesis set is:

  - hpos_r : 0 < d   (writing d for dot − t)
  - hsq_r : 2ε² < d²
  - h' : d ≤ √2·ε

  Informally you'd say "square both sides of h' to get d² ≤ 2ε², contradiction." But squaring an
  inequality is only valid when both sides are nonnegative — and that's precisely what hpos_r
  rescues, since 0 < d ≤ √2·ε makes both sides positive.

  Here's the question: nlinarith doesn't "square an inequality." All it can do is take products
  of pairs of hypotheses (and the hinted terms) and then look for a linear combination that yields
  False. The hints hand it (√2·ε − d)² ≥ 0 and (√2)² = 2, i.e. after expansion:

      2ε² − 2√2·ε·d + d² ≥ 0

  Which two hypotheses must nlinarith multiply together to finish, and can you write down the
  resulting chain that contradicts hsq_r? (Sanity check for your answer: your chain should visibly
  break at exactly one step if d ≤ 0.)

✻ Churned for 21s

Same session, scroll for the full exchange. The agent answers, anchors with a concrete witness, and hands back a sharper question.

Origin story: de Finetti as a stress test

lean4-skills grew out of a large AI-assisted Lean formalisation of de Finetti’s theorem (exchangeable sequences are conditionally i.i.d.). It stressed agents in exactly the operational ways this talk is about:

• conditional expectation and kernels; σ-algebra bookkeeping;
• product-measure uniqueness; L¹/L² transport;
• Mathlib discovery (much of the work is bridge lemmas to existing API);
• statement drift under pressure to “just close the goal.”

Interfaces as trust boundaries

Three independent routes (reverse-martingale, L²/Stieltjes, Koopman) all had to land on the same intermediate interface: finite conditional factorisation relative to a sub-σ-algebra.

• If a route drifted, it failed to meet the interface: an early, localised signal instead of a silent divergence.
• Missing measurability side conditions had somewhere to fail.
• The final theorem did not rest on three incompatible local stories.

What counts as improvement?

If I change the skill, how do I know the change helped? There is no single number, and the answer is not just “more closed sorries.” It is also:

• fewer statement changes;
• better Mathlib reuse;
• smaller diffs;
• clearer stuck summaries;
• less review burden;
• more human understanding.

/lean4:golf: shortening a proof is a review decision

❯ let's pull the latest from origin and then /golf

● Skill(lean4:golf)   ⎿  Successfully loaded skill
  $ find_golfable.py SpherePacking --recursive --filter-false-positives

  1. APPLY-EXACT-CHAIN [HIGH PRIORITY] (directness)
     File: SpherePacking/MagicFunction/a/Integrability/ComplexIntegrands.lean:82
     Lines: 7 | Benefit: directness | Est. reduction: 30-60%
     Preview:
     |   apply φ₀''_holo.comp
     |   · apply (differentiableOn_const (-1)).div
     |     · rw [differentiableOn_add_const_iff]
     … (similar candidates across 5 files, including HAVE-CALC SINGLE-USE patterns)

● Update(SpherePacking/MagicFunction/a/ContourEndpoints.lean)   ⎿  Added 1 line, removed 6 lines
  508 -      have heq : (36 * phiBounds.C₄ / (π^2 * T^2)) * (1 + T)^2 * Real.exp (2 * π * T) *
  509 -          Real.exp (-π * r * T) =
  510 -          (36 * phiBounds.C₄ / π^2) * ((1 + T)^2 / T^2) *
  511 -          (Real.exp (2 * π * T) * Real.exp (-π * r * T)) := by
  512 -        field_simp
            calc (36 * phiBounds.C₄ / (π^2 * T^2)) * (1 + T)^2 * Real.exp (2 * π * T) *
                     Real.exp (-π * r * T)
                = (36 * phiBounds.C₄ / π^2) * ((1 + T)^2 / T^2) *
  516 -              (Real.exp (2 * π * T) * Real.exp (-π * r * T)) := heq
  505 +              (Real.exp (2 * π * T) * Real.exp (-π * r * T)) := by field_simp

● All three modules build successfully, with no new diagnostics — the sorry warnings are the
  three pre-existing intentional ones in PhiBounds (hφ₀/hφ₂/hφ₄) plus upstream files I didn't touch.

  Golf Results (PR scope: cameronfreer/dz-contour-endpoints)

  Net change: −22 lines (23 insertions, 45 deletions) across the three PR files.

  Meaningful simplifications (directness): 7
  - ComplexIntegrands.lean — both Φ₁'_holo/Φ₃'_holo denominator bullets collapsed from 6-line
    apply/bullet trees to 3-line terms, reusing the file's own differentiableOn_id.add_const/
    .sub_const idiom in place of rw [differentiableOn_add_const_iff].
  - ContourEndpoints.lean — three apply mul_le_mul_of_nonneg_right bullet trees collapsed to
    direct exact terms; the 5-line single-use heq have inlined into its calc step
    (:= by field_simp); the unused-alias have h := hS_bound; rw … at h replaced by rewriting
    hS_bound directly (also removes a semicolon).
  - PhiBounds.lean — hnnonneg/hnnat/hmnnat calc/simp/zify proofs replaced with direct terms
    (Int.natCast_nonneg, Int.toNat_of_nonneg, Int.le_toNat), each verified via lean_multi_attempt
    before applying.

  Performance/determinism cleanups: 4 — two by linarith → term proofs (one_pos.trans_le), two
  rw …; exact → (div_le_one hT_pos).mpr hT (removing existing semicolons), filter_upwards with T;
  exact … → Eventually.of_forall.

  Tactic-block compressions: 2 — the t3 hbound (have/simp only/exact → simpa using), and the
  rw + norm_num + ring volume computation collapsed to one norm_num [Measure.real,
  Real.volume_Icc, mul_comm].

  Skipped: the squeeze_zero'/calc anchors (calc skip rule), the constructor in
  norm_x_add_I_mul_T_bounds (multi-line branches), the final cast step in c_φ₀₂_poly (no clean
  low-ladder one-liner found within probe budget), and the three sorry bounds in PhiBounds
  (nothing to golf).

  Build status: ✓ lake build of all three modules passes; sorry count unchanged.

  Optional next step: /lean4:checkpoint to commit this as a golf pass on the branch.

✻ Cooked for 15m 39s

01:42 AM claude-fable-5
Checkpoint Created

  Commit: d3481cc — golf(MagicFunction/a): collapse apply chains and have-wrappers to direct
    terms (3 files, +23/−45)
  Project build: ✓ passing (3454 jobs)
  Axioms: ✓ all 149 declarations in MagicFunction/a use only standard axioms
  Sorries: 70 project-wide, unchanged by this commit (PhiBounds still has its 3 intentional ones)

Sphere-Packing-Lean, Claude Code (Fable 5), June 2026; cropped: a script emits prioritised candidates with previews; the agent inlines a single-use have and verifies each edit with Lean diagnostics. A shorter proof can be worse; golfing is a win only if it stays at least as direct, clear, and deterministic.

Review can also be a workflow

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

What should become shared infrastructure?

1. Better search and evidence traces: semantic, type-pattern, and local search, verified against Lean before editing.
2. Better review workflows: naming, generality, imports, performance, full Mathlib-style API review.
3. Better shared infrastructure: a host-neutral core, reusable domain skills, realistic shared benchmarks.

From values to mechanisms

The protocol does not guarantee these values; it gives each one a surface where it can be checked, reviewed, or defended.

Which search tool answers which question?

Search is not separate from proving: a search result is only a hypothesis until Lean validates a candidate use.

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

Disclosure as part of the artifact

For AI-assisted formalisation, disclosure should say more than “we used an LLM.” Useful disclosure records:

• which tools generated candidate edits;
• what Lean feedback and search tools were available;
• who chose the statements and interfaces;
• who reviewed and accepted generated changes;
• what builds, sorry checks, and axiom checks were run;
• where the code and toolchain can be reproduced.

A caveat about scope

This talk studies workflow design inside a Lean project. It does not settle broader questions about:

• model training on mathematical texts or formal libraries;
• data consent and licensing;
• access to compute;
• corporate incentives;
• environmental and social costs;
• downstream uses of general-purpose AI.

Build success is not enough

Why A/B testing skill changes is hard

• Model behaviour 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 behaviour 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.

A practical evaluation harness

Evaluation includes responsibility

A run is better only if it improves the whole research artifact:

• Correctness: build, sorries, axioms;
• Intent: statement and interface preserved;
• Attribution: existing Mathlib API found and reused where appropriate;
• Reviewability: the trace explains search, edits, and failures;
• Disclosure: human and tool roles are clear;
• Understanding: the human can explain the next decision.

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.

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)

de Finetti’s theorem

The Lean formalisation 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.
• Formalisation 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 factorisation 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 specialised helper lemmas;
• statement drift: locally convenient but globally wrong interfaces.

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