Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps.
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
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 |
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.
Contribution Certificates
Immutable contribution records per MENTAT-CA-001. Each certificate is cryptographically anchored with IPFS CIDs.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerRealizability: Computation as Mathematical Witness
Contributor
Stephen Cole Kleene
University of Wisconsin–Madison (historical)
Foundational insight (1945): mathematical truth can be witnessed by computation. In Kleene's realizability interpretation, a proof of ∃x.P(x) is a natural number n that encodes both the witness and a proof that the witness satisfies P. This bridges constructive mathematics and computability theory — truth means having a computable certificate.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerK₁ Model: Partial Recursive Application on ℕ
Contributor
Stephen Cole Kleene
University of Wisconsin–Madison (historical)
The K₁ realizability model: carrier is ℕ, application decodes n as a Nat.Partrec.Code and evaluates, pairing is Cantor pairing (Nat.pair), numerals are identity (n represents n). Realizability clauses define what it means for n to realize each logical connective. The model is the canonical bridge from recursion theory to constructive logic.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerFirst Lean 4 Formalization — K₁ with Combinatory Completeness
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of Kleene's K₁ realizability model. Proves K₁ has K and S combinators satisfying their standard laws (K·x·y = x, S·x·y·z = (x·z)·(y·z)), establishing combinatory completeness. Establishes equivalence with Kleene's original 1945 clause-by-clause definition. All proved without sorry/admit.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Ontological EngineerKleene K₁ Verified Kernel
Contributor
Apoth3osis Labs
R&D Division
All theorems kernel-checked by Lean 4. Guard-no-sorry passes. Standard axioms only.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
Ontological EngineerStandalone Repository + Interactive Proof Maps
Contributor
Apoth3osis Labs
R&D Division
Published as standalone GitHub repository with interactive 2D/3D UMAP proof maps and comprehensive documentation. First publicly available Lean 4 formalization of K₁ realizability.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026