Classic mathematics

Generate Pythagorean triples

Prove Euclid’s identity for arbitrary integer parameters, then generate several Pythagorean triples.

-- Top 100 #23: Generate Pythagorean triples
-- History: c. 300 BCE · Euclid.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Choosing m=2 and n=1 produces the triple 3, 4, 5.
-- Scope: Proves that Euclid’s formula satisfies the equation for all integer parameters. Classification and primitiveness of triples are not claimed.
-- Source: https://lurch.plus/100/

theorem triple_identity (m n : Int) :
    (m^2-n^2)^2 + (2*m*n)^2 = (m^2+n^2)^2 := by
  grind

def main : IO Unit := do
  for m in [2, 3, 4, 5] do
    let n := 1
    IO.println s!"{m*m-n*n}, {2*m*n}, {m*m+n*n}"

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. 300 BCE · Euclid

Choosing m=2 and n=1 produces the triple 3, 4, 5.

Proves that Euclid’s formula satisfies the equation for all integer parameters. Classification and primitiveness of triples are not claimed.

Historical Top 100 list (reproduced by Lurch)

Expected output

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

3, 4, 5
8, 6, 10
15, 8, 17
24, 10, 26

Exercise

Let n vary too. Which outputs have a common factor?