PropositionsAndProofs.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 26 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned Theorem Proving in Lean documentation, Pinned Theorem Proving in Lean 4 book index

87 declarations, 26 contain sorry, 5 declared as axioms

Imports (2)

VersoManual
TPiL.Examples

def Implies line 39 source
structure Proof line 61 source
def Implies line 64 source
def Implies line 75 source
structure Proof line 76 source
axiom and_commut An axiom: and is commutative, in a toy proof system line 81 source
L4DEL explanation
The book first models proofs as data (Proof p), and an axiom is just a constant of such a type.
1. Implies p q is defined as p → q, and Proof p is a structure with one field, proof : p, wrapping a proof of p.
2. axiom and_commut (p q : Prop) : Proof (Implies (And p q) (And q p)) postulates a proof of the commutativity of And with no argument for it.
3. With p q : Prop in scope, #check and_commut p q reports Proof (Implies (p ∧ q) (q ∧ p)).
4. This is a sketch of how a proof system could be represented; the book then moves to the real Lean treatment of propositions as types.
See also: modus_ponens
Sources and attribution: Pinned Lean source (4e28129fdd58)
axiom: a declaration whose type is asserted without any proof term; Lean takes it on trust.
```
axiom and_commut (p q : Prop) : Proof (Implies (And p q) (And q p))

variable (p q : Prop)

#check and_commut p q     -- message: and_commut p q : Proof (Implies (p ∧ q) (q ∧ p))
```



In addition to axioms, however, we would also need rules to build new
proofs from old ones. For example, in many proof systems for
propositional logic, we have the rule of _modus ponens_:
…
```
Mentions: Proof, Implies, from, in
def Implies line 99 source
structure Proof line 100 source
axiom modus_ponens Modus ponens as an inference rule on Proof line 103 source
Source comment
----
L4DEL explanation
From a proof of p implies q and a proof of p, the rule produces a proof of q.
1. The block first repeats Implies and Proof from the previous example.
2. axiom modus_ponens (p q : Prop) : Proof (Implies p q) → Proof p → Proof q is stated as a function-typed axiom.
3. It is an axiom, so there is no proof term here; the rule is simply assumed.
See also: and_commut
Sources and attribution: Pinned Lean source (4e28129fdd58)
modus ponens: the inference rule that from p implies q and p concludes q.
```
axiom modus_ponens (p q : Prop) :
  Proof (Implies p q) → Proof p →
  Proof q
```

Systems of natural deduction for propositional logic also typically rely on the following rule:

> Suppose that, assuming {lean}`p` as a hypothesis, we have a proof of {lean}`q`. Then we can “cancel” the hypothesis and obtain a proof of {lean}`Implies p q`.

We could render this as follows:

```lean
```
Mentions: Proof, Implies, as
def Implies line 115 source
structure Proof line 116 source

axiom implies_intro line 119 source

Source comment

----

axiom implies_intro (p q : Prop) :
  (Proof p → Proof q) → Proof (Implies p q)
```

This approach would provide us with a reasonable way of building assertions and proofs.
Determining that an expression {lean}`t` is a correct proof of assertion {lean}`p` would then
simply be a matter of checking that {lean}`t` has type {lean}`Proof p`.

Some simplifications are possible, however. To start with, we can
avoid writing the term {lean}`Proof` repeatedly by conflating {lean}`Proof p`
with {lean}`p` itself. In other words, whenever we have {lean}`p : Prop`, we
can interpret {lean}`p` as a type, namely, the type of its proofs. We can
…

Mentions: Proof, Implies, t, is, type, as

