Number theory

Euclid’s gcd algorithm

Run an ancient algorithm and reuse its verified properties in your own theorem.

-- Top 100 #69: Euclid’s gcd algorithm
-- History: c. 300 BCE · Euclid.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: The gcd of 1071 and 462 is 21; Euclidean division quickly reduces the inputs.
-- Scope: Uses Lean core’s proved gcd lemmas to establish divisibility of both inputs. The library supplies the algorithm’s correctness proof.
-- Source: https://lurch.plus/100/

theorem gcd_divides_both (a b : Nat) :
    Nat.gcd a b ∣ a ∧ Nat.gcd a b ∣ b := by
  constructor
  · exact Nat.gcd_dvd_left a b
  · exact Nat.gcd_dvd_right a b

example : Nat.gcd 1071 462 = 21 := by decide

def main : IO Unit := do
  IO.println s!"gcd(1071, 462) = {Nat.gcd 1071 462}"
  IO.println s!"gcd(35, 22) = {Nat.gcd 35 22}"

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.

`decide`

Builds a proof using a decision procedure. Here it checks a concrete arithmetic statement.

`Nat`

Nat contains arbitrary-size natural numbers, including zero. Its subtraction stops at zero.

Background and proof scope

c. 300 BCE · Euclid

The gcd of 1071 and 462 is 21; Euclidean division quickly reduces the inputs.

Uses Lean core’s proved gcd lemmas to establish divisibility of both inputs. The library supplies the algorithm’s correctness proof.

Historical Top 100 list (reproduced by Lurch)

Expected output

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

gcd(1071, 462) = 21
gcd(35, 22) = 1

Exercise

Find and evaluate two inputs with gcd 12. Can you prove 12 divides both?