lean4-skills: Workflows for AI-Assisted Lean Development

Shared infrastructure for Lean agents

lean4-skills makes capable Lean agents easier to steer, inspect, and review.

Coding agents are already capable Lean copilots.

But using one well on a large formalization requires practical knowledge too, and that knowledge is shareable:

• Write down what to repeat and what to avoid. Exact API patterns, elaborator failure modes, disclosed when relevant.
• Make common workflows explicit. Commands, subagents, hooks, and scripts, with real boundaries.
• Give the agent an InfoView and Mathlib search. Goal states, diagnostics, hovers, and multi-attempt testing come from Lean; Loogle, LeanSearch, and LeanFinder search Mathlib. Both reach the agent over lean-lsp-mcp.

As coding agents (model + harness) have improved, the role of lean4-skills has changed

Which aspects matter next?
One direction: trustworthy thought partners via Lean + coding agents.

Contents

1. de Finetti in Lean
2. What can go wrong
3. Search and Lean feedback
4. The workflow layer

de Finetti–Ryll-Nardzewski in Lean 4

lean4-skills began in October 2025 as a personal reference file: notes to reinforce the good patterns and ward off the antipatterns encountered while formalizing de Finetti’s theorem in the exchangeability project.

That project’s headline theorem states that an infinite exchangeable sequence is conditionally i.i.d.:

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

Exchangeable μ X says the joint law of X is invariant under finite permutations of the indices.
Contractable μ X says the joint law is invariant under deleting terms: any m indices, taken in increasing order, have the same law as the first m.

The hard engineering was getting the intended MeasurableSpace, Measure.trim, conditional-expectation, and conditional-independence APIs to elaborate together.

Why 2.5 pages became a large Lean development

~2.5 pp (Kallenberg)  →  42,745 lines · 112 files (ITP artifact)  →  26,767 lines · 105 files (main, 2026-05-27)

Why so long: much of it is transitive dependencies not in Mathlib that needed to be built: reverse martingale convergence, upcrossings, tail and shift σ-algebras, conditional independence, product-measure uniqueness, L¹/L² transport.

• What was not needed: first-pass exploratory proofs, scaffolding, and helper lemmas that existed only because Mathlib was being used suboptimally, as the ITP reviewers pointed out.
• What changed: fixing the Mathlib usage left whole helpers dead, so much of the cleanup was deleting declarations rather than compressing proofs.

theorem exchangeable_iff_conditionallyIID
    [StandardBorelSpace α] [Nonempty α] {μ : Measure Ω} [IsFiniteMeasure μ]
    {X : ℕ → Ω → α} (hX_meas : ∀ n, Measurable (X n)) :
    Exchangeable μ X ↔ ConditionallyIID μ X

‹_› takes any term of the right type, not the one you meant

lemma condExp_mul_pullout [IsFiniteMeasure μ]
    {m : MeasurableSpace Ω} (hm : m ≤ ‹_›) ...

typeclass instance problem is stuck
  IsFiniteMeasure ?m.104

‹_› is local-context lookup, not typeclass search: it asks for any term of type MeasurableSpace Ω, and m qualified. The sub-σ-algebra hypothesis silently became hm : m ≤ m. The stuck IsFiniteMeasure ?m.104 was the downstream symptom.

lemma condExp_mul_pullout {Ω : Type*} {m₀ : MeasurableSpace Ω} {μ : Measure Ω}
    [IsFiniteMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ m₀) ...
  haveI : SigmaFinite (μ.trim hm) := sigmaFinite_trim μ hm
-- several MeasurableSpace Ω in scope: name the ambient m₀ explicitly; avoid ‹_›

Historical incident, 2025: exchangeability c223a5f, the last of four sorries fixed in the 3f5d34e series.

The fix above is shortened from that diff.

The rule that lasted: name the ambient m₀.

The original diff also installed IsFiniteMeasure (μ.trim hm) explicitly. Mathlib had supplied that instance for years, so the line was redundant and later came out (8cf4350); current code writes haveI : SigmaFinite (μ.trim hm) := inferInstance.

