Classic mathematics

Pythagoras: the square identity

Relate a square-area identity to a² + b² = c², then check an exact right-triangle example.

-- Top 100 #4: Pythagoras: the square identity
-- History: c. 500 BCE · Pythagorean tradition.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: The familiar 3–4–5 triangle is one exact integer example.
-- Scope: Proves the square-area identity used in a rearrangement proof, and the 3–4–5 case. The geometric dissection itself is not formalized.
-- Source: https://lurch.plus/100/

-- A square of side a+b, minus four triangles of area a*b/2.
-- The four triangle areas add to 2*a*b, so no fractions remain.
theorem rearrangement (a b : Int) :
    (a + b)^2 - 2*a*b = a^2 + b^2 := by
  grind

-- If the remaining square has area c², the identity follows.
theorem pythagoras_from_areas (a b c : Int)
    (area : c^2 = (a+b)^2 - 2*a*b) : a^2+b^2 = c^2 := by
  grind

example : (3 : Nat)^2 + 4^2 = 5^2 := by decide

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`grind`

Combines logical reasoning and polynomial normalization to construct a proof term that Lean checks.

`Int`

Exact integers, including negatives. Unlike Nat subtraction, integer subtraction does not truncate at zero.

Background and proof scope

c. 500 BCE · Pythagorean tradition

The familiar 3–4–5 triangle is one exact integer example.

Proves the square-area identity used in a rearrangement proof, and the 3–4–5 case. The geometric dissection itself is not formalized.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

File checked successfully.

Exercise

Check the 5–12–13 triangle, then explore the general triple generator in the library.