Written by Leslie Lamport
on 

Exemplary Structured Proof by Leslie Lamport

The following contains the structured proof as presented by Leslie Lamport’s How to Write a Proof. This example is meant to illustrate how structured proofs are converted from LaTeX to a more interactive format.

You can traverse the proof by using either the mouse, arrow keys, or vi navigation keys.

A proof of the irrationality of √2

A proof of the irrationality of 2

Leslie Lamport
(December 1, 1993)

Theorem  There does not exist r in Q such that r2=2.

Proof sketch: We assume r2=2 for r∈𝐐 and obtain a contradiction. Writing r=m/n, where m and n have no common divisors (step ⟨1⟩⁢1), we deduce from (m/n)2=2 and the lemma that both m and n must be divisible by 2 (⟨1⟩⁢2 and ⟨1⟩⁢3). Assume:

  1. 1.

    r∈𝐐

  2. 2.

    r2=2


Prove:  False


⟨1⟩⁢1. Choose m, n in Z such that (1) gcd⁡(m,n)=1, and (2) r=(m/n)
⟨2⟩⁢1. Choose p, q in Z such that q≠0 and r=p/q.

Proof: By assumption ⟨0⟩:1.


⟨2⟩⁢2. Let m =Δ p/gcd⁡(p,q)
n =Δ q/gcd⁡(p,q)

⟨2⟩⁢3. m,n∈𝐙

Proof: ⟨2⟩⁢1 and definition of m and n.


⟨2⟩⁢4. r=m/n
Proof: m/n = p/gcd⁡(p,q)q/gcd⁡(p,q) [Definition of m and n]
= p/q [Simple algebra]
= r [By ⟨2⟩⁢1]

⟨2⟩⁢5. gcd⁡(m,n)=1

Proof: By the definition of the gcd, it suffices to: Assume:

  1. 1.

    s divides m

  2. 2.

    s divides n


Prove:  s=±1


⟨3⟩⁢1. s⋅gcd⁡(p,q) divides p.

Proof: ⟨2⟩:1 and the definition of m.


⟨3⟩⁢2. s⋅gcd⁡(p,q) divides q.

Proof: ⟨2⟩:2 and definition of n.


Q.E.D.

Proof: ⟨3⟩⁢1, ⟨3⟩⁢2, and the definition of gcd.


Q.E.D.

⟨1⟩⁢2. 2 divides m.
⟨2⟩⁢1. m2=2⁢n2

Proof: ⟨1⟩⁢1.1 implies (m/n)2=2.


Q.E.D.

Proof: By ⟨2⟩⁢1 and the lemma.


⟨1⟩⁢3. 2 divides n.
⟨2⟩⁢1. Choose p in Z such that m=2⁢p.

Proof: By ⟨1⟩⁢2.


⟨2⟩⁢2. n2=2⁢p2
Proof: 2 = (m/n)2 [⟨1⟩⁢1.2 and ⟨0⟩:2]
= (2⁢p/n)2 [⟨2⟩⁢1]
= 4⁢p2/n2 [Algebra]
from which the result follows easily by algebra.

Q.E.D.

Proof: By ⟨2⟩⁢2 and the lemma.


Q.E.D.

Proof: ⟨1⟩⁢1.1, ⟨1⟩⁢2, ⟨1⟩⁢3, and definition of gcd.