The Pythagorean theorem

A builder in Accra wants the corner of a new wall to be exactly square. She has no protractor, only a tape measure. So she marks a point 3 metres along one wall and a point 4 metres along the other, and measures the distance between the marks. If it is exactly 5 metres, the corner is a right angle. If it is more, the corner is too wide; if less, too narrow.

Why should the numbers 3, 4 and 5 know anything about right angles? And why does the same trick work with 5, 12 and 13, or with 6, 8 and 10 — but not with 4, 5 and 6? The answer is one of the oldest and most famous theorems in mathematics. It was known, in some form, to scribes in ancient Mesopotamia, to the authors of the Indian Śulbasūtras, and to Chinese astronomers, long before it became attached to the name of Pythagoras. It is also the reason a computer can measure the distance between two points on a map.

Draw a right triangle with sides 3, 4 and 5 on squared paper, and build a square outward on each side. The square on the side 3 contains $9$ unit squares, the square on the side 4 contains $16$, and the square on the side 5 contains $25$. And $9 + 16 = 25$.

So the theorem is really about areas: the two smaller squares together have exactly the same area as the big one. You can try other right triangles in the explorer further down — for legs 1 and 1, the tilted square has area $2$ — and the areas always balance.

Now try a triangle without a right angle, such as an equilateral triangle with all sides 1. The squares on its sides have areas $1$, $1$ and $1$, and $1 + 1 \neq 1$. The right angle is essential.

We will use two facts from earlier lessons: the angles of a triangle add up to $180^\circ$, and the area of a right triangle with legs $a$ and $b$ is $\tfrac12 ab$ (half of an $a \times b$ rectangle).

The left picture also gives an algebraic proof. Its total area is

and subtracting $2ab$ from both sides leaves $a^2 + b^2 = c^2$.

The builder's 3-4-5 trick uses the theorem backwards: from the side lengths she concludes there is a right angle.

The same comparison tells more. If $a^2 + b^2 > c^2$, the angle opposite $c$ is acute (less than $90^\circ$); if $a^2 + b^2 \lt c^2$, it is obtuse (more than $90^\circ$). The computation section checks this on hundreds of triangles; a proof comes later with the law of cosines in trigonometry.

In the coordinate plane we could measure distances along horizontal and vertical lines. Now we can measure them in any direction.

A Pythagorean triple is a set of three positive whole numbers $(a, b, c)$ with $a^2 + b^2 = c^2$, such as $(3, 4, 5)$, $(5, 12, 13)$ and $(8, 15, 17)$. Multiplying a triple by any whole number $k$ gives another, because $(ka)^2 + (kb)^2 = k^2(a^2 + b^2) = k^2 c^2 = (kc)^2$. So $(6, 8, 10)$, $(9, 12, 15)$, $(12, 16, 20)$, … are triples too, and there are infinitely many triples.

A triple whose three numbers have no common factor, like $(3, 4, 5)$, is primitive. Here is a recipe that produces them, recorded in Euclid's Elements (Book X).

$m = 2, n = 1$ gives $(3, 4, 5)$; $m = 3, n = 2$ gives $(5, 12, 13)$; $m = 4, n = 1$ gives $(15, 8, 17)$. In fact, when $m$ and $n$ have no common factor and are not both odd, the formula gives a primitive triple, and every primitive triple arises this way (with the two legs possibly swapped). That second statement is a theorem of number theory whose proof we postpone to elementary number theory; the computation below checks it for all triples up to 100.

What about cubes? Are there positive whole numbers with $a^3 + b^3 = c^3$, or $a^n + b^n = c^n$ for some $n \ge 3$? Pierre de Fermat claimed around 1637 that there are none. His claim, Fermat's Last Theorem, was proved only in 1995, by Andrew Wiles (with a final step completed together with Richard Taylor), using some of the deepest mathematics of the twentieth century.

First, the algebraic step of each dissection proof. What Lean checks here is the area bookkeeping: if the big square is made of the pieces, then $a^2 + b^2 = c^2$. That the pieces really fit together — the geometric half of the proof — is argued in words above, not formalised.

