Number theory

Using the core math library

Import a core module, reuse a library theorem, and prove a concrete large-number GCD equality.

import Init.Data.Nat.Gcd

-- Init ships with Lean. This example does not require Mathlib.
-- Reuse a general theorem rather than proving it again.
example (a b : Nat) : Nat.gcd a b = Nat.gcd b a :=
  Nat.gcd_comm a b

-- A concrete equality, proved by a decision procedure.
example :
    Nat.gcd (2^100 - 1) (2^60 - 1) = 2^20 - 1 := by
  decide

#eval Nat.gcd (2^100 - 1) (2^60 - 1)

Explanation

`import Init.Data.Nat.Gcd`

Loads the core greatest-common-divisor module. Init is already available in this browser runtime.

`Nat.gcd_comm`

A library theorem that proves the GCD is unchanged when its arguments are swapped. Its parameters are the two natural numbers.

`by decide`

Proves this concrete equality using Lean’s decision procedure. norm_num is a different tactic supplied by Mathlib, which is not included here.

`Init · Std · Mathlib`

Init is the core library. Std adds programming data structures and utilities. Mathlib is the community mathematics library, including algebraic hierarchies and analysis. Only Init is bundled here.

Expected output

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

Exercise

Change the exponents to 24, 16, and 8. Check the new equality and its numerical result.