From Prompts to Protocols: lean4-skills for AI-Assisted Lean Formalization

Q&A What to build next: better detectives, one court of appeal

Three open interfaces: external reasoners behind a certification boundary, a persistent checked state that many agents can share, and evaluation beyond kernel acceptance.

Conjecturing numbers: Jakubův, Olšák, Suda, Urban, Neural Conjecturing for Saturation Theorem Provers, AITP 2026 (3,161 Mizar40 problems, 122,356 evaluated cuts; architectures coded with Codex).

opt N Three ways “verified” can still be inadequate

checked ≠ intended

A checker accepts what the environment encodes, not what you meant. An agent can satisfy it by quietly inventing the theory it needs, even a false axiom. The fix is a contract, not a weaker model: preserve the theory; fill this proof.

provable ≠ useful

Neurally generated lemmas for a saturation prover: about 61% provable, only 5–6% actually speed up the search (largest reduction 77×). Which true intermediate claim is worth saying now?

correct ≠ good

Kernel acceptance is a binary floor; quality is multidimensional: right statement and hypotheses, library reuse, readability, small imports, and can the human explain what the agent did?

So measure more than completion: did the interaction sharpen a definition or conjecture? find revealing counterexamples or missing hypotheses? leave reusable API? leave the human able to explain, audit, and continue?

The strongest public evidence is still about formalization and proof quality. The missing evidence for the fourth role is a public case study where Lean-backed interaction changes the mathematics being discovered. That is the next experiment.

Koepke & Wirtz, Naproche Natural Language Formalizations with LLMs; Jakubův, Olšák, Suda, Urban, Neural Conjecturing for Saturation Theorem Provers, both AITP 2026.

opt J Fences, not sandboxes (and not guardrails)

Guardrails and sandboxes assume the agent will wander: narrow the scope, ration the context, wall off every action. Cheap capability is spent making the agent do less.

A fence is a written rule that a capable agent will read and respect. The question stops being “how do we keep it safe?” and becomes “how do we tell it what we want?”: its role, the workflow, what may change, what counts as done.

Statement fence

the theorem does not change silently; changing it is a human decision

Epistemic fence

only Lean-checked claims get a certified verdict; uncertainty is labelled, never hidden

Operational fence

permissions, budgets, checkpoints, axiom and import gates, stop conditions

Once the fence is text, you can ask for more: a skeptic attacking a definition overnight; many agents on one blueprint, checkpoints as the coordination.

And Lean is not only the fence. It is laboratory equipment: a failed elaboration exposes a missing hypothesis; a finite model kills a conjecture; an awkward formalization reveals the wrong definition.

Steve Yegge, Fences, not Sandboxes (2026): a capable agent “just needs to be told what you want: its role in the moment.”

opt K Open-ended mathematics with Lean in the loop

Formal feedback can change the question, not merely certify the answer.

The statement need not be fixed at the start; a counterexample may be the most useful result; an awkward proof may expose the missing abstraction, and not every true claim is worth saying now. Trustworthy means conjectures, evidence, failures, and certified claims stay distinguishable.

Current working practice and a research direction, not yet a public case study. Where it pays: heavy bookkeeping, long chains of small lemmas, definitions still being chosen: the projects on slide 3.

opt L When agents are cheap and plentiful, spend them on diversity

Scout

searches libraries, tools, analogies

Builder

formalizes the surviving branch

Skeptic

attacks claims and definitions; hunts counterexamples

Referee

target fidelity; proof gap vs. false claim; quality

Teacher

explains; diagnoses what human or agent misunderstood

All around one shared Lean repository: checked state, a blueprint, CI-gated handoffs, and a human editor who owns meaning and decides which questions matter.

Parallelism should buy different questions, not twenty copies of one attempt.

Five agreeing agents are not a proof. Five agents producing independently checkable artifacts may be useful. Overnight autonomous runs with obstruction reports as the morning’s reading; roadmaps executed by many hands.

opt M Independent evidence

Used lean4-skills directly

Agentic Proving for Program Verification

Claude Code + lean4-skills on CLEVER: 98.1% end-to-end on entries with self-consistent premises; diagnosed defects in the benchmark itself. Sosso, Arora, Spitters · ICLR 2026 workshop · here on Tuesday

Ramanujan–Nagell · QFT · Numina-Lean-Agent

number theory, physics, and an open agentic reasoning system use the same protocol layer. Banwait 2026 · Douglas, Hoback, Mei, Nissim 2026 · Project Numina

Independent convergence: not users of the package

LeanMarathon

parallel recoverable transactions over an evolving blueprint: 258 lemmas toward seven targets, no sorry. Zhang, Sun, Suzuki, Lee, Liu 2026

Proof-Refactor

generated proofs refactored into modular artifacts, scored by rubric and readability, against a strong Claude Code baseline. Fu, Liu, Wang, Yuan 2026

opt O Parallel exploration over shared formal state

Around a shared Lean state: scouts propose competing definitions and analogies; builders formalize the promising branches; skeptics attack them; referees compare evidence and target fidelity; teachers explain what was learned. The human chooses which questions matter.

Parallelism supplies competing hypotheses; Lean makes their evidence comparable.

statement fence

no theorem changes silently; changing one is a human decision

evidence labels

certified, uncertified, and speculative claims never mix in the record

checked handoffs

budgets, checkpointed builds, obstruction reports between agents

“Fences, not sandboxes”: Steve Yegge, 2026: a capable agent “just needs to be told what you want: its role in the moment.”

opt P Current evidence and the next experiment

Completion is measurable today; mathematical contribution is the open evaluation problem.

CLEVER: Sosso, Arora, Spitters, ICLR 2026 workshop; here on Tuesday; tested Claude Code, while my current work relies at least as much on Codex. Lemma-usefulness numbers: Jakubův, Olšák, Suda, Urban, AITP 2026.

opt A The FLoC arc slide (three stages), for comparison with slide 3

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

opt I A checker accepts what the environment encodes, not what you meant

Axiom. Assume a < n and n*q = a*b and b is positive.
Then n-a | a*(b-q) and b-q is positive and a*(b-q) < a*b.

Verification answers the question encoded by the current environment. Protocols preserve the question the human actually meant.

Koepke & Wirtz, Naproche Natural Language Formalizations with LLMs, AITP 2026. Compare the statement fence and the axiom gate on slide 6.

opt B Every failure mode gets a mechanism and leaves evidence

opt C Where trust actually resides

The same checkpoints that keep a formalization reviewable are what make an exploration trustworthy.

opt D Different questions need different searches

opt E 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.

opt F Commands differ in autonomy, permissions, and stop conditions

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

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