Beyond Kernel Verification: The Missing Engineering Layer of Mathematics

Abstract

AI now generates mathematical arguments and proof code faster than communities can verify, understand, and reuse them. Building on a program already spanning claim-level verification, proof infrastructure, and kernel-closed mathematics, this paper identifies two engineering failures that generation cannot resolve. First, machine-checked projects may still rely on cited theorems, semantic transports, external computations, or unfinished lemmas; local kernel acceptance is not transitive closure of the original claim. Second, closing every dependency does not make a theorem cheap to distribute, intelligible, stable across versions, or composable. Mathematics therefore needs an engineering layer spanning both closure and composition. Contrasting proof architectures make the problem concrete. A direct constructive proof can achieve closure through a light dependency graph, while a certificate-heavy exhaustive proof can reach an exact kernel endpoint yet require days of compilation and tens of gigabytes of cache for full replay. The latter is valid but costly to inherit. The contrast shows that deductive validity and scalable reuse are separate achievements. The proposed layer combines dependency-closure graphs, theorem-component contracts, semantic interfaces, reproducible checkers, and versioned artifacts with division of labor among discoverers, formalizers, verifiers, expositors, and maintainers. It also requires institutions that assign credit, review, training, and lifecycle responsibility to component work. The paper does not claim that cheap independent checking already exists or that all valuable mathematics must be formalized. It argues that AI-driven proof abundance will remain non-scalable until closed results can become understandable and maintainable parts of a larger mathematical system.