/-- **The first rearrangement proof, algebraic step.** If a square of side `a + b` is made up
of a tilted square of side `c` and four right triangles with legs `a`, `b` (area `ab/2` each),
then `a² + b² = c²`.
`(a + b)² = a² + 2ab + b²`, and the four triangles account for `4 · ab/2 = 2ab`. -/
theorem rearrangement_algebra (a b c : Rat) (h : (a + b) ^ 2 = c ^ 2 + 4 * (a * b / 2)) :
    a ^ 2 + b ^ 2 = c ^ 2 := by
  have expand : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * (a * b) := by grind
  have four : 4 * (a * b / 2) = 2 * (a * b) := by grind
  calc a ^ 2 + b ^ 2 = (a + b) ^ 2 - 2 * (a * b) := by rw [expand]; grind
    _ = c ^ 2 + 4 * (a * b / 2) - 2 * (a * b) := by rw [h]
    _ = c ^ 2 := by rw [four]; grind

/-- **The second dissection proof, algebraic step** (the “hypotenuse diagram”). If a square of
side `c` is made up of four right triangles with legs `a`, `b` and a small square of side
`b - a` in the middle, then `a² + b² = c²`, because `(b - a)² + 2ab = a² + b²`. -/
theorem rearrangement_square_in_middle (a b c : Rat)
    (h : c ^ 2 = (b - a) ^ 2 + 4 * (a * b / 2)) : a ^ 2 + b ^ 2 = c ^ 2 := by
  rw [h]
  grind

Next, the theorem and its converse in coordinates. To stay with exact fractions we never take square roots: sqDist is the square of the distance. And “the angle at $C$ is a right angle” is expressed without measuring angles: the step from $C$ to $B$ is the step from $C$ to $A$ turned through a quarter turn, $(p, q) \mapsto (-q, p)$, and then stretched by some factor $t$.

/-- A point of the coordinate plane with rational coordinates. -/
structure Point where
  x : Rat
  y : Rat
deriving DecidableEq

/-- The **square** of the distance from `P` to `Q`: `(x₂ - x₁)² + (y₂ - y₁)²`. Comparing
squares of lengths lets us avoid square roots entirely. -/
def sqDist (P Q : Point) : Rat := (Q.x - P.x) ^ 2 + (Q.y - P.y) ^ 2

/-- The distance from `(1, 2)` to `(4, 6)` is `5`: the legs are `3` and `4`, and
`3² + 4² = 25 = 5²`. -/
theorem distance_example : sqDist ⟨1, 2⟩ ⟨4, 6⟩ = 5 ^ 2 := by decide +kernel

/-- The angle `ACB` is a right angle: the step from `C` to `B` is the step from `C` to `A`
turned through a quarter turn (`(p, q) ↦ (-q, p)`) and scaled by some factor `t`. -/
def IsRightAngleAt (A B C : Point) : Prop :=
  ∃ t : Rat, B.x - C.x = -t * (A.y - C.y) ∧ B.y - C.y = t * (A.x - C.x)

/-- **The Pythagorean theorem in coordinates.** If the angle at `C` is a right angle, then
`AB² = CA² + CB²`.
Write `A - C = (p, q)`, so `B - C = (-tq, tp)`. Then `CA² = p² + q²`, `CB² = t²(p² + q²)` and
`AB² = (-tq - p)² + (tp - q)² = (1 + t²)(p² + q²)`: the cross terms `±2tpq` cancel. -/
theorem pythagoras_coordinates (A B C : Point) (h : IsRightAngleAt A B C) :
    sqDist A B = sqDist C A + sqDist C B := by
  obtain ⟨t, h1, h2⟩ := h
  unfold sqDist
  have e1 : B.x - A.x = (B.x - C.x) - (A.x - C.x) := by grind
  have e2 : B.y - A.y = (B.y - C.y) - (A.y - C.y) := by grind
  rw [e1, e2, h1, h2]
  grind

/-- A tilted right triangle: `C = (1, 1)`, `A = (4, 2)`, `B = (0, 4)`. The step `C → A` is
`(3, 1)` and the step `C → B` is `(-1, 3)`, its quarter turn. So `AB² = 10 + 10 = 20`. -/
theorem right_triangle_example :
    IsRightAngleAt ⟨4, 2⟩ ⟨0, 4⟩ ⟨1, 1⟩ ∧ sqDist ⟨4, 2⟩ ⟨0, 4⟩ = 20 := by
  refine ⟨⟨1, by decide +kernel, by decide +kernel⟩, by decide +kernel⟩

For the converse, the key step is that $p r + q s = 0$ forces $(r, s)$ to be a multiple of $(-q, p)$:

