The Operational Curry–Howard: Proof Discovery as Navigated Software Architecture

We propose a framework that unifies two perspectives on formal proof construction: proof as pathfinding in a type-theoretic state space and proof as programming via the Curry–Howard correspondence. The pathfinding view decomposes proof search into routing (creative navigation between goal classes) and closing (guaranteed completion within decidable fragments). The programming view recasts this decomposition as software architecture: decidable fragments are verified libraries, bridges are adapter patterns, and proof planning is API design.

We introduce three structural concepts: (i) domains as closer Voronoi cells — regions of the goal space where a specific decision procedure guarantees convergence; (ii) bridges as cross-domain theorems that transport goals between domains; and (iii) a *fiber bundle structure* on the proof state space that explains its effective dimensionality.

The framework is grounded in analysis of 26,583 proof traces from the Lean 4 across 226 mathematical domains, with external validation against 49,649 tactic-mode proofs from the Lean 4 Mathlib library. We show: (a) the effective dimensionality of the proof space is 4 (92.2% of variance via PCA), with domain switching as the 5th dimension (6.4%); (b) 85% of proof steps in the kernel fall within decidable fragments; (c) dead ends are overwhelmingly routing failures, not closer failures; (d) cross-domain bridges account for a disproportionate share of creative content; (e) the kernel's tactic vocabulary is 34 tactics with routing entropy of 4.58 bits — but the Mathlib comparison reveals this is system-specific: Mathlib uses 255+ core tactics with routing entropy of 8.68 bits, and 88% of its proof patterns are single-use; and (f) the Millennium Problems have distinct geometric fingerprints in the 4D proof space.

These findings lead to the Recursive Separation Principle: proof construction decomposes into four layers, not two, and the separation recurses within each layer. Closing (L1) and routing (L2) are both algorithmizable in principle — closing by decidability, routing by pattern mining — though the effort required scales with corpus diversity. In the kernel (4.58-bit entropy), 6 iterations suffice; in Mathlib (8.68-bit entropy), 7,000+ patterns would be needed. Planning (L3, bridge selection in the Category of Proof Domains) is partially algorithmizable via A* search — and even within L3's creative core, 88% of intermediate reasoning (lemma invention) reduces to fact recall and schema instantiation. Architecture (L4, choosing what to prove and assume) is where mathematics lives and where the Gödel boundary falls. Extending below the formal framework, a pre-formal **numerical exploration** layer (L0) can discover axiom can