axsent 0.1.0

╔════════════════════════════════════════════════════════════════════════════════════════════╗
║                                                                                            ║
║                     █████╗ ██╗  ██╗███████╗███████╗███╗   ██╗████████╗                     ║
║                    ██╔══██╗╚██╗██╔╝██╔════╝██╔════╝████╗  ██║╚══██╔══╝                     ║
║                    ███████║ ╚███╔╝ ███████╗█████╗  ██╔██╗ ██║   ██║                        ║
║                    ██╔══██║ ██╔██╗ ╚════██║██╔══╝  ██║╚██╗██║   ██║                        ║
║                    ██║  ██║██╔╝ ██╗███████║███████╗██║ ╚████║   ██║                        ║
║                    ╚═╝  ╚═╝╚═╝  ╚═╝╚══════╝╚══════╝╚═╝  ╚═══╝   ╚═╝                        ║
║                                                                                            ║
║                               what a formal library assumes                                ║
║                                                                                            ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝

An accent is a dependence on something local that travels with whoever carries it. An inherited axiom is the same thing: a library speaks in the assumptions of wherever it came from, and most of what it carries it never chose.

Rocq, Agda and Isabelle each let a development assert something without proving it, and each records the dependency edges that carry the assertion outward. axsent reads those declarations and those edges from source text, with no proof assistant installed and nothing built.

pip install axsent

axsent rocq      path/to/stdlib/theories
axsent agda      path/to/agda-stdlib/src
axsent isabelle  path/to/afp/thys

Why counts should not be totalled

A library declares two kinds of assumption and both use the same keyword.

Mathematical — excluded middle, choice, functional extensionality, proof irrelevance. Claims about mathematics. A result depending on one is classical rather than constructive.

Interface — that native 63-bit arithmetic behaves as specified, that a mutable array returns what was written to it, that a foreign function returns what its type says. Claims about the machine and the runtime. A result depending on one is not thereby classical.

Rocq's Corelib declares five times as many axioms as the Rocq standard library and makes no mathematical assumption at all: all 73 specify primitive machine arithmetic, native arrays, floats and strings. Every one of the 16 postulating modules in the Agda standard library is a foreign-function or operating-system interface. A single figure hides which of the two you are looking at.

What it is not

It does not read Lean or Metamath. gonzalgo and mmforge do that. This is a separate instrument for separate systems, not an extension of either.

It measures at file or module granularity, not per theorem. A file requiring a module that declares an axiom inherits it whether or not any theorem in that file uses it, so every figure is an upper bound on inheritance, not a statement about use. Print Assumptions and #print axioms answer the per-theorem question and need a built library. This needs only the source, which is what makes a cross-system census tractable.

Reading the source correctly

Three exclusions do real work, and each was derived from a failure rather than anticipated.

Rocq Parameter and Hypothesis are not axioms inside a Module Type or Section — they are discharged. The Rocq standard library has 389 Parameter and 125 Hypothesis against 14 top-level Axiom; counting the former reports a library assuming five hundred things it does not.

Agda postulate must open a block. postulate[_|->_] is a legal function name, and a word-boundary match counts it as an assumption.

Isabelle comments nest. (* outer (* inner *) still outer *) is one comment; a non-greedy match closes it at the inner terminator and returns the rest as live code. On the Archive of Formal Proofs that single difference is 33 reported sorry occurrences against 3.

The check that makes it trustworthy

Agda's {-# OPTIONS --safe #-} is compiler-enforced and transitive: a safe module may not postulate and may not import a module that is not itself safe. The compiler has already computed the transitive answer, so axsent agda ends by checking itself against it. Any module reported as both --safe and reaching a postulate is a bug in this tool, not a finding about Agda.

Nothing in Rocq, Isabelle, Lean or Metamath offers a comparable ground truth. Run the Agda census first for that reason alone.

Citation

The method and the five-library census it produced:

Gonzalez, V. 2026. Interface Assumptions Are Not Mathematical Assumptions: An Axiom Census of Five Libraries Across Four Proof Systems. Zenodo. https://doi.org/10.5281/zenodo.22148932