/-- If `(r, s)` is perpendicular to a non-zero `(p, q)` in the sense `p·r + q·s = 0`, then
`(r, s)` is a multiple of the quarter turn `(-q, p)`. The factor is
`t = (p·s - q·r) / (p² + q²)`. -/
theorem quarter_turn_of_dot_zero (p q r s : Rat) (hpq : p ≠ 0 ∨ q ≠ 0)
    (h : p * r + q * s = 0) : ∃ t : Rat, r = -t * q ∧ s = t * p := by
  have hne : p * p + q * q ≠ 0 := Rat.ne_of_gt (sum_sq_pos p q hpq)
  have ht : (p * s - q * r) / (p * p + q * q) * (p * p + q * q) = p * s - q * r :=
    Rat.div_mul_cancel hne
  generalize (p * s - q * r) / (p * p + q * q) = t at ht
  refine ⟨t, ?_, ?_⟩
  · have hr : r * (p * p + q * q) = (-t * q) * (p * p + q * q) := by grind
    calc r = r * (p * p + q * q) / (p * p + q * q) := (Rat.mul_div_cancel hne).symm
      _ = (-t * q) * (p * p + q * q) / (p * p + q * q) := by rw [hr]
      _ = -t * q := Rat.mul_div_cancel hne
  · have hs : s * (p * p + q * q) = (t * p) * (p * p + q * q) := by grind
    calc s = s * (p * p + q * q) / (p * p + q * q) := (Rat.mul_div_cancel hne).symm
      _ = (t * p) * (p * p + q * q) / (p * p + q * q) := by rw [hs]
      _ = t * p := Rat.mul_div_cancel hne

/-- **The converse in coordinates.** If `A ≠ C` and `AB² = CA² + CB²`, then the angle at `C`
is a right angle.
Expanding, `AB² = CA² + CB² - 2(p·r + q·s)` where `(p, q) = A - C` and `(r, s) = B - C`; so the
hypothesis says exactly `p·r + q·s = 0`, and `quarter_turn_of_dot_zero` finishes. -/
theorem converse_coordinates (A B C : Point) (hAC : A ≠ C)
    (h : sqDist A B = sqDist C A + sqDist C B) : IsRightAngleAt A B C := by
  have hpq : A.x - C.x ≠ 0 ∨ A.y - C.y ≠ 0 := by
    by_cases hx : A.x - C.x = 0
    · right
      intro hy
      apply hAC
      cases A
      cases C
      simp only at hx hy
      grind
    · left
      exact hx
  have hdot : (A.x - C.x) * (B.x - C.x) + (A.y - C.y) * (B.y - C.y) = 0 := by
    unfold sqDist at h
    grind
  exact quarter_turn_of_dot_zero _ _ _ _ hpq hdot

Finally, whole-number facts: triples, the non-example $5, 6, 8$, scaling, Euclid's formula (for all integers $m, n$), infinitely many triples, and two warnings.

/-- Three Pythagorean triples: `3² + 4² = 5²`, `5² + 12² = 13²`, `8² + 15² = 17²`. -/
theorem triple_examples : 3 ^ 2 + 4 ^ 2 = 5 ^ 2 ∧ 5 ^ 2 + 12 ^ 2 = 13 ^ 2 ∧
    8 ^ 2 + 15 ^ 2 = 17 ^ 2 := by decide

/-- A triangle with sides `5, 6, 8` has **no** right angle: `5² + 6² = 61`, but `8² = 64`.
(By the converse, a right angle would force `61 = 64`; and the right angle could only be
opposite the longest side.) -/
theorem not_right_example : 5 ^ 2 + 6 ^ 2 ≠ 8 ^ 2 := by decide

/-- Scaling a triple gives a triple: if `a² + b² = c²` then `(ka)² + (kb)² = (kc)²`. -/
theorem triple_scale (a b c k : Nat) (h : a ^ 2 + b ^ 2 = c ^ 2) :
    (k * a) ^ 2 + (k * b) ^ 2 = (k * c) ^ 2 := by
  calc (k * a) ^ 2 + (k * b) ^ 2 = k ^ 2 * (a ^ 2 + b ^ 2) := by grind
    _ = k ^ 2 * c ^ 2 := by rw [h]
    _ = (k * c) ^ 2 := by grind

