THE CLEANABLE TABLE

the declarations whose dependence on choice actually came out

275 declarations across 60 modules were rewritten to remove a dependence on the axiom of choice, and the Lean kernel accepted every one. Four were refused and one kept its dependence. This is the list.

The unit is a compiler-generated _proof_N term rather than a lemma anyone wrote, and that is the finding rather than a caveat. The removable dependence in these libraries sits in terms the elaborator emitted, so it comes out by changing the tactic that emits them and not by editing a proof.

Measured with gonzalgo · Lean 4.32.1 with Mathlib v4.32.1 · every rewrite checked by the Lean kernel, not the elaborator

occurrences is how many uses of Classical.propDecidable the generated term carried. outcome is removed where the kernel accepted the rewritten term, kernel rejected where it refused, and still classical where the rewrite left the dependence in place. The full data carries the generated term's name and, for the four refusals, the kernel's message verbatim.

Get the data

cleanable.json · cleanable.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/Substitute.lean

ConstantInfo.value? must be passed allowOpaque := true or theorem proof terms read as empty and every occurrence count comes back zero. Method: 10.5281/zenodo.21769846.

Where it lives

The distribution is the useful part: Init 223, Std 41, Mathlib 9, Batteries 3, Lean 3, Plausible 1. Four fifths of the removable classical dependence in this measurement is in Lean core, and only nine declarations are in Mathlib.

That matters for what anyone can do about it. Lean core's position on the tactic behaviour behind most of these is on record: avoiding choice is a deliberate non-goal there, stated in response to the omega report and without disputing any figure. So the largest share of what is removable sits where removal is not wanted, and the share sitting where it might be welcomed is small.

The four the kernel refused

Every refusal is a type mismatch rather than a timeout or a missing instance: the substituted term elaborated and then failed to check. Those are the interesting ones, because they are cases where a Decidable instance exists and is still not interchangeable with the classical one at the point it is used. The kernel's message is carried verbatim in the data for each.

What this is not

It is not a claim that 275 theorems were made constructive. Removing a use of Classical.propDecidable from a generated term removes one route to the axiom; whether the declaration still reaches choice by another route is a separate question this table does not answer. The Dominator Table is where routes are counted.