Proof Engine Infrastructure: A Claim-Graph Framework for AI-Assisted Mathematical Research

Abstract

AI systems can rapidly produce proof sketches, programs, formalization fragments, solver instances, and candidate proof strategies, but these outputs do not share a common evidentiary status. This paper introduces Proof Engine Infrastructure, an architecture for converting untrusted generation into independently checkable mathematical claims. The architecture couples two levels. At the evidentiary level, each claim is associated with a supporting artifact, a checking procedure, the scope of that check, and any remaining assumptions. At the inferential level, claims and proof obligations form a typed directed hypergraph: alternative routes have disjunctive semantics, whereas obligations requiring several premises have conjunctive semantics. Closure is derived from this graph rather than assigned in prose. The central distinction is between a positive candidate and an earned result. A persuasive argument, a stored certificate, or an isolated formal theorem may justify further work without yet licensing inferential use. Any value, structure, or theorem that changes graph reachability must combine reference grounding, machine-checkable evidence, and an exact binding between the checked object and the stated claim. Promotion is admissible only when these obligations hold together with strength preservation, compositional completeness, and dependency preservation. The checking technology may vary without weakening this invariant. Proof assistants supply one verification boundary; Proof Engine Infrastructure does not replace them, but binds their accepted outputs to exact claims, assumptions, and dependencies, then composes them with other checked evidence to derive graph-level closure. Failed routes remain typed negative evidence without disproving their output claims. Separating generation, verification, composition, and publication also prevents agent identity or provenance from standing in for mathematical evidence. Verification-cost minimization is the design objective, extended from checking an individual artifact to composing heterogeneous evidence across the claim graph. The architecture distinguishes earned research closure from the stronger state of publication closure. A kernel-checked Hamilton classification and a mixed-boundary Rado-number study motivate the framework, but the contribution is methodological: it specifies invariant requirements for evidentiary status and derived closure while allowing implementations to vary with the discipline, proof object, and available verification boundary.