IMO 1960 Q1 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Determine all three-digit numbers $N$ having the property that $N$ is divisible by 11, and $\dfrac{N}{11}$ is equal to the sum of the squares of the digits of $N$.

Since Lean doesn't have a way to directly express problem statements of the form "Determine all X satisfying Y", we express two predicates where proving that one implies the other is equivalent to solving the problem. A human solver also has to discover the second predicate.

The strategy here is roughly brute force, checking the possible multiples of 11.

source

def imo1960_q1.sum_of_squares (L : list ℕ) :

ℕ

Equations

imo1960_q1.sum_of_squares L = (list.map (λ (x : ℕ), x * x) L).sum

source

def imo1960_q1.problem_predicate (n : ℕ) :

Prop

Equations

imo1960_q1.problem_predicate n = ((10.digits n).length = 3 ∧ 11 ∣ n ∧ n / 11 = imo1960_q1.sum_of_squares (10.digits n))

source

def imo1960_q1.solution_predicate (n : ℕ) :

Prop

Equations

imo1960_q1.solution_predicate n = (n = 550 ∨ n = 803)

source

theorem imo1960_q1.not_zero {n : ℕ} (h1 : imo1960_q1.problem_predicate n) :

n ≠ 0

source

theorem imo1960_q1.ge_100 {n : ℕ} (h1 : imo1960_q1.problem_predicate n) :

100 ≤ n

source

theorem imo1960_q1.lt_1000 {n : ℕ} (h1 : imo1960_q1.problem_predicate n) :

n < 1000

source

def imo1960_q1.search_up_to (c n : ℕ) :

Prop

Equations

imo1960_q1.search_up_to c n = (n = c * 11 ∧ ∀ (m : ℕ), m < n → imo1960_q1.problem_predicate m → imo1960_q1.solution_predicate m)

source

theorem imo1960_q1.search_up_to_start :

imo1960_q1.search_up_to 9 99

source

theorem imo1960_q1.search_up_to_step {c n : ℕ} (H : imo1960_q1.search_up_to c n) {c' n' : ℕ} (ec : c + 1 = c') (en : n + 11 = n') {l : list ℕ} (el : 10.digits n = l) (H' : c = imo1960_q1.sum_of_squares l → c = 50 ∨ c = 73) :

imo1960_q1.search_up_to c' n'

source

theorem imo1960_q1.search_up_to_end {c : ℕ} (H : imo1960_q1.search_up_to c 1001) {n : ℕ} (ppn : imo1960_q1.problem_predicate n) :

imo1960_q1.solution_predicate n

source

theorem imo1960_q1.right_direction {n : ℕ} :

imo1960_q1.problem_predicate n → imo1960_q1.solution_predicate n

source

theorem imo1960_q1.left_direction (n : ℕ) (spn : imo1960_q1.solution_predicate n) :

imo1960_q1.problem_predicate n

source

theorem imo1960_q1 (n : ℕ) :

imo1960_q1.problem_predicate n ↔ imo1960_q1.solution_predicate n