Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps. Each claim is machine-checked by the Lean kernel.
Ruliad Lambda • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
What happens when you treat λ-calculus as a rule system and explore all possible term evolutions simultaneously? Wolfram’s “The Ruliology of Lambdas” (2025) proposes exactly this: β-reduction generates multiway graphs, and the structure of these graphs reveals deep connections between computation, confluence, and the topology of the lambda term space. This project provides the first machine-checked verification of the key results: Church-Rosser confluence, λ↔SK simulation, and multiway enumeration.
Original Researcher
Key Verified Results
Steps.churchRosserChurch-Rosser confluence — all β-reduction paths converge
Confluence.lean
Bridge.ofComb_simulates_step_joinableλ ↔ SK bidirectional simulation
SKYBridge.lean
stepEdgesListSound enumeration of multiway β-reduction edges
Beta.lean
enumTermsSize-bounded term enumeration
Enumeration.lean
What Is Proved vs. What Is Exploration
Proved
- •Church-Rosser: β-reduction is confluent
- •λ↔SK simulation: combinators faithfully represent λ-terms
- •Multiway edge enumeration is sound and complete
- •Term enumeration by size is exhaustive
Exploration (not proved)
- •Branchial space geometry and clustering
- •Computational class distribution across term sizes
- •Ruliad structure beyond size-6 terms