Metadata-Version: 2.4
Name: axsent
Version: 0.1.0
Summary: Measure what a formal library assumes: Rocq, Agda and Isabelle, from source, with nothing built
Author-email: Vincent Gonzalez <vincegonzalez@me.com>
License-Expression: MIT
Project-URL: Homepage, https://github.com/vince-gonzalez/axsent
Project-URL: Paper, https://doi.org/10.5281/zenodo.22148932
Keywords: axiom provenance,formal verification,proof assistants,Rocq,Agda,Isabelle,dependency analysis
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Quality Assurance
Requires-Python: >=3.9
Description-Content-Type: text/markdown
License-File: LICENSE
Dynamic: license-file

```
╔════════════════════════════════════════════════════════════════════════════════════════════╗
║                                                                                            ║
║                     █████╗ ██╗  ██╗███████╗███████╗███╗   ██╗████████╗                     ║
║                    ██╔══██╗╚██╗██╔╝██╔════╝██╔════╝████╗  ██║╚══██╔══╝                     ║
║                    ███████║ ╚███╔╝ ███████╗█████╗  ██╔██╗ ██║   ██║                        ║
║                    ██╔══██║ ██╔██╗ ╚════██║██╔══╝  ██║╚██╗██║   ██║                        ║
║                    ██║  ██║██╔╝ ██╗███████║███████╗██║ ╚████║   ██║                        ║
║                    ╚═╝  ╚═╝╚═╝  ╚═╝╚══════╝╚══════╝╚═╝  ╚═══╝   ╚═╝                        ║
║                                                                                            ║
║                               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.

```bash
pip install axsent
```

```bash
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](https://pypi.org/project/gonzalgo/)
and [mmforge](https://pypi.org/project/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

