Comparative case analysis demonstrates distinct maintenance and scaling bottlenecks in formal proof systems, highlighting the need for a dedicated mathematical engineering layer.
Key Points
To resolve the closure and composition problems in AI-assisted and formal mathematics by defining an engineering layer that bridges raw kernel verification and reusable mathematical knowledge.
Evaluated two formal proof case studies implemented in the Lean theorem prover: a direct combinatorial proof and a certificate-heavy extremal proof.
Analyzed the computational overhead, cache requirements, compilation runtimes, and downstream dependency stability across both proof types.
Observed that successful kernel checking does not guarantee usability, with certificate-heavy proofs requiring days of compilation time and tens of gigabytes of cache storage.
Formulated a mathematical engineering specification combining semantic maps, dependency manifests, resource profiling, and lifecycle ownership to support durable theorem reuse.