Things you read. Every claim carries a DOI.
| Name | Type | Status | Description |
|---|---|---|---|
| 📄axsent | Python package | pip install | What a formal library assumes, measured from source: Rocq, Agda and Isabelle, with nothing built. |
| 📄authorecon | Python package | pip install | Reconcile published work against every place it lives, for any ORCID, from public sources. |
| 📄mmforge | Python package | pip install | Find avoidable axiom dependencies in Metamath, and build the proofs that remove them. |
| 📄loadbearing | Python package | pip install | What a claim asserts, separated from what its derivation consumed. |
| 📄certivl | Python package | pip install | Certified interval arithmetic: an enclosure that turns a computed inequality into a proof. |
| 📄ishihara | Python package | pip install | Generate pseudoisochromatic color-vision plates, reproducible from a seed. |
| 📄gonzalgo | Research tool | Published | Which axioms a Lean 4 or Metamath theorem spends rather than inherits. |
| 📄Papers | Publications | Published | Where formal libraries spend their axioms. Full text, DOIs, archives. |
| 📄Modulign | Standard | Published | A dimensional address grammar for observable reality. DAG-OR v3. |