Formal statements in a proof assistant: reading a Lean statement layer by layer and separating 'is a statement' from 'is proved'

Goal and scope

Take the source string s: `∀ (a b : Nat), a ≤ b → a < b + 1` as a teaching object and, in an environment E that is fixed explicitly but never executed, explain layer by layer: its bound variables and their types, its hypothesis and conclusion, the core term S that elaboration would have to produce if it succeeded, why S would have type Prop, and what a proof term would have to establish; then give an informal proof of its mathematical content and contrast it with s′: `∀ (a : Nat), a - 1 < a` (a Prop, but false) and s″: `∀ (a : Int), a - 1 < a` (true). Lean is not run at any point, and nothing here claims that any text parses, elaborates, compiles or is proved by Lean.

Works inside the MKO's scope: statement identity includes the Lean version, imports, name environment and local context (assumption a1); Lean is paused by the owner's instruction, so this guide gives only conceptual explanation and hand type analysis and produces no elaboration or kernel receipt (assumption a2). The cited Lean notation and typing rules carry citation_verified; the canonical MKO and its English edition are not changed.

Givens and symbols

• order_basics
• numeric_evaluation
• def_unfold

• G1 — Environment E=(V,I,N,Γ): V is a specified Lean 4 version (to be recorded in a receipt when Lean work resumes; not pinned here); I is no imports beyond the Lean 4 core prelude; N is the names declared by that prelude; Γ is the empty local context. All four are part of statement identity (MKO assumption a1).
• G2 — Lean is not run in this guide (owner instruction; MKO assumption a2): no parsing, elaboration, type checking or kernel check was executed. Every sentence below about these stages is either a definition of what the stage must establish or a hand analysis conditional on that stage succeeding.
• G3 — The source string s = `∀ (a b : Nat), a ≤ b → a < b + 1`. Declaring a theorem would further require 'theorem t : s := p' with a proof p; this guide discusses only the statement after the colon.
• G4 — Contrast strings s′ = `∀ (a : Nat), a - 1 < a` and s″ = `∀ (a : Int), a - 1 < a`, read in the same E.

• E=(V,I,N,\Gamma) — the environment: Lean version, imports, name environment, local context
• s — the source string (text not yet parsed)
• S — the core term elaboration would produce if it succeeded
• \Gamma\vdash S:\mathrm{Prop} — in Γ, S has type Prop
• p — a candidate proof term of S
• \mathsf{Elab},\ \mathsf{Kernel} — the elaboration and kernel-check stages
• \mathrm{Nat},\ \mathrm{Int} — Lean's natural-number and integer types

Rules and sources

• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• imp_intro · prerequisite — →-introduction (discharging a hypothesis): if Q is derived inside a scope that temporarily assumes P, then P⇒Q follows, and P may no longer be used as known.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_lean_formal_statement_def · cited — In a fixed Lean version, with fixed imports, name environment and local context Γ, source syntax s expresses a formal statement if it elaborates successfully to a core term S with Γ⊢S:Prop. A statement and the existence of its checked proof term are separate states. · mko-lean-formal-statement
• mko_proposition_def · cited — A proposition P may be true or false; being a proposition does not mean that P has been proved true. · mko-proposition
• lean_stages · cited — Lean 4 processes source in stages: parsing turns text into syntax; elaboration turns syntax into a core term, resolving names, notation, implicit arguments and type-class instances, and may fail; type checking infers the core term's type; for a theorem declaration the kernel checks that the supplied proof term has the stated type. Success at one stage does not guarantee success at a later one. · Lean Language Reference, Elaboration and Compilation, Sections 2.1-2.3
• lean_core_notation · cited — In Lean 4 core, a ≤ b is notation for LE.le a b, a < b for LT.lt a b, a + b for HAdd.hAdd a b, a - b for HSub.hSub a b, and the numeral 1 for OfNat.ofNat 1; LE.le and LT.lt have type α → α → Prop. + binds more tightly than ≤ and <, which bind more tightly than →; → associates to the right; a ∀ extends as far right as possible; (a b : Nat) declares two bound variables of type Nat. The core prelude provides instances of these classes for Nat and Int. · Lean 4 v4.30.0 Init/Notation.lean; Lean Language Reference Basic Classes; Init.Prelude API
• prop_formation · cited — Rules of Lean's type theory: (i) if Γ⊢A:Prop and Γ⊢B:Prop then Γ⊢(A→B):Prop; (ii) if Γ⊢α:Sort u and Γ,x:α⊢B:Prop then Γ⊢(∀x:α, B):Prop (impredicativity of Prop); Nat : Type and Int : Type, where Type = Sort 1. · Theorem Proving in Lean 4, Chapters 3 and 4, Sections 3.1 and 4.1
• curry_howard · cited — Propositions as types: a proof of ∀x:α, B is a function sending each x:α to a proof of B; a proof of A→B is a function sending each proof of A to a proof of B; p : S means p is a term of type S. · Theorem Proving in Lean 4, Sections 3.1 and 4.1
• nat_trunc_sub · cited — In Lean 4 core, subtraction on Nat is truncated: a−b=0 when a≤b, and the usual difference otherwise; in particular 0−1=0. Subtraction on Int is the usual ring subtraction. · Lean 4 Init.Prelude API, Nat.sub; Lean Language Reference, Integers, Int.sub
• L_main · lemma — For all natural numbers a and b: if a≤b then a<b+1.

Main derivation

s,\ E

E=(V,I,N,\Gamma),\quad \Gamma=\varnothing

s

\mathsf{Parse}(s)\ ;\ \mathsf{Elab}(s)=S\ ;\ \Gamma\vdash S:\mathrm{Prop}\ ;\ \Gamma\vdash p:S\ ;\ \mathsf{Kernel}(p,S)

s=\texttt{∀ (a b : Nat), a ≤ b → a < b + 1}

\forall a:\mathrm{Nat},\ \forall b:\mathrm{Nat},\ \bigl((a\le b)\to(a<(b+1))\bigr)

\forall a\,b:\mathrm{Nat},\ a\le b\to a<b+1

S=\forall a\,b:\mathrm{Nat},\ \mathrm{LE.le}\,a\,b\to\mathrm{LT.lt}\,a\,(\mathrm{HAdd.hAdd}\,b\,(\mathrm{OfNat.ofNat}\,1))

S

\Gamma\vdash S:\mathrm{Prop}\quad(\text{conditional on}\ \mathsf{Elab}(s)=S)

\mathsf{Elab}(s)=S\ \wedge\ \Gamma\vdash S:\mathrm{Prop}

s\ \text{expresses a formal statement in}\ E

\Gamma\vdash p:S

p=\lambda (a\,b:\mathrm{Nat})\,(h:a\le b).\ q,\quad a,b:\mathrm{Nat},\ h:a\le b\ \vdash\ q:a<b+1

\forall a\,b,\ a\le b\to a<b+1

(a,b)=(3,3):\ 3\le 3\to 3<4;\quad (a,b)=(5,2):\ 5\le 2\to 5<3

\forall a,b\in\mathbb{N},\ a\le b\Rightarrow a<b+1

\text{true in}\ \mathbb{N}\ \text{(informal proof)}

\text{informal proof of the content of}\ S

\mathsf{Parse},\ \mathsf{Elab},\ \mathsf{Kernel}:\ \text{not run};\ p:\ \text{not constructed}

s'=\texttt{∀ (a : Nat), a - 1 < a}

\Gamma\vdash S':\mathrm{Prop}\quad(\text{conditional on}\ \mathsf{Elab}(s'))

\forall a:\mathrm{Nat},\ a-1<a

a=0:\ 0-1=0,\ \neg(0<0)\ \Rightarrow\ \neg\forall a,\ a-1<a

s''=\texttt{∀ (a : Int), a - 1 < a}

