Theorem Notary：カーネル検証済み定理の公開と再利用のための Glass Box プロトコル

AI-assisted mathematics needs completed formal proofs to become dependable inputs to further research. Even after a theorem is proved, an independent consumer must identify its exact statement and assumptions, obtain its proof dependencies, and establish which checks remain valid through later reuse. Existing package imports and proof checkers provide essential mechanisms; successive publications also need a shared contract for carrying these choices forward. We propose Theorem Notary, a Glass Box protocol for a growing network of independently published theorem components. Each eligible theorem has a complete proof checkable by the kernel, the proof assistant's logical core, under a disclosed foundation. Its certificate binds the full statement, definitions, source and proof data, and inherited publications. Publicly inspectable proof material supplies the Glass Box justification; provider signatures record supply without adding logical authority. Consumers select exact identities, check every inherited certificate, and reuse only their own authenticated acceptance for an unchanged checking scope. Derived results enter the same publication cycle. A Lean reference profile specifies these boundaries and their build integration. Evaluation combines actual theorem consumption across independent project boundaries with a large archived formalization and attacks on statement identity, inner proof obligations, and acceptance reuse. The protocol makes completed proofs and valid acceptance reusable inputs to new derivations. It supports cumulative formal knowledge across independently maintained repositories, providing an admission contract for subsequent human and automated mathematical development.