/-- **Euclid's formula.** For all integers `m, n`, the numbers `m² - n²`, `2mn`, `m² + n²`
satisfy `(m² - n²)² + (2mn)² = (m² + n²)²`. With `m = 2, n = 1` this is `3, 4, 5`. -/
theorem euclid_formula (m n : Int) :
    (m ^ 2 - n ^ 2) ^ 2 + (2 * m * n) ^ 2 = (m ^ 2 + n ^ 2) ^ 2 := by
  grind

/-- **There are infinitely many Pythagorean triples**: beyond any number `N` there is a triple
with all sides positive and the first side bigger than `N`. Take `3k, 4k, 5k` with
`k = N + 1`. -/
theorem infinitely_many_triples (N : Nat) :
    ∃ a b c : Nat, N < a ∧ 0 < b ∧ a ^ 2 + b ^ 2 = c ^ 2 := by
  refine ⟨3 * (N + 1), 4 * (N + 1), 5 * (N + 1), by omega, by omega, ?_⟩
  have h := triple_scale 3 4 5 (N + 1) (by decide)
  rw [Nat.mul_comm 3, Nat.mul_comm 4, Nat.mul_comm 5]
  exact h

/-- **`√(a² + b²)` is not `a + b`.** For positive `a, b`, `a² + b² < (a + b)²`: the square of
the sum has the extra `2ab`. So the hypotenuse is always shorter than the two legs together. -/
theorem sum_sq_lt_sq_sum (a b : Nat) (ha : 0 < a) (hb : 0 < b) :
    a ^ 2 + b ^ 2 < (a + b) ^ 2 := by
  have hab : 0 < a * b := Nat.mul_pos ha hb
  have expand : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * (a * b) := by grind
  omega

/-- The diagonal of a unit square has length `√2`, and `√2` is not a whole number: no whole
number `n` has `n² = 2` (`1² = 1` is too small and `2² = 4` already too big). In fact `√2` is not
even a fraction — see the lesson on real numbers. -/
theorem no_whole_sqrt_two : ¬ ∃ n : Nat, n ^ 2 = 2 := by
  intro ⟨n, h⟩
  match n, h with
  | 0, h => exact absurd h (by decide)
  | 1, h => exact absurd h (by decide)
  | k + 2, h =>
    have : 4 ≤ (k + 2) ^ 2 := by
      have := Nat.mul_le_mul (Nat.le_add_left 2 k) (Nat.le_add_left 2 k)
      rw [Nat.pow_two]
      exact this
    omega

All of these are proved here, using core Lean only. Mathlib proves the theorem and its converse for real inner product spaces (any dimension), and classifies all integer triples — the statement we postponed above.

"""Pythagorean triples up to 100: search, count and Euclid's formula.

The experiment finds every triple of whole numbers a < b < c <= 100 with
a^2 + b^2 = c^2 by trying all pairs, picks out the primitive ones (no common
factor), and compares them with the triples produced by Euclid's formula
(m^2 - n^2, 2mn, m^2 + n^2) for m > n > 0 with no common factor and not both
odd. It also checks that every triple is a multiple of a primitive one and
tests a curious pattern: the product abc is always a multiple of 60. All of
this is exact and exhaustive for c <= 100 only.
"""

import math

def triples(limit):
    """All (a, b, c) with a < b < c <= limit and a^2 + b^2 = c^2."""
    found = []
    for c in range(1, limit + 1):
        for b in range(1, c):
            a_sq = c * c - b * b
            a = math.isqrt(a_sq)
            if a < b and a > 0 and a * a == a_sq:
                found.append((a, b, c))
    return sorted(found, key=lambda t: (t[2], t[0]))

def is_primitive(t):
    """No whole number greater than 1 divides all three sides."""
    return math.gcd(math.gcd(t[0], t[1]), t[2]) == 1

def euclid(m, n):
    """Euclid's triple for m > n > 0, with the two legs in increasing order."""
    a, b, c = m * m - n * n, 2 * m * n, m * m + n * n
    return (min(a, b), max(a, b), c)

def euclid_primitives(limit):
    """Triples from Euclid's formula with m > n > 0 coprime, not both odd."""
    out = set()
    m = 2
    while m * m + 1 <= limit:
        for n in range(1, m):
            if math.gcd(m, n) == 1 and (m - n) % 2 == 1:
                t = euclid(m, n)
                if t[2] <= limit:
                    out.add(t)
        m += 1
    return sorted(out, key=lambda t: (t[2], t[0]))