\forall a\in\mathbb{Z},\ a-1<a\ \text{(true)};\quad S''\ne S'

t_0=\texttt{a ≤ b → a < b + 1}

\text{meaning of}\ t_0\ \text{depends on}\ \Gamma\ \text{and elaborator options}

Substeps and lemmas

\Gamma_1=(a:\mathrm{Nat},\ b:\mathrm{Nat})

\Gamma_1\vdash b+1:\mathrm{Nat},\ \Gamma_1\vdash a\le b:\mathrm{Prop},\ \Gamma_1\vdash a<b+1:\mathrm{Prop}

\Gamma_1\vdash a\le b:\mathrm{Prop},\ \Gamma_1\vdash a<b+1:\mathrm{Prop}

\Gamma_1\vdash (a\le b\to a<b+1):\mathrm{Prop}

\Gamma_1\vdash (a\le b\to a<b+1):\mathrm{Prop}

\Gamma\vdash \forall a:\mathrm{Nat},\ \forall b:\mathrm{Nat},\ (a\le b\to a<b+1):\mathrm{Prop}

0<1

b<b+1

a\le b,\ b<b+1

a<b+1

0-1\ \text{in Nat}

0-1=0

0-1<0

0<0,\ \text{which is false}

Reverse audits

• S14 · premise_audit · S01, mko_lean_formal_statement_def, lean_stages — This step states only the dependence and claims no actual elaboration result for t0 in any environment.
• S13 · premise_audit · G4, nat_trunc_sub, order_basics — It needs the usual definition of subtraction on Int (cited) and that order is preserved by addition. N6 checks a finite range only and does not replace the universal proof.
• S12.2 · inverse_equivalence · S12.1, eq_replace — Replacing an expression by an equal one does not change truth, so both directions hold.
• S12.1 · premise_audit · nat_trunc_sub — The conclusion depends on the definition of subtraction on Nat; in Int the same expression equals −1 (see S13).
• S12 · premise_audit · nat_trunc_sub, quantifier_negation, mko_proposition_def — It needs the cited definition of truncated subtraction (citation_verified). One counterexample suffices to refute a universal statement (recomputable as N4, N5).
• S11 · premise_audit · G4, prop_formation, lean_core_notation — As in S05 this is a hand analysis conditional on elaboration succeeding; the conclusion goes only as far as 'is a Prop'.
• S10 · premise_audit · S06, S07, S09, mko_lean_formal_statement_def, G2 — The role of this step is to block promotion: mathematical truth and an informal proof do not imply that Γ⊢p:S has been accepted by the kernel.
• S09.2 · premise_audit · S09.1, order_basics, case_analysis, imp_intro, forall_intro — The two cases cover every way a≤b can hold; no converse is claimed (a<b+1 ⇒ a≤b does hold in ℕ, but it is neither used nor proved here).
• S09.1 · premise_audit · order_basics — Only u<v ⇒ u+w<v+w is used.
• S09 · premise_audit · L_main — The conclusion is a mathematical fact about standard ℕ, not about any Lean state; it produces no proof term and passes through no kernel check. N3 is a finite check on the 49 pairs from 0 to 6 only and does not replace the proof of the lemma.
• S08 · premise_audit · S03, forall_elim — Instantiation only applies the universal statement to particular values; two instances cannot prove the universal statement (N1, N2 check only these numbers).
• S07 · premise_audit · S04, curry_howard — This step only describes the shape a proof term must have; no p is constructed and nothing is kernel-checked.
• S06 · premise_audit · S05, mko_lean_formal_statement_def, G2 — This step does not claim the antecedent holds, so the consequent cannot be treated as confirmed. Nor does it claim S is true or proved: being a statement and being proved are separate states.
• S05.3 · premise_audit · S05.2, prop_formation — It needs Nat to be a type (Sort 1) and rule (ii). The conclusion is that S lies in Prop, which says nothing about whether S is provable.
• S05.2 · premise_audit · S05.1, prop_formation — Only both sides being Props is needed; the implication is not claimed to be true.
• S05.1 · premise_audit · lean_core_notation — It needs the cited type signatures of LE, LT and HAdd. It says only that a≤b is a proposition, not that it is true.
• S05 · premise_audit · S04, prop_formation — It needs the conditional premise of S04 and the cited typing rules; if elaboration produced a different term, this analysis would have to be redone.
• S04 · premise_audit · S03, lean_core_notation, G2 — This step is conditional on Elab(s) succeeding. If E lacked any of the instances or notations, elaboration would fail and S would not exist at all.
• S03 · premise_audit · G3, lean_core_notation — The reading depends on the notation and precedence in E; different imports could redefine notation and give a different structure (MKO paragraph 2). It is not claimed that the parser accepts s.
• S02 · premise_audit · lean_stages, mko_lean_formal_statement_def — The division into stages comes from the cited Lean documentation (citation_verified). This step only defines names for the states and claims none of them has been reached.
• S01 · premise_audit · G1, G2, mko_lean_formal_statement_def — This step only names and derives no new fact. V is not pinned yet; that is an open item and does not affect the conditional analysis below, which treats E as a parameter.

