AI 支援数学の命題単位検証：カーネルで閉じた Hamilton 分類と境界の混在する Rado 研究

AI-assisted mathematical work often combines formal proofs, solver outputs, and explicit witnesses. Readers need to know which claim each object supports and which dependencies remain unresolved. This article develops a comparative case study of that task through a Hamilton classification and a Rado-number investigation. Its verification-profile concepts were incorporated into and extended by Proof Engine Infrastructure, which organizes claim dependencies, composes accepted evidence, and revises research status after correction. The present article provides the complementary case-level account: explicit links from mathematical statements to verification objects, the conclusions licensed by each check, and the assumptions retained by their downstream uses. The Hamilton case traces complete cycle and path classifications for the noncrossing partition refinement graph to matching Lean 4 endpoints with only standard logical dependencies. The Rado case, for x + by = bz, separates a constructive lower bound, finite satisfiability (SAT) obligations, formal deductions using specified computational inputs, and an open threshold conjecture. In particular, checking the published coloring establishes R_5(3) > 296, whereas a Lean declaration that assumes the same bound does not independently verify that witness. The comparison distinguishes the heterogeneity of checking procedures from the completeness of support for a stated target. It also distinguishes evidence accumulation for a fixed claim from withdrawal and revalidation after a correction. The contribution is a worked audit of these boundaries, with a reusable claim-to-evidence record and concrete checking routes. It helps readers assess both fully closed results and rigorously delimited partial studies within the broader Proof Engine framework.