def primitive_root(t):
    """Divide a triple by the common factor of its sides."""
    g = math.gcd(math.gcd(t[0], t[1]), t[2])
    return (t[0] // g, t[1] // g, t[2] // g)

def hypotenuse_counts(found):
    """How many of the triples in ``found`` have each hypotenuse c."""
    counts = {}
    for _, _, c in found:
        counts[c] = counts.get(c, 0) + 1
    return counts

def main():
    all_t = triples(100)
    prim = [t for t in all_t if is_primitive(t)]
    print(f"Triples with c <= 100: {len(all_t)}; primitive: {len(prim)}")
    print("Primitive triples:")
    for i in range(0, len(prim), 4):
        print("  " + "  ".join(f"{t}" for t in prim[i:i + 4]))
    eu = euclid_primitives(100)
    print(f"Euclid's formula (m > n coprime, not both odd): {len(eu)} triples;"
          f" same list: {eu == prim}")
    roots_ok = all(primitive_root(t) in prim for t in all_t)
    print(f"Every triple is k times a primitive triple: {roots_ok}")
    print(f"abc is a multiple of 60 for every triple found: "
          f"{all(a * b * c % 60 == 0 for a, b, c in all_t)}")
    counts = hypotenuse_counts(all_t)
    best = max(counts.values())
    tops = [c for c, k in sorted(counts.items()) if k == best]
    print(f"Hypotenuses in the most triples ({best} each): {tops}")
    print()
    print("Epistemic status: exact, exhaustive search for c <= 100. It is evidence")
    print("for, not proof of, the facts that Euclid's formula gives every primitive")
    print("triple and that 60 always divides abc; both are theorems of number")
    print("theory, proved with divisibility arguments.")

if __name__ == "__main__":
    main()

The search is exhaustive for $c \le 100$: there are exactly 52 triples, 16 of them primitive, and Euclid's formula produces exactly those 16. It also finds a pattern we did not expect: $abc$ is always a multiple of 60. A search can find patterns and refute guesses, but it cannot prove a pattern continues for ever; both patterns are in fact theorems of number theory.

"""Testing the converse: build every whole-number triangle and measure it.

For every triangle with whole-number sides a <= b <= c <= 20, the experiment
builds it in the coordinate plane: C = (0, 0), B = (a, 0), and A = (x, y)
with CA = b and BA = c. Subtracting the two distance equations gives the exact
value x = (a^2 + b^2 - c^2) / (2a), computed with fractions. The angle at C is
then measured numerically (like a protractor) and compared with the test
"compare a^2 + b^2 with c^2". The sign of x is the whole story: x = 0 means a
right angle at C, x > 0 an acute one, x < 0 an obtuse one.
"""

import math
from fractions import Fraction

def triangles(limit):
    """All (a, b, c) with a <= b <= c <= limit satisfying a + b > c."""
    return [(a, b, c) for c in range(1, limit + 1) for b in range(1, c + 1)
            for a in range(1, b + 1) if a + b > c]

def apex(a, b, c):
    """Exact x and approximate y of A, where C = (0, 0) and B = (a, 0)."""
    x = Fraction(a * a + b * b - c * c, 2 * a)
    y = math.sqrt(b * b - x * x)
    return x, y

def angle_at_c(a, b, c):
    """The angle ACB in degrees, measured from the coordinates."""
    x, y = apex(a, b, c)
    return math.degrees(math.atan2(y, float(x)))

def pythagoras_test(a, b, c):
    """'right', 'acute' or 'obtuse' by comparing a^2 + b^2 with c^2."""
    s, t = a * a + b * b, c * c
    return "right" if s == t else ("acute" if s > t else "obtuse")

def measured_type(a, b, c, tol=1e-9):
    """'right', 'acute' or 'obtuse' from the measured angle at C."""
    ang = angle_at_c(a, b, c)
    if abs(ang - 90) < tol:
        return "right"
    return "acute" if ang < 90 else "obtuse"

def main():
    tris = triangles(20)
    counts = {"right": 0, "acute": 0, "obtuse": 0}
    agree = 0
    for t in tris:
        kind = pythagoras_test(*t)
        counts[kind] += 1
        agree += kind == measured_type(*t)
    print(f"Triangles with whole-number sides a <= b <= c <= 20: {len(tris)}")
    print(f"  by the test a^2 + b^2 vs c^2: {counts['right']} right, "
          f"{counts['acute']} acute, {counts['obtuse']} obtuse")
    print(f"  measured angle at C agrees with the test: {agree} of {len(tris)}")
    rights = [t for t in tris if pythagoras_test(*t) == "right"]
    print("  the right ones:")
    print("    " + ", ".join(str(t) for t in rights))
    print()
    print("Three examples (x is exact, the angle is measured):")
    for t in [(3, 4, 5), (5, 6, 8), (4, 5, 6)]:
        x, _ = apex(*t)
        print(f"  sides {t}: x = {str(x):>6}, angle at C = "
              f"{angle_at_c(*t):7.3f} degrees ({pythagoras_test(*t)})")
    smallest = min((abs(angle_at_c(*t) - 90), t) for t in tris
                   if pythagoras_test(*t) != "right")
    print(f"Closest to 90 degrees without being right: {smallest[1]}, off by "
          f"{smallest[0]:.3f} degrees")
    print()
    print("Epistemic status: exhaustive over these 825 triangles. The x-coordinate")
    print("is exact (x = 0 exactly for the right triangles); the angles are")
    print("floating-point measurements, and an angle within 1e-9 degrees of 90")
    print("counts as right. Evidence for these triangles only: the converse is")
    print("proved in the lesson for every triangle.")

if __name__ == "__main__":
    main()

All 825 triangles agree with the test: right exactly when $a^2 + b^2 = c^2$, acute when it is bigger, obtuse when it is smaller. Look at the exact $x$-coordinate $x = \frac{a^2 + b^2 - c^2}{2a}$ of the top vertex: its sign is the sign of $a^2 + b^2 - c^2$. That observation, turned into an argument, is a second proof of the converse.

Change the legs $a$ and $b$ of the right triangle with corner $C$ at the origin. The picture shows the squares on the two legs, the square on the hypotenuse, and the big square of side $a + b$ from the first proof. Choose whole numbers and count unit squares: for $a = 3$, $b = 4$, the big square has area $49$, the four corner triangles $4 \times 6 = 24$, and the tilted square $49 - 24 = 25 = 9 + 16$. Try $a = b = 1$ to see $\sqrt{2}$.

Optional, and never graded: a question that leads somewhere further.

• Mesopotamia. The Old Babylonian tablet YBC 7289 (about 1800–1600 BCE) shows a square with its diagonals and gives $\sqrt{2}$ in base 60 as $1;24,51,10 \approx 1.4142130$, correct to about six decimal places. The tablet Plimpton 322, from the same period, lists numbers closely related to Pythagorean triples such as $(119, 120, 169)$; its exact purpose is still debated.
• India. The Baudhāyana Śulbasūtra (dates uncertain, perhaps 800–500 BCE), a manual for building fire altars, states that the diagonal of a rectangle produces both areas that its length and breadth produce separately — the theorem in words — and lists triples.
• China. The Zhoubi Suanjing (compiled by about the 1st century CE) discusses the gougu rule with the 3-4-5 triangle. In the 3rd century CE, Zhao Shuang's commentary gave the “hypotenuse diagram” used in our second proof, and Liu Hui gave a dissection proof in his commentary on the Nine Chapters.
• Greece. Euclid's Elements (about 300 BCE) proves the theorem as Book I, Proposition 47, and its converse as Proposition 48. The traditional link with Pythagoras comes from much later writers.
• The Islamic world and beyond. Thābit ibn Qurra in 9th-century Baghdad generalised the theorem to all triangles. In 12th-century India, Bhāskara II gave a dissection proof with the square-in-the-middle figure. In 1876 James Garfield, later President of the United States, published a proof using a trapezium. Elisha Loomis's The Pythagorean Proposition (1927; 2nd edition 1940) collected 367 proofs.
• 1995. Andrew Wiles's proof of Fermat's Last Theorem settled the question Fermat asked about higher powers.

• Eli Maor, The Pythagorean Theorem: A 4,000-Year History (2007).
• Euclid, Elements, Book I, Propositions 47–48 (translation by Thomas L. Heath, 1908).
• Frank J. Swetz and T. I. Kao, Was Pythagoras Chinese? An Examination of Right Triangle Theory in Ancient China (1977).
• Elisha Scott Loomis, The Pythagorean Proposition (1927; 2nd edition 1940).