Theorem Notary: A Glass-Box Protocol for Publishing and Reusing Kernel-Checked Theorems

AI-assisted mathematics needs completed formal proofs to become dependable inputs to further research. A project reusing a theorem must preserve its exact statement, assumptions, and proof dependencies, and determine which completed checks remain valid as other projects build on it. We propose Theorem Notary, a protocol for publishing and reusing independently developed theorem components. Its Glass Box design lets a project use a theorem through its stated interface while keeping the complete proof, definitions, dependencies, and foundational axioms publicly available for inspection and checking. The “box” is the reusable interface; the “glass” is continued access to the logical justification behind it. Eligible proofs are complete and checkable by the kernel, the proof assistant's logical core, under the permitted foundational axioms. A certificate binds each theorem to that precise material; provider signatures record who supplied it. Receiving projects check the inherited certificates and retain authenticated records of their own checks. They can reuse those records when the bound inputs and checking conditions remain unchanged. New theorems enter the same publication cycle. A reference implementation for the Lean proof assistant specifies the checks and integrates them into project builds. Evaluation follows actual theorem use across independent projects, examines a large archived formalization, and attempts statement substitution, concealment of dependencies, and forgery of prior checking results. The protocol supplies a common publication and acceptance contract through which completed proofs support cumulative human and automated mathematical development.