\documentclass[12pt, reqno, twoside, letterpaper]{amsart}

%% ---------------------------------------------------------------
%% x-Paperstyle.sty, inlined verbatim for single-file submission
%% ---------------------------------------------------------------
%====================
% x-Paperstyle.sty
% Kit version of 1 Sep 2026.
%====================

%%%--------------------
%%% Packages
%%%--------------------

% Core math + symbols + references.
\usepackage{amsmath,amssymb,amsbsy,amsfonts,amsthm,latexsym,amsopn,amstext,amsxtra,euscript,amscd,stmaryrd,mathrsfs,cite,array}
\usepackage{bbm} % Blackboard-bold digits, e.g. \mathbbm{1} for the indicator.

% Color.
\usepackage{color}
\usepackage[usenames,dvipsnames,svgnames,table]{xcolor}

% Additional named colors (the dvipsnames/svgnames sets are already available;
% these are extras tuned for readable on-screen markup).
\definecolor{ForestGreen}{RGB}{34,139,34}
\definecolor{DarkGreen}{RGB}{0,100,0}
\definecolor{Teal}{RGB}{0,128,128}
\definecolor{Navy}{RGB}{0,0,128}
\definecolor{RoyalBlue}{RGB}{65,105,225}
\definecolor{SkyBlue}{RGB}{70,130,220}
\definecolor{Indigo}{RGB}{75,0,130}
\definecolor{Purple}{RGB}{128,0,128}
\definecolor{Violet}{RGB}{148,0,211}
\definecolor{Crimson}{RGB}{220,20,60}
\definecolor{BrickRed}{RGB}{178,34,34}
\definecolor{BurntOrange}{RGB}{204,85,0}
\definecolor{Amber}{RGB}{255,153,0}
\definecolor{Olive}{RGB}{128,128,0}
\definecolor{Maroon}{RGB}{128,0,0}
\definecolor{SlateGray}{RGB}{112,128,144}
\definecolor{DarkGray}{RGB}{64,64,64}
\definecolor{MidGray}{RGB}{128,128,128}

% Page layout & spacing.
\usepackage[text={6.25in,9.5in},centering]{geometry}
\usepackage{setspace}

% Margin todo notes.
\usepackage[colorinlistoftodos]{todonotes}
% Adjust if you see a todonotes margin width warning.
\setlength{\marginparwidth}{2cm}

% Optional: show labels in PDF.
%\usepackage{showkeys}

