Interface Assumptions Are Not Mathematical Assumptions: An Axiom Census of Five Libraries Across Four Proof Systems

Abstract

A formal library's axiom count is routinely reported as a single number. This paper argues that the number conflates two populations which behave differently and answer different questions, and that the conflation is only visible from outside a single library. Five libraries are censused across four proof systems — the Rocq standard library, Rocq's Corelib, Mathematical Components, the Agda standard library, and the Isabelle Archive of Formal Proofs — with one source-level instrument requiring no build. Rocq's Corelib declares five times as many axioms as the Rocq standard library and assumes less mathematics than any library measured: all 73 of its axioms specify primitive machine arithmetic, native arrays, floats and strings. All 16 postulating modules in the Agda standard library are foreign-function and operating-system interfaces; there is no mathematical postulate in its 1,183 modules. Separating mathematical assumptions from interface assumptions changes the ordering of every library in the census. Two further results are reported. The most widely inherited axiom in the Rocq standard library is functional extensionality, not excluded middle, and it is acquired through a chain of Require Export beneath Require Import Program — a mechanism structurally identical to a previously reported classical dependency in Lean's omega. And Agda's compiler-enforced --safe flag provides the only ground truth in this space against which such an instrument can be validated rather than argued for; the validation is reported, across 1,183 modules, without contradiction. The paper also records what the instrument got wrong before correction, including a nested-comment defect that would have reported thirty admitted proofs in a refereed archive which has none, and a null result: "declared but never cited" is not a defect signal in formal libraries.