theorem t1 line 224 source
Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:158 (different declaration text). Qualify references as t1@path.
theorem is line 248 source
theorem t1 line 269 source
Source comment
----

Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:158 (different declaration text). Qualify references as t1@path.
```
theorem t1 : p → q → p := fun hp : p => fun hq : q => hp
…
```
Mentions: hp
theorem t1 line 284 source
Source comment
----

Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:158 (different declaration text). Qualify references as t1@path.
```
theorem t1 : p → q → p :=
…
```
theorem t1 line 303 source
Source comment
----

Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:158 (different declaration text). Qualify references as t1@path.
```
theorem t1 (hp : p) (hq : q) : p := hp
…
```
Mentions: hp
theorem t1 line 315 source
Source comment
----

Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:158 (different declaration text). Qualify references as t1@path.
```
theorem t1 (hp : p) (hq : q) : p := hp
```
Mentions: hp
axiom hp line 317 source
theorem t2 line 319 source
Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:165 (different declaration text). Qualify references as t2@path.
example (example at line 324) line 324 source
axiom unsound line 328 source
Distinct definitions of this name: book/TPiL/InductionAndRecursion.lean:1138 (different declaration text). Qualify references as unsound@path.
theorem ex Everything follows from false line 330 source
Source comment
Everything follows from false
```
theorem ex : 1 = 0 :=
…
```
theorem t1 line 350 source
Source comment
----

Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:158 (different declaration text). Qualify references as t1@path.
```
theorem t1 {p q : Prop} (hp : p) (hq : q) : p := hp
…
```
Mentions: hp
theorem t1 line 363 source
Source comment
----

Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:158 (different declaration text). Qualify references as t1@path.
```
theorem t1 : ∀ {p q : Prop}, p → q → p :=
…
```
theorem t1 line 373 source
Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:158 (different declaration text). Qualify references as t1@path.
theorem t1 line 383 source
Source comment
----

Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:158 (different declaration text). Qualify references as t1@path.
```
theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp
…
```
Mentions: hp
theorem t2 line 406 source
Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:165 (different declaration text). Qualify references as t2@path.
example (example at line 494) line 494 source
example (example at line 531) line 531 source
example (example at line 555) line 555 source
example (example at line 556) line 556 source
example (example at line 564) line 564 source
inductive type line 592 source
inductive Foo line 608 source
Distinct definitions of this name: book/TPiL/InductiveTypes.lean:40 (same statement text; different proof or body). Qualify references as Foo@path.
inductive Bar line 609 source
def Foo.bar line 611 source
Distinct definitions of this name: book/TPiL/InteractingWithLean.lean:193 (different declaration text). Qualify references as Foo.bar@path.
example (example at line 647) line 647 source
example (example at line 664) line 664 source
example (example at line 667) line 667 source
example (example at line 692) line 692 source
example (example at line 693) line 693 source
example (example at line 713) line 713 source
example (example at line 730) line 730 source
example (example at line 752) line 752 source
example (example at line 781) line 781 source
example (example at line 794) line 794 source
example (example at line 805) line 805 source
example (example at line 813) line 813 source
theorem and_swap line 842 source
example (example at line 852) line 852 source
theorem and_swap line 863 source
example (example at line 866) line 866 source
structure long line 875 source
example (example at line 882) line 882 source
example (example at line 910) line 910 source
theorem dne line 959 source
theorem dne line 969 source
example (example at line 995) line 995 source
example (example at line 1007) line 1007 source
example (example at line 1023) sorry line 1023 source
Source comment
----
```
example (h : ¬(p ∧ q)) : ¬p ∨ ¬q :=
…
```

example (example at line 1127) line 1127 source

Source comment

distributivity

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
…

example (example at line 1148) sorry line 1148 source
Source comment
an example that requires classical reasoning
```
example (p q : Prop) : ¬(p ∧ ¬q) → (p → q) :=
…
```
example (example at line 1168) sorry line 1168 source
Source comment
commutativity of ∧ and ∨
```
example : p ∧ q ↔ q ∧ p := sorry
```
example (example at line 1169) sorry line 1169 source
example (example at line 1172) sorry line 1172 source
Source comment
associativity of ∧ and ∨
```
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry
```
example (example at line 1173) sorry line 1173 source
example (example at line 1176) sorry line 1176 source
Source comment
distributivity
```
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := sorry
```
example (example at line 1177) sorry line 1177 source
example (example at line 1180) sorry line 1180 source
Source comment
other properties
```
example : (p → (q → r)) ↔ (p ∧ q → r) := sorry
```
example (example at line 1181) sorry line 1181 source
example (example at line 1182) sorry line 1182 source
example (example at line 1183) sorry line 1183 source
example (example at line 1184) sorry line 1184 source
example (example at line 1185) sorry line 1185 source
example (example at line 1186) sorry line 1186 source
example (example at line 1187) sorry line 1187 source
example (example at line 1188) sorry line 1188 source
example (example at line 1189) sorry line 1189 source
example (example at line 1190) sorry line 1190 source
example (example at line 1201) sorry line 1201 source
example (example at line 1202) sorry line 1202 source
example (example at line 1203) sorry line 1203 source
example (example at line 1204) sorry line 1204 source
example (example at line 1205) sorry line 1205 source
example (example at line 1206) sorry line 1206 source
example (example at line 1207) sorry line 1207 source