Auditable AI-Assisted Mathematics: Kernel-Checked Theorem Closure and SAT-Guided Artifacts

AI-assisted mathematical research can produce conjectures, programs, proof sketches, solver instances, and formal proof fragments faster than those objects can be assessed. We introduce a claim-level verification framework for deciding when such outputs may be used as mathematical evidence. A verification profile associates a mathematically substantive claim with the object that represents it, a checking procedure, the scope of that check, any remaining assumptions, and a stable version identifier. We apply the framework to two contrasting cases. In the first case, the noncrossing partition refinement graph is proved to have a Hamilton cycle exactly for orders 0, 1, and the even orders at least 4, and to have a Hamilton path exactly when n is at most 3 or n is even. The general even-order construction and the odd-order obstruction are formalized in Lean 4. The two exported theorems compile without project-specific axioms or unfinished proof markers, and an axiom audit reports only the standard logical axioms used by Mathlib. The resulting closure profile is kernel closed: exploratory computation is not a premise of the classification. The second case concerns Rado numbers for x + by = bz. Here analytic arguments, SAT obligations, constructive witnesses, and Lean theorems coexist. The formalization identifies the remaining computational inputs by name rather than absorbing them into an unqualified formal-proof claim. The resulting closure profile is mixed boundary. The theoretical contribution is a framework for assigning verification status, not a new solver, proof assistant, or autonomous mathematician. The adequacy of a check is assessed relative to a stated claim, and any assignment of a stronger status must be documented and monotone. Kernel checking, SAT-certificate checking, witness verification, and version audits consequently have distinct, noninterchangeable roles. The two cases show that the same framework can describe both complete theorem closure and mixed-boundary verification while giving readers direct procedures for checking the evidence.