Error controls and negative controls

Four states are not one thing

The misconception identified in the MKO is treating successful parsing, successful elaboration, having type Prop and a kernel-checked proof as one thing. S02 separates them into five states; s′ shows that even if the early states are reached (should elaboration succeed), the statement can be false and so have no proof. This guide contains hand analysis only; no state was executed.

The same text is not the same statement

s′ and s″ differ only in Nat versus Int, yet they are different core terms, one false and one true (S12, S13); t0 means different things in different local contexts (S14). Comparing statements requires comparing environments and core terms, not strings.

An informal proof is not a checked proof term

The argument in S09 proves the mathematical content and gives a construction plan for the proof term (S07), but it is not a Lean term and has not passed the kernel. Reporting it as 'proved by Lean' would be a false promotion.

• s looks like valid Lean, so it elaborates in every environment → reject — Elaboration depends on version, imports, notation, instances and local context (MKO assumption a1); and elaboration was not run in this guide.
• S has type Prop, so S is proved → reject — S′ is also a Prop, yet it is false at a=0: 0−1=0 and 0<0 fails.
• This guide shows that s compiles and that the theorem is proved by Lean → reject — G2: Lean was not run, and there is no parse, elaboration or kernel receipt.
• s′ and s″ differ only in a type name, so they are the same statement → reject — The types and the subtraction differ; s′ is false at a=0 while s″ is true for every integer.

Result and limitations

s reads 'for all natural numbers a and b, if a≤b then a<b+1': two Nat bound variables, one hypothesis a≤b and one conclusion a<b+1. If elaboration succeeds in E, the typing rules give the core term S type Prop, so s expresses a formal statement; a proof term must be a function taking a, b and h:a≤b to a proof of a<b+1. Its mathematical content is true in standard ℕ (informal proof). Lean was not run: parsing, elaboration, proof term and kernel check are all 'not executed'. s′ is a Prop but false at a=0 and s″ is true, showing that types and environment belong to statement identity.

• When the owner resumes Lean work, pin the toolchain version and import closure and record parse and elaboration receipts for s, s′ and s″; proving s would require constructing a proof term and obtaining a kernel receipt (MKO formal next).
• The core term shown in S04 omits implicit and instance arguments; its exact form, including instance names, requires actual elaboration. The cited notation, typing rules and truncated subtraction have been checked against official Lean documentation and the listed core sources. Lean was not run and no elaboration or kernel receipt was obtained.

Verification and source binding

6 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 5cb0d5f28f6aea7530d0c886c4ff344564b3ecefcd4d14d3748e25c6afef4cd2
• original source SHA-256: 5cb0d5f28f6aea7530d0c886c4ff344564b3ecefcd4d14d3748e25c6afef4cd2
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)