% Bold citations (cite package).
\renewcommand{\citeform}[1]{\textbf{#1}} % Bold citations.

% Hyperlinks (load late).
\usepackage[colorlinks,linkcolor=blue,anchorcolor=blue,
citecolor=blue,backref=page]{hyperref}
\hypersetup{breaklinks=true}

% Backref formatting.
\renewcommand*{\backref}[1]{}
\renewcommand*{\backrefalt}[4]{%
    \ifcase #1 (Not cited.)%
    \or        (p.\,#2)%
    \else      (pp.\,#2)%
    \fi}


%%%--------------------
%%% Headings, floats, and page-break hygiene
%%%--------------------

% Floats never drift past the end of their section.
\usepackage[section]{placeins}

\usepackage{etoolbox}
\usepackage{needspace}

\makeatletter
% amsart only: larger, centered small-caps section titles with extra
% space above (adjust the 1.2 to taste; 2.5 for a roomier preprint).
\@ifclassloaded{amsart}{%
  \def\section{\@startsection{section}{1}%
    \z@{1.2\linespacing\@plus\linespacing}{.5\linespacing}%
    {\normalfont\large\scshape\centering}}%
}{}
% LaTeX suppresses the space above a theorem, lemma, or proof that
% directly follows a heading; this restores it.
\newcommand{\restore@headskip}{\if@nobreak\vskip\medskipamount\fi}
\pretocmd{\@thm}{\restore@headskip}{}{}
\AtBeginEnvironment{proof}{\restore@headskip}
% A heading is kept with the text that follows it, so that no page
% ends with a heading alone.
\pretocmd{\section}{\par\Needspace*{4\baselineskip}}{}{}
\pretocmd{\subsection}{\par\Needspace*{3\baselineskip}}{}{}
\makeatother


%%%--------------------
%%% Global formatting / numbering
%%%--------------------

\numberwithin{equation}{section}

\setlength{\parindent}{15pt}


%%%--------------------
%%% Custom theorem environments
%%%--------------------

\newtheoremstyle{customthm}
{1em}                    % ABOVESPACE
{1em}                    % BELOWSPACE
{\itshape}               % BODYFONT
{}                       % INDENT
{\scshape}               % HEADFONT
{.}                      % HEADPUNCT
{5pt plus 1pt minus 1pt} % HEADSPACE
{}                       % CUSTOM-HEAD-SPEC

\theoremstyle{customthm}

\newtheorem{X}{X}[section]
\newtheorem{theorem}[X]{Theorem}  
\newtheorem{definition}{Definition}
\newtheorem{lemma}[X]{Lemma}
\newtheorem{corollary}[X]{Corollary}
\newtheorem{conjecture}[X]{Conjecture}
\newtheorem{proposition}[X]{Proposition}
\newtheorem{remark}[X]{Remark}
\newtheorem{remarks}[X]{Remarks}

\newtheorem*{theorem*}{Theorem}  
\newtheorem*{definition*}{Definition}
\newtheorem*{lemma*}{Lemma}
\newtheorem*{corollary*}{Corollary}
\newtheorem*{conjecture*}{Conjecture}
\newtheorem*{proposition*}{Proposition}
\newtheorem*{remark*}{Remark}
\newtheorem*{remarks*}{Remarks}


%%%--------------------
%%% Commenting / markups
%%%--------------------

% \long so the argument may contain blank lines / multiple paragraphs.
% Uses the \color switch (not \textcolor) since \textcolor is not \long.
\long\def\cc#1{{\color{Red}#1}} % Color text red
\long\def\ccb#1{{\color{Blue}#1}} % Color text blue
\long\def\ccg#1{{\color{Green}#1}} % Color text green
\long\def\cco#1{{\color{Orange}#1}} % Color text orange
\long\def\ccm#1{{\color{Magenta}#1}} % Color text magenta
\newcommand{\xxx}{\vskip3pt\hrule\vskip3pt} % Draw line
\newcommand{\imhere}{\textcolor{Blue}
	{ \xxx\centerline{\footnotesize\bf I'm here}\xxx }} % Present location
\newcommand{\incomment}[1]{\textcolor{DarkMagenta}
	{ \xxx\centerline{\footnotesize\bf #1}\xxx }} % In-line comment

% Margin comment using todonotes.
\newcommand{\comm}[2][]{\todo[#1,color=green!24]{#2}}

% Draft toggle for magenta "to be studied / incorporated" material.
% Default is \drafttrue; put \draftfalse in the document preamble for a
% clean build with every \td and \tdpar removed. Each \td or \tdpar is
% an open task, not prose; each \comm is an open task on the same footing.
\newif\ifdraft
\drafttrue
\long\def\td#1{\ifdraft\ccm{#1}\fi}          % In-line task, magenta
\long\def\tdpar#1{\ifdraft\par\noindent\ccm{#1}\par\fi} % Task paragraph

%%%--------------------
%%% General math macros / symbols
%%%--------------------

\newcommand{\eps}{\varepsilon }
\newcommand{\mand}{\qquad\mbox{and}\qquad }
\newcommand{\fl}[1]{{\ensuremath{\big\lfloor #1 \big\rfloor}} }
\newcommand{\rf}[1]{{\ensuremath{\big\lceil #1 \big\rceil}} }
\renewcommand{\(}{\ensuremath{\left(} }
\renewcommand{\)}{\ensuremath{\right)} }
\newcommand{\ind}[1]{\ensuremath{\text{\usefont{U}{bbm}{m}{n}\selectfont 1}_{#1}}}% Indicator function (blackboard bold 1)
\newcommand{\e}{{\tt e}}
\newcommand{\er}{\mathrm{e}}
\renewcommand{\le}{\ensuremath{\leqslant} }
\renewcommand{\ge}{\ensuremath{\geqslant} }
\renewcommand{\leq}{\ensuremath{\leqslant} }
\renewcommand{\geq}{\ensuremath{\geqslant} }
\newcommand{\ssum}[1]{\sum_{\substack{#1}}} % stacked sum
\newcommand{\sprod}[1]{\prod_{\substack{#1}}} % stacked product
\newcommand{\dalign}[1]{\[\begin{aligned} #1\end{aligned}\]}
\newcommand{\be}{\begin{equation}}
\newcommand{\ee}{\end{equation}}
% Provide \vcentcolon if not available (e.g., when mathtools isn't loaded).
\providecommand{\vcentcolon}{\mathrel{\mathop{:}}}


\newcommand{\defeq}{\vcentcolon=}
\newcommand{\eqdef}{=\vcentcolon}
\newcommand{\llsym}[1]{\,\mathop{\ll}\limits_{#1}\,}
\newcommand{\ggsym}[1]{\,\mathop{\gg}\limits_{#1}\,}
\newcommand{\asympsym}[1]{\,\mathop{\asymp}\limits_{#1}\,}
\newcommand{\llbracks}[2]{\llbracket #1 \rrbracket_{#2}}


%%%--------------------
%%% Alphabets
%%%--------------------

%%% CALLIGRAPHIC ALPHABET %%%

\newcommand{\cA}{\ensuremath{\mathcal{A}} }
\newcommand{\cB}{\ensuremath{\mathcal{B}} }
\newcommand{\cC}{\ensuremath{\mathcal{C}} }
\newcommand{\cD}{\ensuremath{\mathcal{D}} }
\newcommand{\cE}{\ensuremath{\mathcal{E}} }
\newcommand{\cF}{\ensuremath{\mathcal{F}} }
\newcommand{\cG}{\ensuremath{\mathcal{G}} }
\newcommand{\cH}{\ensuremath{\mathcal{H}} }
\newcommand{\cI}{\ensuremath{\mathcal{I}} }
\newcommand{\cJ}{\ensuremath{\mathcal{J}} }
\newcommand{\cK}{\ensuremath{\mathcal{K}} }
\newcommand{\cL}{\ensuremath{\mathcal{L}} }
\newcommand{\cM}{\ensuremath{\mathcal{M}} }
\newcommand{\cN}{\ensuremath{\mathcal{N}} }
\newcommand{\cO}{\ensuremath{\mathcal{O}} }
\newcommand{\cP}{\ensuremath{\mathcal{P}} }
\newcommand{\cQ}{\ensuremath{\mathcal{Q}} }
\newcommand{\cR}{\ensuremath{\mathcal{R}} }
\newcommand{\cS}{\ensuremath{\mathcal{S}} }
\newcommand{\cU}{\ensuremath{\mathcal{U}} }
\newcommand{\cT}{\ensuremath{\mathcal{T}} }
\newcommand{\cV}{\ensuremath{\mathcal{V}} }
\newcommand{\cW}{\ensuremath{\mathcal{W}} }
\newcommand{\cX}{\ensuremath{\mathcal{X}} }
\newcommand{\cY}{\ensuremath{\mathcal{Y}} }
\newcommand{\cZ}{\ensuremath{\mathcal{Z}} }

%%% SCRIPT ALPHABET %%%

\newcommand{\sA}{\ensuremath{\mathscr{A}} }
\newcommand{\sB}{\ensuremath{\mathscr{B}} }
\newcommand{\sC}{\ensuremath{\mathscr{C}} }
\newcommand{\sD}{\ensuremath{\mathscr{D}} }
\newcommand{\sE}{\ensuremath{\mathscr{E}} }
\newcommand{\sF}{\ensuremath{\mathscr{F}} }
\newcommand{\sG}{\ensuremath{\mathscr{G}} }
\newcommand{\sH}{\ensuremath{\mathscr{H}} }
\newcommand{\sI}{\ensuremath{\mathscr{I}} }
\newcommand{\sJ}{\ensuremath{\mathscr{J}} }
\newcommand{\sK}{\ensuremath{\mathscr{K}} }
\newcommand{\sL}{\ensuremath{\mathscr{L}} }
\newcommand{\sM}{\ensuremath{\mathscr{M}} }
\newcommand{\sN}{\ensuremath{\mathscr{N}} }
\newcommand{\sO}{\ensuremath{\mathscr{O}} }
\newcommand{\sP}{\ensuremath{\mathscr{P}} }
\newcommand{\sQ}{\ensuremath{\mathscr{Q}} }
\newcommand{\sR}{\ensuremath{\mathscr{R}} }
\newcommand{\sS}{\ensuremath{\mathscr{S}} }
\newcommand{\sU}{\ensuremath{\mathscr{U}} }
\newcommand{\sT}{\ensuremath{\mathscr{T}} }
\newcommand{\sV}{\ensuremath{\mathscr{V}} }
\newcommand{\sW}{\ensuremath{\mathscr{W}} }
\newcommand{\sX}{\ensuremath{\mathscr{X}} }
\newcommand{\sY}{\ensuremath{\mathscr{Y}} }
\newcommand{\sZ}{\ensuremath{\mathscr{Z}} }

%%% EUSCRIPT ALPHABET %%%

% Distinct from the \mathscr alphabet above; the euscript package is
% loaded with the core packages. Defined without a trailing space.

\newcommand{\euA}{\ensuremath{\EuScript{A}}}
\newcommand{\euB}{\ensuremath{\EuScript{B}}}
\newcommand{\euC}{\ensuremath{\EuScript{C}}}
\newcommand{\euD}{\ensuremath{\EuScript{D}}}
\newcommand{\euE}{\ensuremath{\EuScript{E}}}
\newcommand{\euF}{\ensuremath{\EuScript{F}}}
\newcommand{\euG}{\ensuremath{\EuScript{G}}}
\newcommand{\euH}{\ensuremath{\EuScript{H}}}
\newcommand{\euI}{\ensuremath{\EuScript{I}}}
\newcommand{\euJ}{\ensuremath{\EuScript{J}}}
\newcommand{\euK}{\ensuremath{\EuScript{K}}}
\newcommand{\euL}{\ensuremath{\EuScript{L}}}
\newcommand{\euM}{\ensuremath{\EuScript{M}}}
\newcommand{\euN}{\ensuremath{\EuScript{N}}}
\newcommand{\euO}{\ensuremath{\EuScript{O}}}
\newcommand{\euP}{\ensuremath{\EuScript{P}}}
\newcommand{\euQ}{\ensuremath{\EuScript{Q}}}
\newcommand{\euR}{\ensuremath{\EuScript{R}}}
\newcommand{\euS}{\ensuremath{\EuScript{S}}}
\newcommand{\euT}{\ensuremath{\EuScript{T}}}
\newcommand{\euU}{\ensuremath{\EuScript{U}}}
\newcommand{\euV}{\ensuremath{\EuScript{V}}}
\newcommand{\euW}{\ensuremath{\EuScript{W}}}
\newcommand{\euX}{\ensuremath{\EuScript{X}}}
\newcommand{\euY}{\ensuremath{\EuScript{Y}}}
\newcommand{\euZ}{\ensuremath{\EuScript{Z}}}

%%% FRAKTUR ALPHABET %%%

\newcommand{\fA}{\ensuremath{\mathfrak{A}} }
\newcommand{\fB}{\ensuremath{\mathfrak{B}} }
\newcommand{\fC}{\ensuremath{\mathfrak{C}} }
\newcommand{\fD}{\ensuremath{\mathfrak{D}} }
\newcommand{\fE}{\ensuremath{\mathfrak{E}} }
\newcommand{\fF}{\ensuremath{\mathfrak{F}} }
\newcommand{\fG}{\ensuremath{\mathfrak{G}} }
\newcommand{\fH}{\ensuremath{\mathfrak{H}} }
\newcommand{\fI}{\ensuremath{\mathfrak{I}} }
\newcommand{\fJ}{\ensuremath{\mathfrak{J}} }
\newcommand{\fK}{\ensuremath{\mathfrak{K}} }
\newcommand{\fL}{\ensuremath{\mathfrak{L}} }
\newcommand{\fM}{\ensuremath{\mathfrak{M}} }
\newcommand{\fN}{\ensuremath{\mathfrak{N}} }
\newcommand{\fO}{\ensuremath{\mathfrak{O}} }
\newcommand{\fP}{\ensuremath{\mathfrak{P}} }
\newcommand{\fQ}{\ensuremath{\mathfrak{Q}} }
\newcommand{\fR}{\ensuremath{\mathfrak{R}} }
\newcommand{\fS}{\ensuremath{\mathfrak{S}} }
\newcommand{\fU}{\ensuremath{\mathfrak{U}} }
\newcommand{\fT}{\ensuremath{\mathfrak{T}} }
\newcommand{\fV}{\ensuremath{\mathfrak{V}} }
\newcommand{\fW}{\ensuremath{\mathfrak{W}} }
\newcommand{\fX}{\ensuremath{\mathfrak{X}} }
\newcommand{\fY}{\ensuremath{\mathfrak{Y}} }
\newcommand{\fZ}{\ensuremath{\mathfrak{Z}} }

%%% BLACKBOARD BOLD %%%

\newcommand{\B}{\ensuremath{\mathbb{B}} }
\newcommand{\C}{\ensuremath{\mathbb{C}} }
\newcommand{\F}{\ensuremath{\mathbb{F}} }
\newcommand{\K}{\ensuremath{\mathbb{K}} }
\renewcommand{\L}{\ensuremath{\mathbb{L}} }
\newcommand{\N}{\ensuremath{\mathbb{N}} }
\renewcommand{\P}{\ensuremath{\mathbb{P}} }
\newcommand{\Q}{\ensuremath{\mathbb{Q}} }
\newcommand{\R}{\ensuremath{\mathbb{R}} }
\newcommand{\V}{\ensuremath{\mathbb{V}} }
\newcommand{\Z}{\ensuremath{\mathbb{Z}} }

% Doubled blackboard-bold names, defined WITHOUT the trailing space of
% the short forms above, for use in running math where the spurious
% space is visible. \PP and \EE also avoid renewing LaTeX's \P.
\newcommand{\ZZ}{\ensuremath{\mathbb{Z}}}
\newcommand{\PP}{\ensuremath{\mathbb{P}}}
\newcommand{\EE}{\ensuremath{\mathbb{E}}}
\newcommand{\VV}{\ensuremath{\mathbb{V}}}


%%%--------------------
%%% Other symbols
%%%--------------------

%  UPRIGHT INTEGRALS  %

\newcommand{\dd}{\ensuremath{\,\mathrm{d}}} % As in \int t dt.

%% \int         will be upright (display mode)
%% \smallint    will be upright (text mode)
%
%% \oldint      will be slanted (display/text mode)
%% (\oldsmallint available, but not necessary)
%
%\let\oldintop\intop
%\def\oldint{\oldintop\nolimits}
%
%\let\oldsmallint\smallint
%
%\DeclareSymbolFont{EUEX}{U}{euex}{m}{n}
%
%\DeclareSymbolFont{euexlargesymbols}{U}{euex}{m}{n}
%\DeclareMathSymbol{\intop}{\mathop}{euexlargesymbols}{"52}
%     \def\int{\intop\nolimits}
%
%\DeclareSymbolFont{euexsymbols}     {U}{euex}{m}{n}
%\DeclareMathSymbol{\smallint}{\mathop}{euexsymbols}{"52}


%%%--------------------
%%% Suggested optional gadgets
%%%--------------------
%
% Everything below is commented out. Uncomment whatever you find useful.
% A few of these want extra packages (noted inline); those \usepackage
% lines are included in the comment block so you can lift them up top.

% --- Paired delimiters via mathtools (auto-sizing, \abs*{...} etc.) ---
% Requires: \usepackage{mathtools}
%\DeclarePairedDelimiter{\abs}{\lvert}{\rvert}       % \abs{x}, \abs*{x}
%\DeclarePairedDelimiter{\norm}{\lVert}{\rVert}      % \norm{v}
%\DeclarePairedDelimiter{\set}{\{}{\}}               % \set{x : x>0}
%\DeclarePairedDelimiter{\ip}{\langle}{\rangle}      % inner product \ip{u,v}

% --- Common operators (upright, correct spacing) ---
%\DeclareMathOperator{\Tr}{Tr}
%\DeclareMathOperator{\rank}{rank}
%\DeclareMathOperator{\supp}{supp}
%\DeclareMathOperator{\diam}{diam}
%\DeclareMathOperator{\dist}{dist}
%\DeclareMathOperator{\Var}{Var}
%\DeclareMathOperator{\Cov}{Cov}
%\DeclareMathOperator*{\argmin}{arg\,min}   % \argmin\limits_{...}
%\DeclareMathOperator*{\argmax}{arg\,max}

% --- Probability / expectation shorthands ---
%\newcommand{\E}{\ensuremath{\mathbb{E}}}          % expectation
%\newcommand{\Prob}{\ensuremath{\mathbb{P}}}       % (\P is already \mathbb{P})
%\newcommand{\given}{\mathrel{}\middle|\mathrel{}} % use inside \left. ... \right)

% --- Restriction bar: f\restr{A} ---
%\newcommand{\restr}[1]{\ensuremath{\!\upharpoonright_{#1}}}

% --- Abbreviations that fix spacing after a period ---
%\newcommand{\ie}{i.e.\@\xspace}    % requires \usepackage{xspace}
%\newcommand{\eg}{e.g.\@\xspace}    % requires \usepackage{xspace}
%\newcommand{\cf}{cf.\@\xspace}     % requires \usepackage{xspace}

% --- QED-style end-of-proof markers you can drop mid-text ---
%\newcommand{\qedbox}{\hfill$\square$}

% --- A "highlight" markup that shades text (screen review) ---
% Requires: \usepackage{soul} (and soul's \sethlcolor)
%\newcommand{\hl}[1]{\colorbox{yellow!40}{#1}}     % simple boxed highlight

% --- Strike-through for deletions in revision (screen review) ---
% Requires: \usepackage{soul}
%\newcommand{\del}[1]{\textcolor{MidGray}{\st{#1}}}

% --- Numbered "TODO" counter in the margin, distinct from \comm ---
%\newcommand{\TODO}[1]{\todo[color=red!30]{\textbf{TODO:} #1}}

% --- Autoref name tweaks so \cref/\autoref read nicely ---
% Requires: \usepackage{cleveref} (load AFTER hyperref)
%\crefname{equation}{Eq.}{Eqs.}
%\crefname{theorem}{Theorem}{Theorems}
%\crefname{lemma}{Lemma}{Lemmas}

% --- Quick vector/matrix builders ---
%\newcommand{\vect}[1]{\ensuremath{\boldsymbol{#1}}} % bold vector
%\newcommand{\smat}[1]{\left(\begin{smallmatrix}#1\end{smallmatrix}\right)} % inline matrix

% --- "Big-O family" with consistent spacing ---
%\newcommand{\bigO}{\ensuremath{O}}
%\newcommand{\smallo}{\ensuremath{o}}
%\newcommand{\Om}{\ensuremath{\Omega}}
%\newcommand{\Th}{\ensuremath{\Theta}}

% --- Numbered equation shorthand with a label ---
%\newcommand{\bel}[1]{\begin{equation}\label{#1}}   % \bel{eq:foo} ... \ee
%% ---------------------------------------------------------------
%% End of inlined x-Paperstyle.sty
%% ---------------------------------------------------------------
% Uncomment as needed.
%\usepackage{mathtools}
%\usepackage{graphicx}
%\usepackage{booktabs}
%\usepackage{tikz}

% Draft toggle (defined in x-Paperstyle). Every \td{...} and \tdpar{...}
% is an open task. Switch to \draftfalse for a clean build.
\draftfalse

%% ---------------------------------------------------------------
%% Paper-specific macros
%% ---------------------------------------------------------------
\newcommand{\Con}{\mathrm{Con}}
\newcommand{\ZFC}{\mathsf{ZFC}}
\newcommand{\Lean}{\mathsf{Lean}}
\newcommand{\False}{\mathtt{False}}
\newcommand{\LProp}{\mathtt{Prop}}
\newcommand{\LType}{\mathtt{Type}}
\newcommand{\sem}[1]{\llbracket #1 \rrbracket}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  PAPER STARTS HERE  %%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title[A theorem Lean can state but never verify]{A true theorem Lean
can state but can never verify}

\author{William D. Banks}
\address{Department of Mathematics\\
University of Missouri\\
Columbia, MO 65211\\
USA}
\email{bankswd@missouri.edu}

\keywords{Lean, proof assistants, consistency, incompleteness,
inaccessible cardinals, type theory}
\subjclass[2020]{03B35, 03F40, 03B38, 03E55}

\date{September 13, 2026}

\begin{document}

\begin{abstract}
We give an expository account of a mathematical result that the
Lean proof assistant can formally \emph{state} but, by G\"odel's
second incompleteness theorem, can never \emph{verify}, and which
it also does not refute, namely, \emph{the consistency of Lean's
own underlying type theory}. Working in $\ZFC$ extended by the
existence of infinitely many inaccessible cardinals, we sketch
the construction of a set-theoretic model of Lean's Calculus of
Inductive Constructions (with its universe hierarchy, quotient
types, and choice), outline the proof of a soundness lemma, and
conclude that no derivation of $\False$ exists. The argument is
the model-theoretic consistency proof carried out in full by
Carneiro, building on Werner's set-theoretic interpretation of
the same calculus; all substantive results are due to these
authors, and this paper claims no new mathematics. We explain
why this theorem lies outside Lean's own reach, note that
G\"odel's second incompleteness theorem has itself been verified
by Lean's kernel for first-order arithmetic, and discuss why
every consistency proof ultimately rests on trust rather than
proof.
\end{abstract}

\maketitle

%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% PAPER BEGINS %%%%%
%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction and statement of results}
\label{sec:intro}

\subsection{Background}

Lean~\cite{lean4} is a proof assistant, a computer program whose
small,
fully specified kernel mechanically checks every step of a formal
mathematical proof. Lean's logical rulebook is a dependent type
theory, namely, the
\emph{Calculus of Inductive Constructions} (CIC) with a countable
hierarchy of
non-cumulative universes, definitional proof irrelevance, quotient
types,
and an axiom of definite description/choice
(\texttt{Classical.choice})~\cite{carneiro}.

The trustworthiness of such a system rests on a single property, which
is of course
\emph{consistency}. In Lean's language there is a distinguished
proposition
$\False$, an inductive type that has no constructors; it is the
canonical
contradiction. Because the underlying logic validates \emph{ex falso
quodlibet}, a single derivation of $\False$ would make every
proposition
derivable and render the certification stamp utterly meaningless.
Consistency is
the assertion that this never happens.

\subsection{Results}

This paper presents that assertion as a theorem and proves it. The
proof
is not ours, rather it is the model-theoretic consistency proof
carried out in
detail by Carneiro~\cite{carneiro}, building on the tradition of
set-theoretic models of type theory going back to
Werner~\cite{werner}. Our aim is a self-contained exposition of its
architecture, followed by a careful discussion of its peculiar
epistemic status. The theorem below is a true statement \emph{about}
Lean
that Lean itself can formalize, can never prove, and does not
disprove.
Our main result is the following.

\begin{theorem}[Consistency of Lean; Carneiro~\cite{carneiro}]
\label{thm:main}
Work in $\ZFC^{+}$, which is $\ZFC$ extended by the existence of
infinitely many inaccessible cardinals. Then Lean's type theory does
not
derive $\False$; in other words, $\Con(\Lean)$ holds.
\end{theorem}

The hypothesis is essentially optimal
(Remark~\ref{rem:calibration}), and Theorem~\ref{thm:main} is
proved in Section~\ref{sec:proof} by constructing a set-theoretic
model of Lean's type theory and establishing soundness. The
theorem's significance is framed by two further facts: Lean
itself can never prove $\Con(\Lean)$ (Theorem~\ref{thm:godel},
proved in Section~\ref{sec:framing}), and Lean does not refute it
either (Theorem~\ref{thm:nonref}, proved in
Section~\ref{sec:proof} alongside the main theorem). Together
these show that $\Con(\Lean)$ is independent of Lean.
Section~\ref{sec:discussion} discusses what has and has not been
proved, and what has been machine checked.

\subsection{Conventions}

Precise definitions of the object theory, of the arithmetized sentence
$\Con(\Lean)$, and of the metatheory $\ZFC^{+}$ are given in
Section~\ref{sec:prelim}. Throughout, we use $\sem{\,\cdot\,}$ to
denote the
set-theoretic interpretation constructed in Section~\ref{sec:proof},
$V_{\alpha}$ denotes the cumulative hierarchy, and $\vdash$ denotes
kernel-level derivability in Lean.

\section{Preliminaries}
\label{sec:prelim}

\subsection{The object theory}

By \emph{Lean's type theory} we mean the kernel-level calculus that
is described in~\cite{carneiro}, consisting of dependent function
types ($\Pi$-types), a universe
hierarchy $\mathtt{Sort}\,0 = \LProp$,
$\mathtt{Sort}\,(n{+}1) = \LType\,n$,
universe polymorphism, inductive type families with their recursors,
definitional proof irrelevance in $\LProp$, together with the three
axioms of
propositional extensionality, quotient soundness, and choice. A
\emph{derivation} is a finite object checkable by a terminating
algorithm;
consequently the set of theorems of Lean is recursively enumerable,
and
derivations can therefore be coded by natural numbers in any theory
interpreting
elementary arithmetic; this includes Lean itself, which constructs
$\N$ as an inductive type and proves (far more than) Peano
arithmetic.

We write $\Con(\Lean)$ for the arithmetized statement
\begin{center}
\text{\tt "No natural number
codes a kernel-accepted derivation of $\False$."}
\end{center}

\subsection{The metatheory}

Our metatheory is
\[
\ZFC^{+} \;=\; \ZFC + \text{``there exist infinitely many inaccessible
cardinals.''}
\]
Recall that a cardinal $\kappa$ is said to be
\emph{inaccessible} if it is uncountable,
regular, and a strong limit
($\lambda < \kappa \Rightarrow 2^{\lambda} <
\kappa$). The role of inaccessibility is \emph{closure}. For each
inaccessible
$\kappa$, the cumulative-hierarchy stage $V_{\kappa}$ is closed under
all
the set-forming operations that Lean's typing rules demand, namely,
dependent
products indexed by members of $V_\kappa$, least fixed points of the
monotone operators arising from inductive specifications, quotients,
and
choice functions. Indeed, we have $V_\kappa \models \ZFC$ (since
it is a Grothendieck universe), and this is precisely why nothing
weaker
than a large-cardinal hypothesis will do.
Lean proves $\Con(\ZFC)$ (see~\cite{carneiro}), and therefore by
G\"odel's second
incompleteness theorem, $\ZFC$ alone cannot prove $\Con(\Lean)$.

\begin{remark}[Calibration]\label{rem:calibration}
The large-cardinal hypothesis of Theorem~\ref{thm:main} is
essentially optimal. Carneiro~\cite{carneiro} calibrates the two
theories level by level, with the fragment of Lean having
$n{+}1$ universes proved consistent in $\ZFC$ plus $n{+}1$
inaccessibles, and conversely the fragment of Lean having
$n{+}2$ universes proving the consistency of $\ZFC$ plus $n$
inaccessibles; in particular Lean proves the consistency of
every finite fragment of $\ZFC^{+}$. Thus $\Lean$ and
$\ZFC^{+}$, the latter read as a schema, are equiconsistent.
Both sit strictly below $\ZFC$ + ``there is a Mahlo cardinal''
in consistency strength, a standard fact, since the inaccessible
cardinals below a Mahlo cardinal are unbounded and the
cumulative-hierarchy stage at such a cardinal therefore models
$\ZFC^{+}$.
\end{remark}

\section{Unprovability}
\label{sec:framing}

We first record the fact that frames the significance of
Theorem~\ref{thm:main}.

\begin{theorem}[Unprovability; G\"odel II]\label{thm:godel}
If Lean is consistent, then Lean cannot prove the statement
$\Con(\Lean)$.
\end{theorem}

\begin{proof}[Proof sketch]
Lean is recursively axiomatized with decidable proof checking,
and it interprets elementary arithmetic with enough strength to
verify the derivability conditions of Hilbert, Bernays, and
L\"ob for its own provability predicate. G\"odel's second
incompleteness theorem~\cite{godel} applies verbatim to any
consistent theory of this kind and shows that no such theory
proves its own canonical consistency statement.
\end{proof}

\section{Proof of Theorem~\ref{thm:main}}
\label{sec:proof}

The classical strategy is to construct a set-theoretic model of the
calculus,
prove soundness of the typing rules with respect to the model, and
observe
that $\False$ denotes the empty set.

\subsection{Step 1: The interpretation of universes}

Let $\kappa_0 < \kappa_1 < \kappa_2 < \cdots$ be a fixed increasing
sequence
of inaccessible cardinals. Define
\[
\sem{\mathtt{Sort}\,0} \;=\; \sem{\LProp} \;=\; \{\varnothing,
\{\varnothing\}\},
\qquad
\sem{\mathtt{Sort}\,(n{+}1)} \;=\; \sem{\LType\,n} \;=\; V_{\kappa_n}.
\]
Propositions are interpreted \emph{proof-irrelevantly}, which means
that each proposition is interpreted as one of exactly two sets,
$\varnothing$ when the proposition is false in the model and the
singleton $\{\varnothing\}$ when it is true, the sole element
$\varnothing$ serving as its unique formal witness. This matches
Lean's definitional proof irrelevance, under which any two proofs of
the
same proposition are definitionally equal. Universe polymorphism is
handled
by interpreting a polymorphic constant as a family of interpretations
indexed by assignments of natural numbers to its universe variables.

\subsection{Step 2: The interpretation of terms and types}

By recursion on (well-typed) syntax one assigns a set-theoretic
denotation $\sem{\Gamma}$ to every context $\Gamma$ and, for a given
environment $\rho \in \sem{\Gamma}$, denotations $\sem{T}_{\rho}$
and $\sem{e}_{\rho}$ to every type $T$ and term $e$ in that
context, as follows.

\begin{itemize}
\item \emph{Dependent products.} The interpretation
$\sem{\Pi\,x{:}A.\,B}_{\rho}$ is the
set-theoretic dependent function space
$\prod_{a \in \sem{A}_{\rho}} \sem{B}_{\rho[x \mapsto a]}$, with the
convention that a product landing in $\LProp$ is collapsed to its
proof-irrelevant truth value. Inaccessibility of $\kappa_n$ ensures
that this
set again lies in $V_{\kappa_n}$ whenever its data do.
\item \emph{Inductive types.} An inductive specification determines a
monotone operator on $V_{\kappa_n}$; its least fixed point exists
because
$\kappa_n$ is regular and a strong limit, and interprets the inductive
type. Constructors denote the evident injections and recursors denote
definition by well-founded recursion on the fixed point. In
particular,
\[
\sem{\False} = \varnothing\mand
\sem{\N} = \omega .
\]
\item \emph{Quotients.} For a binary relation $r$ on a type $A$,
the set $\sem{\mathtt{Quot}\,r}$ is the genuine set quotient of
$\sem{A}$ by the equivalence relation generated by $\sem{r}$;
\texttt{Quot.mk} denotes the projection and \texttt{Quot.lift}
the induced map, so the quotient axioms hold.
\item \emph{Choice.} The constant $\mathtt{Classical.choice}$, whose
type is
\[
\Pi\,\alpha{:}\LType\,u.\ \mathtt{Nonempty}\,\alpha \to
\alpha,
\] is interpreted by a choice function on $V_{\kappa_u}$,
which exists by the
axiom of choice in the metatheory. Propositional extensionality holds
because $\sem{\LProp}$ has exactly two elements.
\end{itemize}

\subsection{Step 3: Soundness}

\begin{lemma}[Soundness]\label{lem:soundness}
For every judgment derivable in Lean's kernel, we have
\begin{enumerate}
\item if $\Gamma \vdash T : \mathtt{Sort}\,u$ then
$\sem{T}_{\rho} \in \sem{\mathtt{Sort}\,u}$ for all
$\rho \in \sem{\Gamma}$;
\item if $\Gamma \vdash e : T$ then
$\sem{e}_{\rho} \in \sem{T}_{\rho}$ for all $\rho \in \sem{\Gamma}$;
\item if $\Gamma \vdash e \equiv e' : T$ (definitional equality) then
$\sem{e}_{\rho} = \sem{e'}_{\rho}$ for all $\rho \in \sem{\Gamma}$.
\end{enumerate}
\end{lemma}

\begin{proof}[Proof sketch]
By induction on derivations, checking each typing and conversion rule
against the clauses of Step~2. The computation rules
($\beta$, $\eta$, $\iota$ for recursors, quotient computation) hold as
literal equalities of sets under the interpretation. However, two
points require
genuine care, and these constitute the technical heart
of~\cite{carneiro}.

\emph{Proof irrelevance.} Definitional proof irrelevance makes Lean's
declarative definitional equality ill-behaved as an algorithm (it is
undecidable, and the kernel's algorithmic approximation is not
transitive
on all terms). The soundness proof therefore proceeds for an
idealized,
declarative presentation of the equality judgment, of which the
kernel's
algorithm is shown to accept only instances; semantically, proof
irrelevance is validated because $\sem{\LProp}$-inhabitants are
subsingletons
by construction.

\emph{Universe polymorphism and large elimination.} Soundness is
proved uniformly in universe-level assignments, and the eliminators of
$\LProp$-valued inductive types are checked to respect the collapsed,
proof-irrelevant interpretation (Lean's restriction of large
elimination to
syntactic subsingletons is exactly what makes this clause go through).
\end{proof}

\subsection{Step 4: Conclusion and consequences}

\begin{proof}[Proof of Theorem~\ref{thm:main}]
Suppose on the contrary that Lean derives
$\vdash e : \False$ for some term $e$ in the empty context. By
Lemma~\ref{lem:soundness}(2), $\sem{e} \in \sem{\False}$. By Step~2,
$\sem{\False} = \varnothing$. Thus $\varnothing$ has an element,
contradicting the definition of $\varnothing$ in the metatheory.
Hence no such derivation exists; that is, $\Con(\Lean)$ holds.
\end{proof}

\begin{theorem}[Non-refutability]\label{thm:nonref}
Work in $\ZFC^{+}$. Then Lean does not prove $\lnot\Con(\Lean)$.
\end{theorem}

\begin{proof}
The negation $\lnot\Con(\Lean)$ is a $\Sigma_1$ arithmetic
sentence, for it asserts the existence of a specific finite
object, namely a code of a kernel-accepted derivation of
$\False$. By Step~2 the model interprets $\N$ as the standard
$\omega$, so the arithmetic sentences of Lean are evaluated over
the standard natural numbers, and Lemma~\ref{lem:soundness}(2)
shows that every arithmetic theorem of Lean is true there; in
particular Lean proves no false $\Sigma_1$ sentence. By
Theorem~\ref{thm:main} the sentence $\lnot\Con(\Lean)$ is false,
hence unprovable in Lean.
\end{proof}

\begin{corollary}
Work in $\ZFC^{+}$. Then $\Con(\Lean)$ holds, whereas
\[
\Lean \nvdash \Con(\Lean)\mand\Lean \nvdash \lnot\Con(\Lean).
\]
$\Con(\Lean)$ is thus a sentence in Lean's own language that is
provable in the metatheory but independent of Lean itself.
\end{corollary}

\section{Discussion: what has and has not been proved}
\label{sec:discussion}

\subsection{Why the theorem cannot be internalized}

Theorem~\ref{thm:godel} is not an artifact of Lean's design but a law
governing every sufficiently strong formal system. Any proof checker
capable of formalizing ordinary mathematics is thereby capable of
formalizing its own syntax; G\"odel's diagonal construction then
manufactures the sentence whose unprovability is equivalent to
consistency. The system can \emph{state} its own reliability and can
even
verify the conditional
$\Con(\ZFC^{+}) \to \Con(\Lean)$ (implications of this shape are not
blocked) but it can never discharge the antecedent.
Adjoining new axioms (say, an inaccessible cardinal,
stated type-theoretically) yields a stronger system that proves
$\Con(\Lean)$, but that system is then barred from proving
\emph{its} own consistency. The frontier moves, but it never closes.

\subsection{The regress, stated honestly}

The unconditional content of this paper is the implication
\[
\Con\big(\ZFC + \text{infinitely many inaccessibles}\big)
\;\Longrightarrow\; \Con(\Lean),
\]
together with the standard reasons for confidence in its
hypothesis. Those reasons are the coherence of the intuitive
picture of the cumulative hierarchy of sets, a century of
set-theoretic practice in which no contradiction has ever
appeared, and the calibration of Remark~\ref{rem:calibration},
which shows that the assumption is no stronger than the task
demands. No consistency proof, by anyone, for any theory of this
strength, does better. The consistency of the metatheory itself
can be established only from a still stronger standpoint, and
that standpoint from a stronger one yet, \emph{ad infinitum}.
Gentzen's proof of $\Con(\mathsf{PA})$ from transfinite induction
up to $\varepsilon_0$ (see~\cite{gentzen}) set the pattern, with
consistency purchased in currency that is minted one level up, and
Theorem~\ref{thm:main} is its modern, large-cardinal descendant.
The theorem therefore delivers not absolute certainty
but the strongest substitute mathematics has found, a precise
reduction of the reliability of a proof checker to the soundness
of the classical foundations of set theory.

\subsection{What has been machine checked}

There is a coda that returns the story to Lean itself. G\"odel's
second incompleteness theorem, the engine of
Theorem~\ref{thm:godel}, has been formalized and verified in
Lean. The Foundation development~\cite{foundation} contains
kernel-checked proofs of both incompleteness theorems for
arithmetic theories extending $\mathsf{I}\Sigma_1$, so the very
fact that bounds what Lean can certify about itself carries a
certificate that Lean's kernel accepts. The certificate stops
exactly where Theorem~\ref{thm:godel} says it must. The
formalized statement concerns first-order arithmetic, not Lean's
own type theory; instantiating it at Lean would require
formalizing kernel derivability inside Lean and verifying the
derivability conditions of Hilbert, Bernays, and L\"ob for it, a
program begun in the Lean4Lean project~\cite{lean4lean} but not
yet complete. We propose this as a natural continuation. A future
development could certify Theorem~\ref{thm:godel} for Lean
itself, while Theorem~\ref{thm:main} would remain, provably,
beyond its reach.

\section*{Acknowledgments}

The author thanks Ade Irma Suriajaya and Jesse Thorner for their
comments on the original manuscript. He also thanks the Max
Planck Institute for Mathematics in Bonn for its support and
excellent working conditions during the preparation of this
paper. Part of this work was carried out during the workshop
``Arithmetic, L-functions, and Pseudorandomness'' (26w5546) at
the Banff International Research Station, and the author thanks
BIRS for its hospitality. Travel support from a Faculty
International Travel award of the College of Arts and Science of
the University of Missouri is gratefully acknowledged.

In accordance with the AMS policy statement on generative
artificial intelligence, the author discloses that the large
language model Claude (Anthropic) was used extensively in the
preparation of this paper. The model produced initial drafts of
much of the text, including the exposition of the proofs, and
assisted with literature searches, proof checking, and
brainstorming. The mathematical results are due to the authors
cited in the text. The author directed and revised the entire
manuscript, verified every mathematical claim and every
reference, and takes full and sole responsibility for the final
content.

\section*{Declarations}

\emph{Funding.} The author's work was supported in part by a
PIMS--BIRS grant, by the Max Planck Institute for Mathematics
in Bonn, and by a Faculty International Travel award of the
College of Arts and Science of the University of Missouri.

\emph{Competing interests.} The author has no competing
interests to declare that are relevant to the content of this
article.

\begin{thebibliography}{99}

\bibitem{carneiro}
M.~Carneiro,
The type theory of Lean.
Master's thesis, Carnegie Mellon University, 2019.

\bibitem{lean4lean}
M.~Carneiro,
Lean4Lean: verifying a typechecker for Lean, in Lean.
In: \emph{31st International Conference on Types for Proofs and
Programs (TYPES 2025)}, Leibniz Int. Proc. Inform., vol.~384,
Schloss Dagstuhl, Dagstuhl, 2026, 2:1--2:23.

\bibitem{lean4}
L.~de~Moura and S.~Ullrich,
The Lean 4 theorem prover and programming language.
In: \emph{Automated Deduction -- CADE 28},
Lecture Notes in Comput. Sci., vol.~12699, Springer, Cham, 2021,
625--635.

\bibitem{foundation}
The Formalized Formal Logic project,
Foundation: formalization of mathematical logic in Lean 4.
\url{https://github.com/FormalizedFormalLogic/Foundation}.

\bibitem{gentzen}
G.~Gentzen,
Die Widerspruchsfreiheit der reinen Zahlentheorie.
\emph{Math. Ann.} 112 (1936), 493--565. English translation:
The consistency of elementary number theory, in M.~E.~Szabo (ed.),
\emph{The Collected Papers of Gerhard Gentzen}. Stud. Logic Found.
Math., vol.~55, North-Holland, Amsterdam, 1969, 132--213.

\bibitem{godel}
K.~G\"odel,
\"Uber formal unentscheidbare S\"atze der Principia Mathematica und
verwandter Systeme I.
\emph{Monatsh. Math. Phys.} 38 (1931), 173--198.

\bibitem{werner}
B.~Werner,
Sets in types, types in sets.
In: \emph{Theoretical Aspects of Computer Software (TACS~'97)},
Lecture Notes in Comput. Sci., vol.~1281, Springer, Berlin, 1997.

\end{thebibliography}

\end{document}