Beyond Kernel Verification: The Missing Engineering Layer of Mathematics

Abstract

AI systems can now produce mathematical arguments and formal proof code quickly. This does not make verification a single solved problem. A Lean file may compile while the announced theorem still depends on an unresolved citation, transport, computation, or project axiom. Even after every dependency is closed, a proof can remain too large, opaque, or unstable to reuse economically. This paper calls these the closure problem and the composition problem, and develops a mathematical engineering layer for handling both. Two author-produced cases make the distinction concrete. A direct combinatorial proof reaches a comparatively light kernel-checked endpoint; a certificate-heavy extremal proof also reaches an exact endpoint, but its full replay requires days of compilation and tens of gigabytes of cache. The comparison motivates a theorem component organized around three questions: what exact claim is made, what evidence and checker establish it, and how can others reuse and maintain it? The proposed layer combines semantic maps, dependency and axiom manifests, reproducible checking, resource profiles, stable interfaces, and lifecycle ownership. These principles are not confined to fully formalized mathematics: informal results face the same handoffs through citations, computations, versions, explanation, and maintenance, although their checking boundaries are less exact. Journal review and kernel acceptance remain complements to mathematical understanding; neither replaces it. The central claim is that growing proof output requires explicit handoffs from candidate to closed result and from closed result to durable shared knowledge.