Math Machines: The Systems Architecture of Mathematical Trust

Mathematical trust is becoming an engineering problem. As proofs and results increasingly depend on solvers, proof assistants, large libraries, numerical pipelines, and evolving toolchains, “accepted by review” no longer guarantees that correctness can travel across teams, time, and infrastructure. This paper proposes Math Machines: seven interoperable architectures that treat closure as a computable state transition under explicit admissibility rules. The approach is deliberately zero-trust: the prover (human, AI, or system) is treated as an untrusted source until it supplies verifier-facing artifacts. We specialize the zero-trust closure architecture from science to mathematics by making proof artifacts, checkers, and identity constraints first-class closure objects. We unify three elements into a single operational model: (i) tribunals that declare what counts as evidence and what it means to be closed, (ii) receipts that make verification cheaper than reproduction, and (iii) obligation graphs that localize what remains open (OPEN), partially supported (HOLD), or closed (CLOSED). A running example is used throughout: a large CNF UNSAT claim accompanied by a DRAT/LRAT-style proof log and independently checkable verification. The goal is not to replace peer review, but to move correctness closure from authority to protocol — especially under AI-driven claim volume, tool drift, and adversarial failure modes.