Mathesis is the maths section of the hyperpolymath estate. It keeps an atlas of the mathematics in other repositories, the theory that no single system owns, and methods that apply mathematics to decisions. Each statement carries its evidence: Mathesis derives status from the receipts of the home repositories, and does not assert it.
The standards repository prescribes what must be proved (PROOF-POLICY). Each home repository proves its own claims and keeps their receipts. Mathesis describes what is proved, where, and how strongly.
-
A census of proof files. It reads each public repository in the frame (
docs/atlas/census/repos.jsonl) and records one row of counts for each repository that has proof files of its own: provers, declarations, holes, axioms. Each row names the commit that the census read and when. -
Generated atlas views. A catalogue split into theory and engineering, an A-Z view, an organisation view and a machine-readable index, all generated from the census rows.
-
A claims registry. Claim pins point at one theorem in its home repository, at a commit and a receipt digest. The canon receipt reader of PROOF-POLICY §8.5.1 derives each Proof Witness Grade. No grade is typed by hand.
-
Bridge candidates. Recorded relations between artefacts in two repositories, generated into one view.
-
Home theory. THY-1, reachability is monotone under additive features, is proved in Agda and re-proved in Rocq and Lean. CI checks all three in a pinned Guix shell. A theorem enters the theory shelf only under a stated admission rule, and a generated index lists each one with its dependant.
-
Applied systems. Methods that apply mathematics to decisions, starting with accounting and finance. A shared input schema keeps missing apart from zero. A cohort model in Agda has three number modes and three synthetic worked examples, each checked by Agda. Its four general properties are proved in Agda and re-proved in Rocq and Lean.
-
Privacy by count. The frame names public repositories only. The number of private repositories in the listing is kept as one number.
|
Note
|
Planned
The token-lattice theorems of the theory shelf, receipts for the cohort model proofs (APP-1 to APP-4), a published atlas, receipts in more home repositories, and a scheduled census. See the roadmap. |
The views check needs Bun, network access for the receipts, and a checkout of
metadatastician/standards at the reader pin named in
scripts/registry/claims-registry.mjs.
export MATHESIS_STANDARDS=/path/to/standards
just check-views
bun scripts/atlas/census-atlas.mjs find agdaThe proof checks need Agda, Rocq and Lean. CI runs them in the pinned Guix
shell; just check runs both halves.
guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- just checkWondering how this works? See EXPLAINME.adoc.
| Path | Purpose |
|---|---|
|
The atlas shelf: census data ( |
|
The census, the atlas views and the claims registry |
|
Their tests, with negative controls |
|
Home theory sources: Agda, Rocq and Lean |
|
The proof receipt of Mathesis |
|
The theory shelf: the admission rule, the admission records and the generated theorem index |
|
The applied shelf |
|
Roadmap, proof needs, proof status, readiness and test needs |
|
The repository deed: identity, boundaries, golden path |
-
EXPLAINME: the evidence for each claim above, and the proof ledger.
-
Atlas: the pipeline, the public frame and the one-writer rule for census data.
-
ADR 0004: the claims registry.
-
Standards and authority map: the limits of Mathesis.
-
Roadmap and proof status.
-
Re-anchoring plan: the identity and the stages of work.
Code (scripts/, Justfile): MPL-2.0. Documentation and the catalogue:
CC-BY-SA-4.0. See LICENSE and LICENSES/.