Sorries and assumptions🔗

Everything in the library that is incomplete or rests on an assumption beyond the three axioms every classical Lean development uses (Classical.choice, propext, Quot.sound). This is the referee's checklist, and it reports only what is missing: nothing here is a measure of how far the library has got.

No declaration depends on a sorry.

No declaration rests on an axiom beyond the ordinary three.

What it rests on

Nothing above this point leaves the project, and most of what lies beyond it needs no trust: upstream proofs were rechecked by the kernel, and anything left unproved in one arrives here as a sorry or an extra axiom — both already counted above, upstream included.

What does not come for free is an upstream definition that a statement is about. A theorem mentioning a definition from another package means what it means only if that definition is the intended one, and no proof settles that — nothing below the statement can, because it is the statement that names it. So what follows counts statements, not proofs.

The graph is the dependency order: the toolchain at the top, this project at the bottom, an edge from each package to the one that requires it.

No upstream package is unaudited: every one of the 8 was passed to --trust.