>_VERIFICATION.SEAL
Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps.
0 SORRY
Kleene K\u2081 Realizability • Lean 4 + Mathlib • Apoth3osis Labs
❓
The Central Question
Can every computable function be represented in Kleene’s realizability model? This project formalizes Kleene’s K₁ model — where natural numbers serve as realizers (witnesses) via partial recursive function evaluation — and proves it has K and S combinators satisfying their standard laws. This establishes combinatory completeness: every computable function is representable, bridging Curry-Howard (propositions = types) with classical recursion theory (realizability = computability).
Original Researcher
Stephen Cole Kleene
University of Wisconsin–Madison (1909–1994)
Founder of recursion theory and the theory of recursive realizability. Introduced Kleene’s realizability interpretation in 1945, providing the first systematic connection between constructive mathematics and computation. His work is foundational to the Curry-Howard correspondence, constructive type theory, and modern proof assistants.
K₁ Realizability Interpretation
| Connective | Classical | K₁ Realizability |
|---|---|---|
| ∃x.P(x) | Some x exists | n encodes witness + proof |
| P → Q | If P then Q | n transforms P-witnesses to Q-witnesses |
| P ∨ Q | P or Q | Tag (0/1) + realizer for chosen branch |
| ∀x.P(x) | For all x | Uniform realizer for all inputs |