From Lean Proofs to Axiom-Free Executables
A specification for verified compilation, diverse-kernel validation, and higher semantics
Author: Anonymous. Version: 1.0, 27 October 2026.
Status: Specification for a future verified Lean implementation. The attached PDF contains the full manuscript, proofs, assumptions, and bibliography. The source package contains a finite executable reference model and its measured test report. Neither a complete Lean compiler implementation nor completed multi-kernel validation is claimed.
1. The computational object
For $A:\mathrm{Type}$, $B:A\to\mathrm{Type}$, and $R:\prod_{x:A}B(x)\to\mathrm{Prop}$, distinguish
$$H:\forall x:A,\exists y:B(x),R(x,y)$$
from a witness-producing construction
$$F:(x:A)\to\{y:B(x)\mid R(x,y)\}.$$
An ordinary Lean existential proof lives in proof-irrelevant Prop; it cannot generally be eliminated into arbitrary data. The second interface returns a value with a certificate. Projection gives $f(x)=(F(x)).\mathrm{val}$ and the proof $(F(x)).\mathrm{property}$ without adding choice. For a type-valued second family use Sigma; for a proposition-valued property use Subtype.
This does not say that every proof is an executable algorithm. Let $\mathsf{Halt}(e)$ be the diagonal halting predicate and define
$$R(e,b)\iff(b=1\land\mathsf{Halt}(e))\lor(b=0\land\neg\mathsf{Halt}(e)).$$
Classically $R$ has a unique Boolean witness for every $e$, but a total computable selector would decide the halting problem. Uniqueness alone does not create an algorithm.
2. Three separate guarantees
We distinguish (i) absence of declared axioms from audited logical dependencies, (ii) computational support for all retained operations, and (iii) a theorem relating source and target execution. Proof erasure does not imply logical axiom freedom; kernel checking does not automatically prove native compiler correctness.
For a finite declaration environment $D$ and selected roots $S$, let $\mathsf{Reach}_D(S)$ be the least set containing the roots and every referenced declaration in types, bodies, and inductive/recursor dependencies. Define
$$\mathsf{Ax}_D(S)=\{a\in\mathsf{Reach}_D(S):a\text{ is an axiom declaration}\}.$$
The default strict profile requires $\mathsf{Ax}_D(S)=\varnothing$. Roots include source programs, specifications, correctness proofs, frontend certificates, and the compiler theorems used for release. This excludes Classical.choice, propext, Quot.sound, sorryAx, user axioms, and native-evaluation axioms when reachable. Kernel rules such as proof irrelevance remain foundational assumptions; an empty axiom list is not an assumption-free foundation.
The audit must inspect exported terms and types, including opaque proof bodies, rather than search source text. An ordinary worklist computes the finite reachable closure: each node is expanded at most once; path induction proves completeness. Missing bodies, unresolved references, duplicate identifiers, and malformed exports are errors. Open hypotheses must be discharged or exposed as preconditions. A proof of $P\to Q$ is not a proof of $Q$.
Runtime admissibility is additional. The first frontend rejects unsupported recursion, quotient operations, unproved representation changes, unsafe and unrestricted partial computation, and unchecked foreign implementations. A flag such as noncomputable is a conservative engineering signal, not a decision procedure for mathematical noncomputability. Trusted host arithmetic must have an explicit primitive ledger and refinement boundary.
3. Exact initial language
The initial target is a deeply embedded arithmetic language inside Lean, not arbitrary Lean.Expr. Let $E_n$ be well-scoped expressions with $n$ natural-number variables, environments $\rho\in\mathbb N^n$, and newest variable at index zero. Constructors are
$$e ::= k\mid\mathsf{var}(i)\mid\mathsf{add}(e,e)\mid\mathsf{let}(e,b)\mid\mathsf{if0}(c,t,f)\mid\mathsf{loop}(m,z,b)\mid\mathsf{ann}(P,h,e).$$
Here $i:\mathrm{Fin}(n)$; the body of let belongs to $E_{n+1}$; a loop body belongs to $E_{n+2}$; and an annotation carries $P:\mathrm{Prop}$ and $h:P$. An annotation does not automatically assert a semantic property of its enclosed program.
Numerals, variables, and addition have their standard denotations. A binding evaluates its value and extends the environment. if0 evaluates only the selected branch. A loop evaluates its bound and seed once, starts with $a_0=\llbracket z\rrbracket\rho$, and computes
$$a_{i+1}=\llbracket b\rrbracket(a_i::i::\rho),\quad 0\le i<\llbracket m\rrbracket\rho.$$
Thus the body sees accumulator at index zero and iteration index at index one. The loop returns the last accumulator. An annotation has the denotation of its body.
A semantic certificate is separate:
$$p:\forall\rho,\ P(\rho)\to R(\rho,\llbracket e\rrbracket\rho).$$
Every expression is total: structural induction reduces the only remaining recursion to induction on the evaluated finite loop bound. This establishes mathematical termination, not feasible resource usage.
The erased data language has the same constructors except annotations. Erasure is homomorphic and satisfies $\mathsf{erase}(\mathsf{ann}(P,h,e))=\mathsf{erase}(e)$.
Erasure theorem. For all $e,\rho$,
$$\llbracket\mathsf{erase}(e)\rrbracket_0\rho=\llbracket e\rrbracket\rho.$$
Proof. Induct on expressions. Bindings use the induction hypothesis at the extended environment. Loop bounds and seeds agree by induction; induction on the iteration index then gives equal accumulators, using the body hypothesis at each extended environment. An annotation reduces to its body. This proves the theorem for the stated language, not all of Lean's dependent core.
4. Structured stack code
The target contains PUSH(k), LOAD(i), ADD, sequencing, ENTER(B), BR(T,F), and LOOP(B). Stacks have their top at the left. The effect judgment $n\vdash C:h\Rightarrow k$ checks environment scope and input/output stack heights.
PUSH and LOAD push one number; ADD maps $b::a::s$ to $(a+b)::s$. ENTER pops an argument and runs its block with that argument added to the environment. BR pops a condition and runs one arm. LOOP takes $z::m::s$ and repeats its block $m$ times under $a_i::i::\rho$. Its body must have effect $h\Rightarrow h+1$ under $n+2$ variables. Arbitrary well-typed blocks can change the base stack's contents, so each iteration carries forward its returned base stack. Compiler-generated blocks satisfy a stronger frame theorem and preserve the original base stack exactly.
The compiler is structural:
$$\begin{aligned} C(k)&=\mathsf{PUSH}(k),\\ C(\mathsf{var}(i))&=\mathsf{LOAD}(i),\\ C(\mathsf{add}(a,b))&=C(a);C(b);\mathsf{ADD},\\ C(\mathsf{let}(v,b))&=C(v);\mathsf{ENTER}(C(b)),\\ C(\mathsf{if0}(c,t,f))&=C(c);\mathsf{BR}(C(t),C(f)),\\ C(\mathsf{loop}(m,z,b))&=C(m);C(z);\mathsf{LOOP}(C(b)). \end{aligned}$$
Compiler theorem. For every $e:E_n^0$ and starting height $h$, $n\vdash C(e):h\Rightarrow h+1$, and for every environment and stack,
$$\mathsf{run}(C(e),\rho,s)=\llbracket e\rrbracket_0\rho::s.$$
Proof. Structural induction supplies the effect and the stronger frame property. Addition pushes the two operand values in order, then adds them. Binding invokes the body theorem with the extended environment and original stack. Branching removes the test before running the selected arm. The loop body theorem preserves the base stack and computes the next accumulator; induction on the loop index identifies the complete accumulator sequence with the source semantics.
Certified execution. Combining erasure and compiler preservation with $p$ gives: if $P(\rho)$, the compiled code returns $[v]$ and $R(\rho,v)$.
The raw decoder/effect checker returns explicit errors for malformed code. The typed interpreter has a totality theorem. Fuel or memory exhaustion in a concrete implementation is a separate outcome; it must never become a fabricated successful answer.
5. Ordinary Lean declarations and the backend boundary
To compile an ordinary Lean declaration $f:\mathbb N^n\to\mathbb N$, an untrusted frontend proposes $e:E_n$ and a certificate
$$q:\forall\rho,f(\rho)=\llbracket e\rrbracket\rho.$$
The kernel checks this exact statement, and the strict audit includes its dependencies. A heuristic or agent-written frontend can therefore be incomplete without being trusted. Unsupported terms are rejected. The source declaration and specification are fixed independently of the candidate; the candidate is not allowed to substitute a different theorem.
The verified endpoint is the specified bytecode machine. Compiling a Lean implementation of its interpreter to a native executable additionally trusts the existing compiler, runtime, arithmetic libraries, operating system, and hardware. A further backend needs a representation relation and an operational simulation theorem, including overflow and resource assumptions. Proof checking alone does not close this gap.
6. Categorical, topos, and homotopy semantics
Contexts denote $\mathbb N^n$; substitutions are tuples of expressions. The substitution lemma is
$$\llbracket e[\sigma]\rrbracket\rho=\llbracket e\rrbracket(\llbracket\sigma\rrbracket\rho).$$
It yields a category after external identification by pointwise equality. In the strict Lean development, use setoid-enriched homs and pointwise laws instead of introducing quotient or function-extensionality axioms. Predicates form a fibration over contexts, with reindexing by precomposition. A refinement morphism consists of a computational substitution and a proof that it preserves the chosen predicates. Forgetting the certificate explains the data/proof separation precisely.
In a locally cartesian closed semantics, a family is a map $p:B\to A$ and a witness-producing dependent function is a section. Internal existence says $p$ is epic. These are different conditions. In sheaves on $S^1$, the sheaf of local square roots associated to $z\mapsto z^2$ is locally inhabited, but has no global section: a section would induce $2k=1$ on fundamental groups. Local existence therefore does not supply globally chosen data.
Computability requires more than a topos interpretation. A morphism of assemblies is tracked by a partial recursive index defined on all valid realizers. For the standard natural-number assembly, such a tracker makes the underlying function total recursive. The source operations and the specified compiler have explicit computational presentations; a bare existence truth value supplies no tracker.
Let $\mathcal X$ be a Grothendieck $(\infty,1)$-topos with natural-numbers object $N_{\mathcal X}$. The arithmetic core interprets in $N_{\mathcal X}^n$. These objects and their mapping spaces are $0$-truncated, so no nontrivial higher paths are magically introduced into this arithmetic computation. More general families distinguish
$$\prod_{x:A}B(x)\quad\text{and}\quad\prod_{x:A}\|B(x)\|_{-1}.$$
In the slice over $A$, the second states that the family map is an effective epimorphism; the first supplies a section. If the map is also $(-1)$-truncated, it is an equivalence and its section is unique up to contractible choice. This uses hypotheses internal to the chosen model; classical uniqueness of a noncomputable relation does not provide them effectively.
Lean's own equality is proposition-valued and proof irrelevant. The higher semantics is external or encoded through explicit objects; it is not an identification of stock Lean equality with arbitrary HoTT identity types. A category of presentations and simulations can be localized at observation-preserving equivalences. The observation functor factors through that localization by its universal property, but every actual compiler pass must still provide the required simulation. Runtime erasure is neither automatically homotopical truncation nor a geometric morphism. Higher-topos model existence and cubical canonicity are also distinct results.
7. Different kernels and release criteria
Lean 4.35.0 supports lake check --paranoid, using the official checker plus leanchecker-paranoid, lean4lean, nanoda, con-leche, and con-ron. These implementations have different degrees of shared design and runtime independence. A hardened build of the official kernel is not a wholly independent proof theory.
The default lake check axiom policy permits propext, Classical.choice, and Quot.sound. It must be supplemented by a strict empty dependency audit. Use #print axioms during development and a structured root-closure check at release.
The release predicate requires all of the following: exact specification/source/code/export binding; empty axiom dependencies of required roots; supported computational operations; matching theorem statements; acceptance of the identical export by every selected checker; and complete reproducibility evidence. Timeouts, unsupported features, missing checkers, and internal errors are not acceptance. Disagreement blocks release; majority voting is not sufficient.
If at least one accepting checker is sound for the fragment and binding is correct, its stated soundness guarantee applies to the intended theorem. Agreement alone does not prove that a checker is sound or justify multiplying independent failure probabilities. In particular, con-leche's model-existence guarantee is relative to its stated set-theoretic hypotheses. Those metatheoretic assumptions are distinct from axioms in the object program.
The release record contains exact versions, dependency locks, roots, theorem statements, axiom closures, bytecode and executable hashes, export identity, checker binary hashes and modes, commands, exit statuses, logs, and test seeds. It states the remaining trust boundary.
8. Implementation plan and evidence
M0 freezes syntax and requirements. M1 implements Lean source/target types, evaluators, and effect checking. M2 proves erasure, stack effects, frame preservation, and compiler correctness. M3 verifies declaration auditing and validates frontend certificates. M4 binds serialization and executable input/output to the verified terms. M5 performs diverse-kernel replay and independent rebuilds. M6 optionally extends the source or verifies a native backend. Extensions require their own rules and proofs.
The accompanying Python reference model uses arbitrary-precision naturals and explicit errors. Its finite validation covers 560 source trees of size 1 through 4, contexts of length 0 through 2, literals 0/1, environments over 0/1/3, and four starting stacks: 3,456 source/environment cases and 13,824 stack cases. Another 1,000 seeded random programs give 4,000 stack cases. Eight targeted programs, 14 rejection cases, two deliberately corrupted translations, a general-loop base-stack case, and explicit budget exhaustion also pass. These are specification checks, not universal proofs or Lean kernel evidence.
Checking with different kernels cannot establish that software has no bugs. A mistaken specification can have a valid proof; parsers, native compilers, runtime systems, and deployment can still fail. The defensible release claim identifies exactly which properties of which artifacts were verified, under which assumptions, and by which checkers.
References
1. de Moura and Ullrich, The Lean 4 Theorem Prover and Programming Language (2021). https://doi.org/10.1007/978-3-030-79876-5_37 2. Lean Reference, Axioms. https://lean-lang.org/doc/reference/latest/Axioms/ 3. Theorem Proving in Lean 4, Axioms and Computation. https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation/ 4. Lean Reference, Elaboration and Compilation. https://lean-lang.org/doc/reference/latest/Elaboration-and-Compilation/ 5. Lean 4.35.0 release notes. https://lean-lang.org/doc/reference/latest/releases/v4.35.0/ 6. de Moura, Lean Now Ships with Verified Kernels (2026). https://leodemoura.github.io/blog/2026-10-15-lean-now-ships-with-verified-kernels/ 7. Breitner and contributors, The con-leche proof idea. https://leanprover.github.io/con-leche/con-leche-proof-idea.html 8. Sozeau et al., Coq Coq Correct! (2020). https://metarocq.github.io/coqcoqcorrect 9. The Univalent Foundations Program, Homotopy Type Theory (2013), sections 3.7-3.8. https://homotopytypetheory.org/book/ 10. Shulman, All (infinity,1)-toposes have strict univalent universes (2019). https://arxiv.org/abs/1904.07004 11. Coquand, Huber, and Sattler, Canonicity and homotopy canonicity for cubical type theory (2022). https://lmcs.episciences.org/9043 12. Jacobs, Categorical Logic and Type Theory (1999). https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html 13. Lurie, Higher Topos Theory (2009). https://arxiv.org/abs/math/0608040 14. Awodey, Birkedal, and Scott, Local realizability toposes and a modal logic for computability (2002). https://doi.org/10.1017/S0960129502003675
Disclosure: Prepared anonymously under human direction with AI assistance. The submitting author or research group remains responsible for the manuscript and any private editorial identification. No completed submission, acceptance, full Lean implementation, or multi-kernel verification is claimed.