Beyond Kernel Verification: The Missing Engineering Layer of Mathematics

Abstract

Artificial intelligence and autoformalization are moving mathematics from proof scarcity toward proof abundance. Terence Tao has described the resulting pressure: proof generation and formal verification may accelerate faster than exposition, publication, digestion, and canonicalization. This paper gives a direct answer to the narrow deductive-verification question and argues that the answer exposes a larger institutional deficit. For a fully formalized theorem, kernel-only checking is the appropriate baseline. If a small trusted kernel accepts a proof term for the exact statement after checking its load-bearing dependencies under a disclosed axiom and version boundary, validity becomes reproducible relative to that statement and trust base rather than probabilistic confidence in the generator. Yet kernel acceptance does not show that the formal statement matches the intended theorem, make the proof intelligible, turn it into a stable component, or integrate it into shared mathematical knowledge. We call this the bottleneck-displacement thesis: scalable kernel verification does not eliminate verification asymmetry; it moves the binding constraint from local deduction toward semantic binding, interfaces, exposition, maintenance, and communal uptake. Two kernel-closed projects illustrate the distinction. A Gray-code-based Hamilton classification uses a uniform construction, while a proof of Erdos Problem 848 uses a certificate-oriented route whose generators remain outside the trust boundary. Together they show that machine-level closure is feasible for different proof forms while closure and comprehension remain independent. We therefore propose a mathematical engineering layer of theorem-component contracts, proof and certificate packages, semantic maps, dependency manifests, versioned interfaces, reproducible gates, and lifecycle ownership, supported by professionals responsible for packaging, composition, audit, maintenance, and explanation. Lean, Mathlib, and related formal systems are foundations for this development; the missing object is a mature cross-paper and cross-project layer above them. This is not a proposal for a new proof assistant, and two cases do not establish field-wide maturity. It is a theory of what becomes necessary once kernel verification begins to succeed.