Proof Engine Infrastructure: A Fail-Closed Claim-Graph Method for Accountable AI-Assisted Mathematical Research

Background: AI systems can produce proof sketches, formal code, solver artifacts, and candidate strategies faster than research communities can assess them. Long-running and parallel agents can also hallucinate, lose problem context, duplicate obligations, or return incompatible formulations. Disclosure and local checking alone do not show which claim has been earned, whether its dependency route is closed, or whether evidence remains current after correction. Methods: Proof Engine Infrastructure was developed as a fail-closed method for claim-level research reporting. An agent-to-claim control plane externalizes claims, obligations, and receipts in a typed directed hypergraph. Its minimum loop declares the target and admissible roots, decomposes claim paths, dispatches work, assigns edge-adequate evidence boundaries, binds checked inputs and outputs, composes earned edges, and recomputes the frontier. A contrasting-case analysis examined three completed projects with different mathematical objects and two closure architectures. An odd-sum case visualizes parallel checks, asynchronous returns, frontier selection, an unresolved continuation, and retained knowledge. Results: A new uniform Hamilton classification tested paper-to-kernel binding. A new exact all-N solution of Erdős Problem 848 completed the finite range left by earlier GPT-5-assisted work, using compression, certificates, semantic checking, complete coverage, and kernel replay. A rational-Dyck-path project repeated direct closure on a new object. The running graph showed five parallel checks, one selected open frontier, and retained partial and negative routes without claiming closure. A separate large ongoing proof program provided qualitative operational evidence for concurrent proof search, formalization, review, correction, and assembly. Wider parallelism was useful but token- and coordination-intensive. Conclusions: Fail-closed agent-to-claim graphs provide a correction-aware control layer between AI-assisted generation, heterogeneous verification, and publication. Three completed projects provide bounded transfer evidence within mathematics, while ongoing use supports practical concurrent development. The next research stage is a graph-native Proof Engine 2.0 protocol for typed handoffs, receipt-only trust, conflict resolution, dependency-aware scheduling, and resource accounting, followed by matched-task quantitative evaluation.