Path Integral Proof Search
Formal Verification Certificate
This research has been formally verified and integrated into production systems. Every claim is backed by machine-checked proof.
Path Integral Proof Search • Lean 4 + Mathlib • Apoth3osis Labs
Can proof search be formalized as a path integral with convergence guarantees?
Automated theorem provers explore a graph of tactic states, but the search strategy is typically ad hoc—heuristic scoring, random restarts, timeout-based backtracking. There is no theory of the search process itself. No measure over paths. No notion of convergence. No way to detect when two strategies are topologically equivalent and one can be pruned.
Path Integral Proof Search changes this. Proofs are paths through a multiway graph of proof states. Each path has an action (cost). The path integral sums over all paths weighted by exp(−β·S), recovering the minimum-action proof as β → ∞ and uniform exploration as β → 0. Sheaf cocycle conditions ensure consistent weighting across multiple proof perspectives. Çech H¹ detects topologically inequivalent strategies.
This project formalizes the entire framework in Lean 4: path algebra, action functional, Boltzmann measure, sheaf transport, homotopy theory, obstruction detection, and annealing convergence—79 theorems, zero sorry, across 11 modules and 2,382 lines of proof code.
Why this is Ruliology
Proof search is a rule system: you have states, transitions (tactics), and a combinatorial explosion of paths. The path integral treats this rule system the way statistical mechanics treats physical systems—by summing over all configurations weighted by their action. The result is not a single proof but a measure over the space of all proofs, with mathematically guaranteed convergence properties.
The sheaf-theoretic layer is where the formalization goes beyond standard search theory. Multiple proof “lenses” (perspectives on the same goal) create a covering of the search space. The cocycle inequality on transport factors ensures that any path through a sequence of lens transitions has bounded cost—no runaway penalties from cascading perspective shifts. When the Çech H¹ class is nontrivial, the proof search has topologically inequivalent strategies that cannot be deformed into each other. This is a structural fact about the search space, not a heuristic.
The formal verification commitment: every convergence bound, every cocycle inequality, every obstruction witness is machine-checked by the Lean 4 kernel. The gap between the ℝ-valued theory and the Float-valued runtime is honestly acknowledged (Known Limitation #4)—not papered over.
What Is Proved vs. What Is Engineering
Proved (79 theorems)
- •Path composition is valid, associative, has identity
- •Action is non-negative, additive, zero on identity
- •Boltzmann weights converge (β→∞ kills non-minimal)
- •Transport factors bounded [1,2] with cocycle inequality
- •Çech H¹ detects inequivalent strategies
- •Geometric annealing converges exponentially
Engineering (not proved)
- •Choice of three-component action decomposition
- •Heuristic thresholds in action weights
- •Float-valued beam search vs ℝ-valued theory
- •“Homotopic” is coarser than genuine topological homotopy
- •Only triangle skeleton (n=3 cover) for Çech
- •Convergence for finite path sets, not completeness
ProofPath.lean Path algebra: composition, identity, associativity
│
Action.lean Three-component cost: naturalness + transport + compression
│
Measure.lean Boltzmann exp(−β·S), sheaf transport, cocycle bounds
│ │
Topology.lean GroupoidBridge.lean
(homotopy, (J-eliminator,
ProofGroupoid, quotient classifiers,
Čech obstruction) transport-based H¹)
│ │
└──────────┬───────────────┘
│
AnnealingTheory.lean Convergence: geometric/logarithmic/linear schedules
│
┌──────────┼──────────────────┐
│ │ │
Search.lean Adapter.lean ObstructionMonitor.lean
(beam search) (DiffATP bridge) (live Čech pruning)
│ │ │
└──────────┼──────────────────┘
│
Main.lean CLI entry point
│
Tests.lean 417 lines, 47 regression examplesPath Algebra
Foundation: ProofState, ProofStep, PathValid inductive for connectivity witnesses, ProofPath structure with composition. Associative composition, identity elements (left/right), length additivity over composition, and validity preservation through join.
- •comp_valid — composition of valid paths is valid
- •comp_assoc — path composition is associative
- •comp_id_left, comp_id_right — identity neutrality
- •length_comp — length is additive over composition
Action Functional
Three-component cost: operationNaturalness + transportCost + informationCompression. Uses a 6-element FSum (actionTransportProbe) for concrete transport profiles. Every step and every path has non-negative action. Action is additive over composition and zero on identity paths. Same-lens steps incur zero transport cost.
- •stepActionRat_nonneg — every step has non-negative action
- •pathActionRat_nonneg — every path has non-negative action
- •action_comp — S(p·q) = S(p) + S(q)
- •action_id — S(id) = 0
- •nucleus_step_zero_transport — same-lens → zero transport cost
Boltzmann Measure & Sheaf Transport
Boltzmann weights exp(−β·S) with SheafConsistentMeasure structure. Multiplicative weight composition W(p·q) = W(p)·W(q). Classical limit: as β → ∞, non-minimal paths are exponentially suppressed (Filter.Tendsto). Uniform limit: at β = 0, all paths have equal weight. Transport factors bounded in [1,2] with cocycle (triangle) inequality. Concrete boltzmannMeasure instance.
- •weight_comp — W(β, p·q) = W(β, p) · W(β, q)
- •beta_limit_classical — β→∞ suppresses non-minimal paths
- •beta_limit_uniform — β=0 gives equal weight
- •lensTransitionFactor_cocycle — triangle inequality
- •lensTransitionFactorRat_ge_one, _le_two — bounds [1,2]
- •boltzmannMeasure — concrete SheafConsistentMeasure
Homotopy & Čech Obstruction
Discrete homotopy via ProofPath.homotopic setoid (preserves start, finish, transportSupport). ProofGroupoid quotient. Canonical stationary and obstructed loops. H¹ class existence implies topologically distinct proof strategies. J-eliminator (groupoidJ) via Quotient.hrecOn. Transport-based obstruction classifier obstructionClassT that respects homotopy and factors through the quotient. Obstructed quotient classes yield concrete Čech H¹ witnesses.
- •nontrivial_H1_implies_inequivalent — H¹ ↔ distinct strategies
- •single_lens_all_homotopic — single-lens paths are homotopic
- •groupoidJ — J-eliminator for ProofGroupoid
- •obstructionClassT_respects_homotopy — homotopy invariance
- •groupoid_obstruction_yields_H1 — obstructed class → H¹ witness
Annealing Convergence
Three annealing schedules (geometric, logarithmic, linear) with convergence bounds. Positive action gap for finite path sets with a strict minimizer. Geometric schedule gives exponential bound on non-minimal path weight ratios. As steps → ∞, all non-minimal path probabilities converge to zero (Filter.Tendsto). Logarithmic (Hajek-style) cooling diverges to ∞.
- •actionGap_pos — finite sets with strict minimizer have positive gap
- •geometric_convergence_rate — exponential bound on weight ratios
- •geometric_convergence_rate_tendsto — non-minimal probabilities → 0
- •logarithmicBeta_tendsto_atTop — log cooling diverges
Runtime & Integration
Beam search with configurable width, temperature annealing, and live Čech obstruction pruning. DifferentiableATP adapter: parseGoalToFSum, searchNodeToProofState, runPathIntegralSearch. CLI entry point with JSON output, schedule selection, and full argument parsing. 417-line test suite with 47 regression examples covering all layers.
- •pathIntegralSearch — beam search with obstruction pruning
- •checkObstruction, partitionByObstruction — live H¹ monitoring
- •canonical_loop_detected, singleton_clear — obstruction witnesses
- •parseGoalToFSum, runPathIntegralSearch — ATP adapter
Six Extensions from This Foundation
Higher Homotopy
Upgrade from π&sub1; (fundamental groupoid) to higher homotopy groups. Detect not just loops but higher-dimensional obstructions in the proof space.
Continuous Path Integral
Replace discrete path sums with genuine Wiener-measure path integrals. Connect to stochastic differential equations for proof-state dynamics.
Learned Action Functional
Replace the hand-tuned three-component action with a neural action functional trained on proved (goal, tactic) pairs. The mathematical framework stays unchanged.
Runtime Verification
Bridge the theory-runtime gap: formally verify the Float-valued beam search against the ℝ-valued Boltzmann measure using interval arithmetic.
Empirical Benchmarks
Measure prove-rate improvements on standard benchmarks (miniF2F, ProofNet). Compare PathIntegral search against vanilla best-first and MCTS.
Multi-Kernel Transport
Extend sheaf transport across proof assistants (Lean, Coq, Isabelle). Transport factors encode the cost of cross-kernel translation; cocycle bounds still apply.
GitHub Repository
Standalone repo with all 11 Lean source files, README, CITATION.cff, and license.
IPFS Archive
Content-addressed, permanently pinned Lean source archive.
bafkreiawdmura4w2qngg2ckqnqrxjbvsx6pevnwf5tw27qk725he4h4i2a
All Research Projects
Browse all Ruliology research projects and formalized mathematics.
PATH INTEGRAL PROOF SEARCH · HEYTINGLEAN · APOTH3OSIS