| \documentclass[11pt]{article} |
| \usepackage{common} |
| \title{} |
| \begin{document} |
| \notehead{0301}{Curry--Howard: propositions as types, proofs as terms}{What it \emph{means} for the Lean kernel to accept a proof, and which axioms keep a proof-based reward honest. Companion notebook: \texttt{notebooks/\allowbreak 0301-curry-howard.ipynb}.} |
|
|
| |
| \begin{problem} |
| \question{When does the kernel accepting a term amount to an unforgeable certificate that a statement is proved, and relative to what?} |
| A reward for a prover must answer one question with no human in the loop: \emph{is this text a proof of this statement?} |
| A language model can emit text that \emph{looks} like a proof indefinitely; we need a checker whose acceptance is an |
| \emph{unforgeable} certificate. Curry--Howard turns ``is this a proof?'' into ``does this term have this type?'', which |
| is a decidable, mechanical question answered by a very small program (the kernel). Everything else in the Lean pipeline |
| (tactics, automation, an LLM) is allowed to be wrong, because its output is re-checked by that small program. |
| The price: the guarantee holds only \emph{relative to} the kernel, the axioms the term depends on, and the statement that was typed. |
| This note makes each of the three precise; notes 0302--0305 deal with the statement. |
|
|
| |
| \end{problem} |
| \stepcounter{section} |
|
|
| \section{Notation} |
| \begin{center}\small |
| \begin{tabular}{@{}lp{9.6cm}@{}}\toprule |
| Symbol & Meaning\\\midrule |
| $p,q,a,b$ & atomic propositions (atoms); $\bot$ is falsity\\ |
| $A,B,C$ & propositions = types, built from atoms and $\bot$ by $A\to B$\\ |
| $\Gamma$ & context: finite map from variables to types, $x_1{:}A_1,\dots,x_n{:}A_n$\\ |
| $\Gamma\vdash t:A$ & typing judgement: in context $\Gamma$ the term $t$ has type $A$\\ |
| $t[x{:=}u]$ & capture-avoiding substitution of $u$ for $x$ in $t$\\ |
| $t\rightsquigarrow t'$ & one reduction step ($\beta$ or commuting conversion, \S3.3)\\ |
| $\mathrm{abort}_A\,e$ & ex falso: from $e:\bot$ produce a term of any type $A$\\ |
| $\mathcal A_{\mathrm{ok}}$ & allowed axiom set $\{\texttt{propext},\texttt{Quot.sound},\texttt{Classical.choice}\}$\\ |
| $\mathrm{Ax}(c)$ & set of axioms in the dependency closure of constant $c$ (\texttt{\#print axioms})\\ |
| $R(c)$ & reward $=\mathbf 1[\text{kernel accepts }c\ \wedge\ \mathrm{Ax}(c)\subseteq\mathcal A_{\mathrm{ok}}]$\\ |
| $v\models A$ & classical truth of $A$ under valuation $v:\text{atoms}\to\{0,1\}$\\ |
| $w\Vdash A$ & Kripke forcing at world $w$ (\S3.4)\\\bottomrule |
| \end{tabular} |
| \end{center} |
|
|
| |
| \section{Derivation} |
| \subsection{The BHK reading: what a proof \emph{is}} |
| Take ``a proof of $A\to B$ is a construction that turns any proof of $A$ into a proof of $B$'' (Brouwer--Heyting--Kolmogorov) |
| as the \emph{definition}. A construction that turns inputs into outputs is a function, so: |
| \begin{center}\small\begin{tabular}{@{}ll@{}}\toprule |
| proposition & a proof of it is\\\midrule |
| $\bot$ & (nothing: there is no proof)\\ |
| $A\to B$ & a function from proofs of $A$ to proofs of $B$\\ |
| $A\wedge B$ & a pair (proof of $A$, proof of $B$)\\ |
| $A\vee B$ & a tagged proof of $A$ or of $B$\\ |
| $\forall x{:}X,\,P(x)$ & a function sending each $x$ to a proof of $P(x)$ (a dependent function, \S0302)\\ |
| $\exists x{:}X,\,P(x)$ & a pair (witness $x$, proof of $P(x)$)\\\bottomrule\end{tabular}\end{center} |
| We work in the smallest fragment that already shows every phenomenon: $A::=p\mid\bot\mid A\to B$. |
|
|
| \subsection{Typing rules = natural-deduction rules} |
| Terms: $t::=x\mid\lambda x{:}A.\,t\mid t\,u\mid\mathrm{abort}_A\,t$. The four typing rules are |
| \[ |
| \frac{x{:}A\in\Gamma}{\Gamma\vdash x:A}\;(\mathrm{Var})\qquad |
| \frac{\Gamma,x{:}A\vdash t:B}{\Gamma\vdash\lambda x{:}A.\,t:A\to B}\;(\to\!\mathrm I)\qquad |
| \frac{\Gamma\vdash f:A\to B\quad\Gamma\vdash u:A}{\Gamma\vdash f\,u:B}\;(\to\!\mathrm E)\qquad |
| \frac{\Gamma\vdash e:\bot}{\Gamma\vdash\mathrm{abort}_A\,e:A}\;(\bot\mathrm E). |
| \] |
| Erase the terms and the rules are exactly the natural-deduction rules for implication and ex falso: assumption, implication |
| introduction (discharge the assumption $x{:}A$), modus ponens, and $\bot$-elimination. |
|
|
| \begin{proposition}[Curry--Howard on derivations]\label{prop:ch} |
| $\Gamma\vdash_{\mathrm{ND}}A$ (a natural-deduction derivation with undischarged assumptions $\Gamma$) iff there is $t$ with $\Gamma\vdash t:A$. |
| \end{proposition} |
| \emph{Proof.} ($\Leftarrow$) Induction on the typing derivation: the last rule is one of the four rules; erasing terms gives the |
| corresponding ND rule applied to the ND derivations obtained from the premises by the induction hypothesis. |
| ($\Rightarrow$) Induction on the ND derivation: assumption $\mapsto x$; $\to$I applied to a derivation with term $t$ $\mapsto\lambda x{:}A.\,t$; |
| $\to$E applied to derivations with terms $f,u$ $\mapsto f\,u$; $\bot$E $\mapsto\mathrm{abort}_A\,t$. Each step is the identity on rule shape. $\square$ |
|
|
| So \emph{a type is provable iff it is inhabited}, and a proof is a term. Two examples, with the types the notebook's kernel |
| (\texttt{infer}) reads off: |
| $K=\lambda x{:}A.\lambda y{:}B.\,x : A\to B\to A$, and $S=\lambda f.\lambda g.\lambda x.\,(f\,x)(g\,x):(A\to B\to C)\to(A\to B)\to A\to C$. |
|
|
| \subsection{Proof normalisation: a detour is a redex} |
| An introduction immediately followed by the matching elimination is a \emph{detour}: ``prove $B$ from a hypothesis $x{:}A$, close it up to $A\to B$, then |
| apply it to a proof $u$ of $A$.'' The shortcut is to plug $u$ in for the hypothesis. As terms: |
| \[ |
| (\lambda x{:}A.\,t)\,u\;\rightsquigarrow_\beta\;t[x{:=}u],\qquad |
| (\mathrm{abort}_{A\to B}\,e)\,u\;\rightsquigarrow\;\mathrm{abort}_B\,e\quad(\text{commuting conversion}). |
| \] |
| The second rule removes an elimination applied to an ex-falso proof of an implication; it is needed so that normal forms have a |
| clean shape (\S3.5). |
|
|
| \begin{lemma}[Substitution]\label{lem:subst} |
| If $\Gamma,x{:}A\vdash t:B$ and $\Gamma\vdash u:A$ then $\Gamma\vdash t[x{:=}u]:B$. |
| \end{lemma} |
| \emph{Proof.} Induction on $t$ (bound variables renamed apart, the Barendregt convention). |
| \emph{Var $y$:} if $y=x$ then $B=A$ and $t[x{:=}u]=u:A$. If $y\neq x$ then $y{:}B\in\Gamma$ and $t[x{:=}u]=y$. |
| \emph{$\lambda y{:}C.\,s$:} $B=C\to D$ with $\Gamma,x{:}A,y{:}C\vdash s:D$. By weakening $\Gamma,y{:}C\vdash u:A$, so by IH $\Gamma,y{:}C\vdash s[x{:=}u]:D$ and $\to$I gives the claim. |
| \emph{$f\,s$} and \emph{$\mathrm{abort}$:} immediate from IH on subterms. $\square$ |
|
|
| \begin{theorem}[Subject reduction]\label{thm:sr} |
| If $\Gamma\vdash t:A$ and $t\rightsquigarrow t'$ then $\Gamma\vdash t':A$. |
| \end{theorem} |
| \emph{Proof.} Induction on the derivation of $t\rightsquigarrow t'$. |
| \emph{$\beta$:} $t=(\lambda x{:}C.\,s)\,u$. Inversion of $\to$E and $\to$I gives $\Gamma,x{:}C\vdash s:A$ and $\Gamma\vdash u:C$; Lemma~\ref{lem:subst} gives $\Gamma\vdash s[x{:=}u]:A$. |
| \emph{Commuting conversion:} $t=(\mathrm{abort}_{C\to A}\,e)\,u$; inversion gives $\Gamma\vdash e:\bot$, so $\Gamma\vdash\mathrm{abort}_A\,e:A$ by $\bot$E. |
| \emph{Congruence} (reduction inside $\lambda$, application, abort): the premise type is unchanged by IH, so the same rule re-applies. $\square$ |
|
|
| Subject reduction is what makes ``simplify the proof'' safe: normalising never changes \emph{which} proposition is proved. |
|
|
| \subsection{Consistency: no closed term inhabits $\bot$} |
| \begin{lemma}[Closed normal forms]\label{lem:cnf} |
| Every closed $\rightsquigarrow$-normal typable term is a $\lambda$-abstraction. |
| \end{lemma} |
| \emph{Proof.} Induction on the term. A variable is not closed. $\mathrm{abort}_A\,e$: $e$ is closed and normal, so by IH it is a $\lambda$, hence has an arrow type, contradicting $e:\bot$; so this case cannot occur. An application $f\,u$ with $f,u$ closed and normal: by IH $f$ is a $\lambda$, so $f\,u$ is a $\beta$-redex, contradicting normality. Only $\lambda$ remains. $\square$ |
|
|
| \begin{theorem}[Consistency]\label{thm:cons} |
| There is no $t$ with $\vdash t:\bot$. |
| \end{theorem} |
| \emph{Proof.} We \emph{assume} strong normalisation of $\rightsquigarrow$ on typable terms (Tait's reducibility argument, \cite{tait67}; we do not re-derive it, and the notebook only checks it by fuel on 3000 random terms). Normalise $t$ to $t'$; by Theorem~\ref{thm:sr}, $\vdash t':\bot$ with $t'$ closed and normal. By Lemma~\ref{lem:cnf}, $t'$ is a $\lambda$, so its type is an arrow, not $\bot$. Contradiction. $\square$ |
|
|
| \paragraph{A semantic check (soundness) and its failure of converse.} |
| Classical truth: $v\models\bot$ never; $v\models A\to B$ iff $v\not\models A$ or $v\models B$. |
| \begin{theorem}[Classical soundness]\label{thm:sound} |
| If $\Gamma\vdash t:A$ and $v\models\Gamma$ (every type in $\Gamma$ is true under $v$) then $v\models A$. In particular every inhabited closed type is a tautology. |
| \end{theorem} |
| \emph{Proof.} Induction on the derivation. Var: $v\models\Gamma$ gives $v\models A$. $\to$I: if $v\models A$ then $v\models\Gamma,x{:}A$ so IH gives $v\models B$; hence $v\models A\to B$. $\to$E: $v\models A\to B$ and $v\models A$ give $v\models B$. $\bot$E: $v\models\bot$ is impossible, so the implication holds vacuously. $\square$ |
|
|
| The converse is \emph{false}: Peirce's law $((a\to b)\to a)\to a$ is a tautology (if $v\models a$ the conclusion holds; if $v\not\models a$ then $v\models a\to b$ for every $b$, so the hypothesis $(a\to b)\to a$ would need $a$, so it is false, and the implication holds) yet it is uninhabited. To see this one uses Kripke semantics: worlds with a preorder $\le$, atoms monotone in $w$, and |
| \[ |
| w\Vdash A\to B\iff\forall w'\ge w:\ w'\Vdash A\Rightarrow w'\Vdash B,\qquad w\not\Vdash\bot. |
| \] |
| The same induction as Theorem~\ref{thm:sound} (using monotonicity: $w\Vdash A$ and $w\le w'$ imply $w'\Vdash A$) shows that inhabited types are forced at every world of every model. |
| Countermodel for Peirce: two worlds $w_0\le w_1$; $a$ true only at $w_1$; $b$ true nowhere. At $w_1$: $w_1\Vdash a$, $w_1\not\Vdash a\to b$. At $w_0$: $w_0\not\Vdash a\to b$ (witness $w_1$). Hence $w_0\Vdash(a\to b)\to a$ vacuously, but $w_0\not\Vdash a$, so $w_0\not\Vdash$ Peirce. |
|
|
| \subsection{Search procedures (what the notebook implements)} |
| \emph{Naive.} Every normal term of atomic type has shape $x\,n_1\cdots n_k$ or $\mathrm{abort}_A(x\,n_1\cdots n_k)$ with $x$ a variable; every normal term of arrow type is (after $\eta$-expansion) a $\lambda$. Enumerate by depth with backtracking. This answers only ``found within depth $D$''. |
| \emph{Efficient.} Dyckhoff's contraction-free calculus G4ip \cite{dyckhoff92} replaces the implication-left rule by four rules ($L0{\to}$: from $p$ and $p\to B$ use $B$; $L{\to}{\to}$: from $(C\to D)\to B$ prove $D$ using $C$ and $D\to B$, then continue with $B$; $L\bot{\to}$: drop $\bot\to B$; $L\bot$: close the goal from $\bot$). Each premise is smaller in a well-founded measure, so search \emph{terminates}; a failed search is therefore a proof of non-provability. The proof term is extracted rule by rule ($L{\to}{\to}$ uses $g:=\lambda d.\,f\,(\lambda\_.\,d)$) and re-checked by the independent \texttt{infer}. |
|
|
| \subsection{What the Lean kernel checks} |
| Lean's logic is the Calculus of Inductive Constructions \cite{mathlib20}: dependent function types $\Pi x{:}A.\,B(x)$ generalise $A\to B$ (note 0302), the bottom universe $\Prop$ is \emph{impredicative} (a $\Pi$ into $\Prop$ is a $\Prop$, whatever the domain) and \emph{proof-irrelevant} (any two proofs of the same proposition are definitionally equal, notebook cell ``proof irrelevance''). |
| The Lean 4 kernel \cite{lean4lean} implements the judgements $\Gamma\vdash t:A$ and definitional equality $\Gamma\vdash t\equiv t'$ (by weak-head normalisation); it also adds quotient types and, via inductive declarations, \texttt{False}, \texttt{Eq}, \texttt{And}, \texttt{Exists}, \dots A declaration $\texttt{theorem}\ c : T := v$ is accepted iff $\vdash T:\Sort\,u$ and $\vdash v:T$ (and then $c$ is added to the environment). Three consequences: |
| \begin{enumerate}[nosep] |
| \item \textbf{Tactics are untrusted.} \texttt{by omega} or \texttt{by intro; exact} is a program in the \emph{elaborator} that builds an $\mathrm{Expr}$; the kernel never sees the script. In the notebook \texttt{by omega} elaborates to a 64-line term, \texttt{by intro $\langle a,b\rangle$; exact $\langle b,a\rangle$} to \texttt{fun p q h => match h with | $\langle a,b\rangle$ => $\langle b,a\rangle$}. A buggy tactic can fail; it cannot make an ill-typed term pass. |
| \item \textbf{The trusted base is small and explicit}: the kernel, the axioms in $\mathrm{Ax}(c)$, and (for the \emph{statement}) the definitions the statement mentions. |
| \item \textbf{The theorem is only as good as the typed statement}: the kernel checks $v:T$ for the $T$ it was given, not for the $T$ in the author's head. |
| \end{enumerate} |
|
|
| \subsection{The three standard axioms, and why they are admissible} |
| \texttt{propext}: $(a\leftrightarrow b)\to a=b$ for propositions. \texttt{Quot.sound}: related elements have equal images in a quotient (it yields function extensionality: \texttt{t\_funext} uses exactly \{\texttt{Quot.sound}\} in the notebook). \texttt{Classical.choice}: $\mathrm{Nonempty}\ \alpha\to\alpha$; together with \texttt{propext} \emph{and function extensionality} (hence \texttt{Quot.sound}) it yields excluded middle by Diaconescu's argument (our \texttt{peirce\_law} term uses \texttt{Classical.em}, and \texttt{\#print axioms} reports all three: $\{\texttt{Classical.choice},\texttt{propext},\texttt{Quot.sound}\}$). |
| Their consistency is a theorem for the \emph{Lean~3} theory only: Carneiro showed Lean consistent relative to ZFC with $n$ inaccessible cardinals for all $n<\omega$ (\cite{lean4lean} \S1, ref.\ [6]). For Lean~4 the same paper says that nested inductive types and $\eta$ for structures ``significantly impact the theory'', so that ``the soundness proof from [6] is no longer directly applicable'' (\S1): consistency of Lean~4 with these axioms is therefore the assumption (K) below, supported by Lean4Lean's ongoing formalisation, not a result we can cite. Peirce's law is thereby \emph{provable in Lean} though uninhabited in the pure $\to,\bot$ calculus: Lean is not the minimal calculus, it is that calculus plus these axioms. The cost is computational: the term for Peirce contains \texttt{Classical.choice}, which has no reduction rule, so it is a proof but not a program. |
|
|
| \subsection{The reward and the three ways to forge it} |
| Let $R(c)=\mathbf 1[\vdash c\text{ accepted by the kernel}\wedge\mathrm{Ax}(c)\subseteq\mathcal A_{\mathrm{ok}}]$. |
| \begin{theorem}[Gated reward is sound]\label{thm:reward} |
| If the kernel is sound and $\mathcal A_{\mathrm{ok}}$ is consistent, then $R(c)=1$ for a constant $c$ of type $T$ implies $T$ holds in every model of CIC${}+\mathcal A_{\mathrm{ok}}$. |
| \end{theorem} |
| \emph{Proof.} $R(c)=1$ means $\vdash v:T$ in CIC extended by the axioms in $\mathrm{Ax}(c)\subseteq\mathcal A_{\mathrm{ok}}$. Soundness of the kernel (assumption K) turns a derivation into truth in every model of that theory. $\square$ |
|
|
| \begin{proposition}[Exploits collapse the reward]\label{prop:exploit} |
| (i) \texttt{sorryAx}: its type is $\Pi(\alpha{:}\Sort\,u),\ \mathrm{Bool}\to\alpha$ (notebook: \texttt{\#print sorryAx}), so $\texttt{sorryAx}\ T\ b:T$ for \emph{every} $T$, including \texttt{False}. (ii) A user \texttt{axiom evil : False} gives $\texttt{evil.elim}:T$ for every $T$. (iii) \texttt{native\_decide} introduces the axiom \texttt{Lean.ofReduceBool}$:\forall a\,b{:}\mathrm{Bool},\ \texttt{reduceBool}\ a=b\to a=b$: the kernel accepts $\texttt{reduceBool}\ a=b$ by \emph{running compiled code}, so correctness now also depends on the compiler/evaluator and on every definition's \emph{compiled} behaviour matching its \emph{logical} definition (a gap that \texttt{implemented\_by}/\texttt{unsafe} can open). |
| With any of (i)--(ii) allowed, $R(c)=1$ for every statement, so $P(R{=}1\mid T\text{ false})=P(R{=}1\mid T\text{ true})=1$: the likelihood ratio is $1$ and $R$ carries zero information about truth. |
| \end{proposition} |
| \emph{Proof.} (i), (ii): direct from the types. The information statement is Bayes' rule with equal likelihoods. $\square$ |
|
|
| \emph{Measured} (notebook, Lean 4.9.0-rc1 + Mathlib pin of this repo): for the three false statements \texttt{(1:Nat)=2}, \texttt{$\forall n,\,n<3$}, \texttt{False} the proof \texttt{sorry} compiles with a warning and has $\mathrm{Ax}=\{\texttt{sorryAx}\}$: accepted by a compile-only gate in 3/3 cases, rejected by the axiom gate in 3/3. This is rule~3 of the strict tier (\texttt{align/verify/lean/strict.py}; \texttt{docs/LEAN\_VERIFIER.md} \S2). |
|
|
| |
| \section{Boxed result} |
| \begin{result} |
| \textbf{R1 (Curry--Howard).} $\Gamma\vdash_{\mathrm{ND}}A\iff\exists t.\ \Gamma\vdash t:A$ (Prop.~\ref{prop:ch}); \textbf{R2 (subject reduction)} $\Gamma\vdash t:A,\ t\rightsquigarrow t'\Rightarrow\Gamma\vdash t':A$ (Thm.~\ref{thm:sr}); |
| \textbf{R3 (consistency and soundness)} no closed $t:\bot$; inhabited $\Rightarrow$ classically valid and Kripke-valid, converse false (Peirce); |
| \textbf{R4 (gated reward)} $R(c)=1\Rightarrow T$ true in every model of CIC$+\mathcal A_{\mathrm{ok}}$; allowing \texttt{sorryAx}, a user axiom of type \texttt{False}, or (trust-widening) \texttt{Lean.ofReduceBool} voids this. |
| \end{result} |
|
|
| \paragraph{Numerical verification (notebook 0301; all cells executed, outputs saved).} |
| \begin{center}\small |
| \begin{tabular}{@{}P{7.1cm}P{3.2cm}P{5.2cm}@{}}\toprule |
| Identity / claim & measured & value\\\midrule |
| R2: type preserved by every reduction step (3000 random typed terms, 1205 with a redex; 1431 $\beta$ and 420 commuting-conversion steps, so both cases of Thm.~\ref{thm:sr} are exercised) & violations over 1851 steps & 0\\ |
| Naive depth-14 search vs G4ip verdict on all 3873 formulas ($\le4$ arrows, atoms $a,b,\bot$) & disagreements & 0\\ |
| Every G4ip proof term re-checked by independent \texttt{infer}, and its normal form too & failures over 1775 proofs & 0\\ |
| R3: provable $\Rightarrow$ tautology (3873 formulas) & violations & 0\\ |
| R3: provable $\Rightarrow$ forced at every world of 29 chain models & violations & 0\\ |
| R3: classically valid but uninhabited (incl.\ Peirce, DNE) & count among 2098 uninhabited & 32\\ |
| R3: uninhabited types refuted by a chain model ($\le3$ worlds) & count & 2098/2098\\ |
| R4: \texttt{\#print axioms} gate on 9 theorems & accepted set & constructive, \texttt{omega}, \texttt{decide}, \texttt{funext}, \texttt{simp}, Peirce\\ |
| R4: rejected set & & \texttt{native\_decide}, \texttt{sorry}, user axiom\\ |
| Speed: G4ip vs naive on the 3873 formulas & $\times$ & 42 (0.02 s vs 1.05 s)\\\bottomrule |
| \end{tabular} |
| \end{center} |
| (``max abs error'' is not meaningful for exact symbolic identities; the table reports counts of violations, all zero.) |
| A side observation from the same run: \texttt{2\^{}10 = 1024 := by decide} reports $\mathrm{Ax}=\{\texttt{propext}\}$ on this pin; it is inside $\mathcal A_{\mathrm{ok}}$, but shows that ``\texttt{decide} uses no axioms'' is not a safe belief, which is why the gate reads the real dependency closure rather than assuming it. |
|
|
| |
| \section{What breaks} |
| \begin{center}\small |
| \begin{tabular}{@{}P{3.6cm}P{6.3cm}P{5.6cm}@{}}\toprule |
| Failure & Mechanism & Assumption violated\\\midrule |
| Kernel soundness bug & Lean 4's kernel has had soundness bugs; Lean4Lean found one \emph{by failing to prove a theorem}: an overflow check in \texttt{Expr.data} used \texttt{panic!}, which continues with $0$ for \texttt{UInt64}, switching on an optimisation in \texttt{hasLooseBVars} \cite{lean4lean} \S4.1 & (K) kernel soundness. Mitigation: external checkers (Lean4Lean, Comparator \cite{comparator})\\ |
| \texttt{sorry}/\texttt{admit} & \texttt{sorryAx} inhabits every type & $\mathrm{Ax}(c)\subseteq\mathcal A_{\mathrm{ok}}$; compile warnings are not a gate\\ |
| User \texttt{axiom}, \texttt{opaque} with a false type, \texttt{unsafe} & enlarges the theory & same; also lexical bans can be evaded, so read $\mathrm{Ax}(c)$ from the environment\\ |
| \texttt{native\_decide} & trusts compiled evaluation (\texttt{Lean.ofReduceBool}) & the kernel is the only evaluator trusted\\ |
| Meta-programming / environment edits & meta-programs run inside the elaborator with access to the environment; a lexical ban cannot enumerate every route, and \texttt{debug.skipKernelTC}-style switches exist upstream (not an option on this pin) & the elaborator is untrusted and the kernel \emph{does} check; so re-check with kernel-forced-on\\ |
| Wrong \emph{statement} typed & kernel certifies $v:T$ for the given $T$ & the statement means what the author intended (0302, 0305)\\ |
| Classical axioms & proof is not a program (\texttt{Classical.choice} has no reduction) & only matters if the proof is meant to be run\\\bottomrule |
| \end{tabular} |
| \end{center} |
| The audit literature agrees on the category: the \emph{kernel only checks that a proof establishes a formal statement; it does not verify that the statement faithfully encodes the intended informal problem}, and mechanically certified faults include ``counterexamples, vacuous theorems, and unsound axioms'' (\cite{faults26}, abstract). |
|
|
| \nextnote{0302 asks what a Lean \emph{statement} actually is: dependent function types, \texttt{Prop} versus \texttt{Type}, decidability, and ten miniF2F statements decoded binder by binder.} |
|
|
| |
| \begin{small} |
| \begin{thebibliography}{99} |
| \bibitem{lean4lean} M.~Carneiro, \emph{Lean4Lean: Verifying a Typechecker for Lean, in Lean}, arXiv:2403.14064. \S1 (soundness bugs in Lean~4's kernel; relative consistency of the Lean~3 theory with ZFC$+n$ inaccessibles, ref.\ [6]; that proof is ``no longer directly applicable'' to Lean~4); \S4.1 (``Bit tricks and soundness bugs'', \texttt{looseBVarRange}, \texttt{panic!}); \S5 (``The global environment'': the \texttt{VDecl} declaration forms \texttt{block}, \texttt{axiom}, \texttt{opaque}, \dots). |
| \bibitem{mathlib20} The mathlib Community, \emph{The Lean Mathematical Library}, arXiv:1910.09336. \S2 (CIC, universe hierarchy, impredicative and proof-irrelevant \texttt{Prop}; the axioms \texttt{choice} and \texttt{propext}, quotients); \S4.2 (the \texttt{decidable} class). Describes Lean~3; Lean~4 keeps the same logic. |
| \bibitem{faults26} P.~S.~Ammanamanchi, S.~Bhat, S.~Biderman, \emph{Faults in Our Formal Benchmarking}, arXiv:2606.29493 (ICML 2026), abstract. |
| \bibitem{comparator} Lean FRO, \texttt{leanprover/comparator}. Not an arXiv paper and the repository was not fetched; as described in \cite{faults26} it is ``a trusted evaluator that checks proofs against a conservative set of axioms and disallows potentially unsafe tactics like \texttt{native\_decide}'' (the specific default axiom list and the sandboxing are not verified here). |
| \bibitem{tait67} W.~W.~Tait, ``Intensional interpretations of functionals of finite type I'', J.\ Symbolic Logic 32 (1967). Strong normalisation by reducibility. \emph{Not on arXiv; not fetched; cited only for the named theorem, which this note assumes.} |
| \bibitem{dyckhoff92} R.~Dyckhoff, ``Contraction-free sequent calculi for intuitionistic logic'', J.\ Symbolic Logic 57 (1992). \emph{Not on arXiv; not fetched; the notebook cross-checks G4ip against naive search and Kripke models rather than relying on the citation.} |
| \bibitem{howard80} W.~A.~Howard, ``The formulae-as-types notion of construction'' (1980); H.~B.~Curry, R.~Feys, \emph{Combinatory Logic} I (1958). \emph{Not on arXiv; not fetched; historical attribution of Prop.~\ref{prop:ch}, whose proof is given above.} |
| \bibitem{house} This repository: \texttt{align/docs/LEAN\_VERIFIER.md} \S2 (strict tier, axiom audit), \texttt{align/verify/lean/strict.py} (rule 3). |
| \end{thebibliography} |
| \end{small} |
| \end{document} |
|
|