A captured instance drifts from the ambient one

A different failure than ‹_›: there the wrong structure was selected outright; here a local definition captured the right structure, and later elaboration expected another.

set mη := MeasurableSpace.comap η inferInstance

hη ht has type      @MeasurableSet Ω inst✝⁶ (η ⁻¹' t)
but expected        @MeasurableSet Ω inferInstance (η ⁻¹' t)

inst✝⁶ is the ambient [MeasurableSpace Ω] binder: anonymous, so Lean prints inst✝ and numbers it by position. The numeral locates a term; it never names a structure.

set installs nothing. Two elaborations produced ambient terms that were not definitionally equal, so the set-bound inferInstance stopped matching. Again: name the ambient, pass it explicitly.

let mΩ : MeasurableSpace Ω := ‹MeasurableSpace Ω›   -- plain let, not letI/haveI
have hmη_le : MeasurableSpace.comap η mγ ≤ mΩ := by
  intro s hs; rcases hs with ⟨t, ht, rfl⟩
  exact (hη ht : @MeasurableSet Ω mΩ (η ⁻¹' t))

lean4-skills references/measure-theory.md, “The inferInstance Drift Trap”, which resolved the instance-synthesis failures in a ~150-line conditional-expectation proof; making ambient facts explicit took type unification from 500k+ heartbeats to normal elaboration.

Predictable failures without guardrails

Recurring pain points, and the rules they became

The rules that generalize beyond measure theory

Ask Mathlib for the property you actually need

This goal is a Mathlib lemma: conditional expectation has the same integral as f over every m-measurable set. It does not need proving, it needs finding.

The agent was instead proving a stronger a.e. identity between the two functions. Saying the property in words returns the lemma on the first search.

Goal
  hm : m ≤ m₀     hf : Integrable f μ     hs : MeasurableSet[m] s
  ⊢ ∫ x in s, μ[f | m] x ∂μ = ∫ x in s, f x ∂μ

lean_leanfinder("conditional expectation has the same integral on an m-measurable set")
  → MeasureTheory.setIntegral_condExp

hover
  (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)] (hf : Integrable f μ) (hs : MeasurableSet[m] s)

lean_multi_attempt
  exact setIntegral_condExp hm hf hs   ✓

Reconstructed interaction; the goal and the setIntegral_condExp signature are exact, current Mathlib. The agent gets the human InfoView loop (goal, hover, diagnostics, tactic tests) through lean-lsp-mcp.

Finding the lemma is the easy half

The tower property: for m₁ ≤ m₂ ≤ m₀, conditioning twice is conditioning once on the smaller. A guess at the name finds it in Mathlib immediately; the previous slide got there by describing the property instead.

Goal
  m₁ m₂ m₀ : MeasurableSpace Ω     hm₁₂ : m₁ ≤ m₂     hm₂ : m₂ ≤ m₀
  ⊢ μ[μ[f | m₂] | m₁] =ᵐ[μ] μ[f | m₁]

lean_local_search("condExp_condExp")
  → MeasureTheory.condExp_condExp_of_le

hover
  (hm₁₂ : m₁ ≤ m₂) (hm₂ : m₂ ≤ m₀) [SigmaFinite (μ.trim hm₂)]

lean_multi_attempt
  exact MeasureTheory.condExp_condExp_of_le hm₁₂ hm₂   ✓

the neighbouring API the goal keeps needing:
  #check MeasureTheory.stronglyMeasurable_condExp    -- μ[f|m] is StronglyMeasurable[m]
  #check MeasureTheory.setIntegral_condExp           -- the defining projection property
  #check MeasureTheory.condExp_condExp_of_le         -- the tower property

Reconstructed interaction; signature exact, current Mathlib. Alternative route via condExp_of_stronglyMeasurable also needs Integrable (from integrable_condExp); the tower lemma is the direct path.

Sometimes the search is for a construction, not a lemma

Kallenberg’s statement quantifies over a random measure ν: conditionally on ν, the X n are i.i.d. with law ν. Nothing in Mathlib is that object, and no name search will find it.

noncomputable def directingMeasure
    (X : ℕ → Ω → α) (hX : ∀ n, Measurable (X n)) (ω : Ω) : Measure α :=
  (ProbabilityTheory.condExpKernel μ (tailSigma X) ω).map (X 0)

#check ProbabilityTheory.condExp_ae_eq_integral_condExpKernel
  -- μ[f | m] =ᵐ[μ] fun ω ↦ ∫ y, f y ∂(condExpKernel μ m ω)

What Mathlib does have is condExpKernel, the conditional distribution given a σ-algebra. It lives on the sample space Ω, so Measure.map (X 0) pushes it to the state space α, where ν belongs.

Two consequences. The agent has to assemble the definition from pieces it can find, rather than retrieve one lemma. And this construction explains the [StandardBorelSpace Ω] assumption in the original implementation; measurability of the pushed-forward family and the statement itself also involve [StandardBorelSpace α].

exchangeability ViaMartingale/DirectingMeasure.lean:53, abridged binders. ConditionallyIID packages the kernel data as a measurable family ν : Ω → Measure α; the martingale route constructs ν exactly this way.

No edit until Lean has checked the candidate

One goal, start to finish. Every step leaves a record: the query, the candidates and their verdicts, the diagnostics after the edit, the diff.

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

And the library lemma is not just shorter: the proof now rests on an interface Mathlib maintains, reviews, and keeps working across versions, instead of a hand-rolled induction that only this file understands.

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

Search Mathlib to reuse its API, not just to save time

-- bespoke induction / adapter
have hcard : s.card ≤ t.card := by
  -- 15 lines

-- Mathlib’s own lemma, used directly
exact Finset.card_le_card h
-- 1 line

Different questions need different searches

When one search mode fails, another finds it

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.

From repeated failures to measure-theory.md

• m ≤ ‹_›: the wrong ambient instance
• set … comap … inferInstance: instance drift and 500k-heartbeat unification
• right theorem, unread hover: the hidden [SigmaFinite (μ.trim hm)] blocks it

The countermeasures, as Lean actions:

• name the ambient m₀ explicitly
• @MeasurableSet with the intended structure
• read the hover; #check the signature
• test with lean_multi_attempt

Each failure that recurred became an exact rule in references/measure-theory.md. The core skill routes the agent there when the task calls for it; the document is not carried in every prompt.

Incidents become guidance at different layers

reference   references/measure-theory.md, typeclasses.md, performance.md …
workflow    commands/draft · formalize · prove · autoprove · review · refactor · golf · checkpoint
            + subagents, hooks, and scripts around the cycle engine
tooling     lean_goal · hover · lean_loogle · lean_leansearch · lean_multi_attempt

• m ≤ ‹MeasurableSpace Ω› became m ≤ m → domain reference: name the ambient m₀
• a candidate hid [SigmaFinite (μ.trim hm)] → read the hover, then test the exact application
• the agent proposed another hypothesis → the /prove header fence, and hand off to /formalize
• the same blocker recurred → stuck report, review, replan

Progressive disclosure: nothing is pasted into every prompt. The core holds invariants and a map; /prove brings its own contract; measure-theory.md is read on demand when the task reaches measure theory; Lean supplies goal, hover, and diagnostics on demand.

Stored advice says what to inspect. Only Lean says what is true here.

The protocol layer, and what stays outside it

The layer shapes what the agent does, not what Lean reports. Lean stays external and authoritative.

Commands are not prompt text: they differ in permissions, budgets, and stop behavior.

Commands differ in autonomy, permissions, and stop conditions

Inside one /prove cycle: the work loop

Bounded by max cycles and a wall-clock budget checked between cycles (a review gate, not a hard process timeout). “Stuck” is a first-class outcome with its own report.

The work loop sits inside a bounded cycle

/prove owns the proof body, not the proposition

 theorem target
     {m : MeasurableSpace Ω} (hm : m ≤ m₀)
+    [SigmaFinite μ]                        -- rejected in /prove mode
     ... := by

prove      reject the header diff; report why the hypothesis seemed needed
formalize  statement changes go here, with human approval

A changed binder, hypothesis, or result type is not proof progress. It is a new formalization decision. In deep mode the literal header (theorem … := by) is snapshotted at entry and any change rolls the cycle back; on the fast path it is a workflow constraint checked in the diff. Imports and outer-scope instance edits sit outside the snapshot, so they stay diff-review concerns.

/prove is allowed to fail

status: STUCK
goal:   ⊢ ∫ x in s, μ[f | m] x ∂μ = ∫ x in s, f x ∂μ
diagnostics: failed to synthesize SigmaFinite (μ.trim hm)
searched:
  setIntegral_condExp · "integral of conditional expectation on a measurable set"
tested:
  exact setIntegral_condExp hm hf hs       ✗ instance
  simpa using setIntegral_condExp hm hf hs ✗ same
obstruction: missing SigmaFinite instance for the trimmed measure
next: check whether [IsFiniteMeasure μ] is in scope, then
      haveI : SigmaFinite (μ.trim hm) := inferInstance

Illustrative report in prove.md’s format, reconstructed from the set-integral search episode earlier in the deck; the state before supplying the trimmed-measure instance.

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

/learn: teach the material, catch up on a session, or talk informally with Lean under the hood

❯ show proof socratically

Pedagogy: Switching to Socratic mode on sq_trick_sound — I'll start with the question whose
answer carries the whole design insight rather than walking the tactics linearly.

  theorem sq_trick_sound (dot t ε : ℚ)
      (hpos : t < dot) (hsq : 2 * ε ^ 2 < (dot - t) ^ 2) :
      (dot : ℝ) > √2 * (ε : ℝ) + (t : ℝ) := by
    …  by_contra; push_neg; nlinarith [sq_nonneg (√2·ε − d), Real.sq_sqrt …]

  First question. Squaring is where the radical disappears — so why is
  hpos : t < dot there at all? Can you give values where 2ε² < (dot − t)² holds
  but the conclusion is false?

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

● Exactly right. Squaring forgets sign: d² > 2ε² only says |d| > √2·|ε|. Concrete witness:
  dot = 0, t = 10, ε = 1 — then 2ε² = 2 < 100 = d², but 0 > √2 + 10 is false. So hpos is
  what restores the sign information that squaring destroyed.

…  the exchange continues: which two hypotheses nlinarith must multiply, and why the
   chain breaks when d ≤ 0

✻ Churned for 21s

Live session, Noperthedron project, June 2026, trimmed; pedagogy mode by Romir Patel.

/disprove: search broadly, certify only in Lean

Its own workflow, not a fallback: test a conjecture, check a generalization, turn a solver’s guess into a checked artifact. The target is never weakened.

theorem smt_bad : ∀ x y : ℤ,
    2 * x ^ 2 - 3 * y ^ 2 ≠ 5 := by sorry

decide      not applicable (infinite domain)
omega       nonlinear
enumerate   one-dimensional only
external/Z3 sat: x = -4, y = 3   [untrusted]

theorem T_counterexample : ∃ x y : ℤ,
    2 * x ^ 2 - 3 * y ^ 2 = 5 :=
  ⟨-4, 3, by norm_num⟩

checked wrapper  ¬ TARGET     ✓
lake env lean    typechecks   ✓
axiom gate       whitelist    ✓
REFUTED

The search may be heuristic or external; the verdict may not be. REFUTED needs a closed Lean term of ¬ TARGET past the axiom gate; otherwise WITNESS_UNCERTIFIED or INCONCLUSIVE.

The counterexample is appended as a separate artifact. Janko Ondras, AI4Math @ ICML 2026; PR #134.

Every failure mode gets a mechanism and leaves evidence

Evaluate more than correctness and speed

Correctness and speed are the easy measurements. API quality, maintainability, and whether a reviewer can follow what happened show up across weeks and projects, not in one file’s sorry count.

A benchmark that scores only the bottom band can rank a lucky, unreviewable proof above a stopped run with a good obstruction report.