THE CONTROLLED TACTIC TABLE

same goal, ten tactics, axioms recorded per cell

Every observational measure in this program has the same weakness: a theorem's classical dependence can come from what it says or from how it was proved, and a census cannot tell you which. This is the intervention that can. The goal is held fixed, the tactic varies, and anything that changes between cells is the tactic's doing.

The result is a boundary rather than a gradient. norm_num introduces the axiom of choice on all 15 order goals (≤, <, ≥ over Nat and Int) and on none of the 12 equality and divisibility goals. On the same 27 goals decide, omega and trivial introduce it nowhere, so no goal here ever required it.

Measured with gonzalgo · Lean 4.32.1 with Mathlib v4.32.1 · 9 goal families × 3 goals × 10 tactics = 270 cells, every cell a separate theorem with its own #print axioms

closed is false where the tactic did not prove the goal. Lean records those as depending on sorryAx, which is the tactic failing rather than a proof resting on something unfinished, so they are excluded from every rate below — a tactic that never ran cannot have introduced an axiom. classical means Classical.choice appears in the cell's axiom set.

Get the data

controlled-tactics.json · controlled-tactics.csv · CC-BY-4.0 · version 2026-08-12

One of the gonzalgo indexes — standing measurements of what formal libraries rest on, remeasured as the libraries move.

Reproduce it

lake env lean -D maxErrors=4000 lean/Controlled.lean

set_option maxErrors inside the file is ignored; only the command-line flag works, and without it Lean halts at 100 errors long before the last theorem. The generator and the raw output are in 10.5281/zenodo.21883963.

Rates, over goals each tactic actually closed

What the boundary means

norm_num's dependence is not a property of the arithmetic. The same numbers, stated as an equality, come out choice-free from the same tactic. It is the order goals specifically, and on Nat and Int the constructive decidability instance exists and is axiom-free, so the classical route was taken where a free one was available.

grind is classical on every goal it closes and that is not a defect: it is architecturally classical. Reporting it beside norm_num without that distinction is exactly the error the attribution paper is about — a rate cannot separate a tactic that is designed classical from one that reached for choice unnecessarily.

aesop and simp agree on all 27 goals, cell for cell. aesop's classical cells are simp's classical cells. A search procedure built over a simp set inherits that set's axiom behaviour rather than adding to it.

Why this is worth more than the census

Per-tactic rates measured across a library vary as much within a library as between them — 5.8–28.2% in Mathlib, 45–100% in Lean core — because eligibility is a property of the theorem while the defect is a property of the proof term. Fixing the goal removes that confound entirely. Every difference in this table is attributable, because nothing else was allowed to vary.