Lean's Tactic Language Is Smaller Than It Looks

The folklore problem

Ask around about applying formal-grammar constraints to theorem provers and you'll hear the same objection: proof-assistant tactic languages are programming languages — unbounded, dynamically extensible, full of arbitrary term syntax. You can't write a grammar for that. And even if you could, it would have thousands of productions and wouldn't be useful for anything.

This objection sounds right and is almost exactly backwards. The question was never "how big is Lean's grammar?" (infinite — it's a macro language with a metaprogramming escape hatch, by design). The question is: how big is the subset of Lean's tactic language that people actually use? That's an empirical question, and empiricism is cheap: Mathlib is public, it's huge, and it's written by the most expert tactic users on earth.

So we built a context-free grammar for the Lean 4 tactic sublanguage from scratch, measured it against every tactic line in all of Mathlib, and then checked whether the same methodology transfers to other proof assistants. This post is about what the corpus taught us. (A companion post applies this grammar as a decoder constraint and measures what happens; this one is about its construction and comprehensiveness.)

The design: copy Lean's own parser, not a textbook

Before writing a single production, there was a design decision to make, and Lean itself made it for us. Lean 4's tactic parser is keyword-dispatched: the parser looks at the leading identifier of each command and hands off to that tactic's own syntax declaration (rw goes one way, simp another). Everything after the keyword is mostly arbitrary term syntax — hypotheses, lemma names, using clauses — which no context-free grammar can meaningfully resolve, because terms aren't parsed in isolation; they're elaborated against the proof state (unification, typeclass synthesis, implicit arguments). Term syntax isn't context-free, and pretending otherwise would produce a grammar that's simultaneously enormous and wrong.

So the faithful move is to mirror Lean's dispatch structure rather than model the whole language:

• Shape: every production is KEYWORD ARGS — named productions carry explicit shape where a tactic has fixed syntax (rfl takes nothing, simp takes optional args, convert! requires them), and everything else falls into ARGS, a permissive catch-all ≈ rest-of-line. Permissiveness here is principled, not laziness: term-level content will be judged by the elaborator anyway, and a tactic grammar's job is only to route on the keyword and confirm the shape.
• Recursion exactly where nesting actually occurs. Scan real proofs and tactic-level recursion happens in precisely two places — · focus bullets and | pattern => tac case arms inside induction ... with. Two recursive productions (focus_tac, case_arm_tac); everything else is flat. A grammar textbook would give you a dozen nesting constructs; the corpus gives you two.
• A generic IDENT ARGS? catch-all as final alternative, lowest priority. This mirrors a design fact about Lean itself: the tactic namespace is user-extensible via macros. No fixed grammar can enumerate all keywords that might exist in some file importing some library — so unknown keywords fall through gracefully instead of failing. The catch-all isn't a hole in the grammar; it's the grammar's model of extensibility.

This design descended from an original architecture thesis about LLM proving pipelines (§10.1 of that document sketched exactly this KEYWORD ARGS shape); what we did next was test whether it survives contact with the entire corpus.

Counting is harder than it looks: two extraction bugs

First you need the corpus: every real tactic line in Mathlib. Shallow-cloned leanprover-community/mathlib4 in full — 8,302 files, 464,950 lines — and wrote an extractor to pull out logical tactic lines.

The naive version fails invisibly. Tactics wrap across physical lines, so you need continuation merging. The obvious rule — merge lines with unbalanced brackets — sounds fine and is wrong. When we ran it, our first full-corpus pass reported a pile of parse failures; hand-auditing them showed 51% were not grammar gaps at all but artificial line-splits: continuations like

  rw [mul_comm]
    (by norm_num)

where the second line has no unclosed bracket but is still part of the same tactic under Lean's actual indentation rule (colGt). Bracket balance is one continuation mechanism; indentation-awareness is a second, independent one. You need both. Fixing the merger collapsed the candidate set from an inflated ~229,560 lines to 144,154 genuinely distinct logical tactic lines.

The second bug was real too, and more interesting: 36% of early failures traced to a single missing production — | pattern => tac case arms inside match/induction ... with. One recursive production (case_arm_tac) eliminated them wholesale. Iterating against failure buckets, rather than guessing at tactics in the abstract, turned out to be the whole game: each round of hand-auditing what actually failed bought far more coverage than any amount of upfront language theory.

Fifty-three productions

The design above, iterated against real failure buckets until it stopped improving, produced a grammar small enough to print on one screen: 53 named productions plus the catch-all and the two recursive forms. Measured against the full corrected corpus:

Every one of the 205 residual failures was hand-audited. Not one was a missing tactic keyword. They split into known extraction edge cases (48 lone · bullets with nothing on their merged line, 45 anonymous-constructor literals in term mode, 26 compiler directives like #adaptation_note, 15 docstring fragments that leaked past comment-stripping) plus a miscellaneous tail. Structural coverage: 99.86% of everything Mathlib writes, with 53 productions.

Three more measurements, because one isn't evidence

A single number from a single script written by its own author is a demo, not a finding. So we triangulated the underlying claim — that tactic usage is extraordinarily concentrated — four independent ways:

Four measurements, three methodologies, tight agreement. Concentration isn't an artifact of our extractor; it's a property of the ecosystem.

And does the grammar generalize beyond human-written code to model output? We took 14 real theorem statements, asked a frontier model for first tactics, and classified: 93% named, 7% fallback, zero outside the grammar. Consistent with the human baseline (small n, no significance claimed — but no divergence either).

The inversion: when you find a gap, grow the language, not the grammar

Traditional constrained-decoding wisdom says: found a tactic your grammar can't express? Add productions until it can. There's an inversion worth considering, because Lean makes it unusually cheap: add a macro instead.

macro "solve_positivity" : tactic => `(tactic| positivity)
macro "discharge_linear" e1:term:max e2:term:max : tactic =>
  `(tactic| linarith [$e1, $e2])

One line moves positivity or a curried linarith call inside the grammar's keyword-dispatch world forever, verified at parse time by the real elaborator. We compiled a bridge suite against genuine from-source-built Mathlib tactics (exit code 0 across positivity, gcongr, nested-focus cases), and caught a real language lesson doing it: bare two-term macro arguments greedily swallow application syntax — combine_facts hp hq parses as one term, hp applied to hq — and the fix is precedence annotations (term:max) per slot. The compiler's error (Function expected at hp) pinpointed it immediately. Write macros with explicit precedence or they will lie to you.

This reframes grammar maintenance: rare-but-real tactics don't need new productions, they need a one-time, kernel-checked promotion into keyword form. Whether that's cleaner than growing the grammar is a taste decision; that it's available changes the maintenance math.

Does this transfer? Two other proof assistants say yes

If concentration were a Lean quirk it would still be interesting but narrower, so we reran the methodology elsewhere — briefly, because the results don't need much space.

Rocq (Coq): math-comp, 147 files, 150k lines, extracted via Rocq's literal Proof./Qed. delimiters (a more reliable boundary than Lean's inferred indentation blocks). Top-20 leading tokens covered 98.0% of 74,370 tactic units — more concentrated than Lean, plausibly because SSReflect's design philosophy is a narrow core tactic set carrying rich inline modifiers — and a 27-production grammar scored 98.81% on its very first pass, versus Lean's 73.8% first pass. One bonus finding from building tooling on both: Rocq's Tactic Notation argument kinds (constr(e1), ident(x)) explicitly delimit each slot as its own nonterminal, so the macro-argument greediness bug described above simply cannot occur there.

Isabelle: the kernel build was blocked for us (its component repository was unreachable), but the grammar work proceeded against real AFP source with position-based proof/qed nesting extraction: 95.47%, 26 productions — lower for a diagnosed reason (a third continuation mechanism, wrapped fact-reference lists like using X[of ...], same lesson class as Lean's colGt fix, not yet applied). This also corrected our own starting misconception: Isar's core proof language has an explicitly documented grammar; it is not somehow less grammar-tractable than its peers.

Three systems, one methodology, same shape of answer: tactic usage concentrates hard everywhere we looked.

What coverage does not tell you

One caveat before anyone runs off citing 99.86%, and it's the reason this post ends where it does.

Coverage of real text is not constraint strength. Our grammar achieves 99.86% because it is permissive by design — the catch-all admits essentially anything identifier-led, and ARGS swallows arbitrary terms. Accepting nearly everything real mathematicians wrote says little about how much garbage it rejects. Those are different measurements, and the second one is what matters if you want to put the grammar in a decoder's sampling loop as a logit mask.

We did exactly that. Results — including what fraction of a modern model's tokens die at the parser without the mask, what happens to hallucinated lemma names (spoiler: nothing good, and instructively so), and two infrastructure bugs that silently unmask "constrained" decoding — are in the companion post.

Artifacts: grammar definition, extractor, per-line classifications, and the full failure audit available alongside the companion post. Corpus: mathlib4 @ current master, batteries, math-comp, AFP excerpts.

If you build on this, I'd love to hear about it — sngugi.research@gmail.com.