# mathlib3documentation

mathlib-archive / imo.imo1960_q1

# 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.

Equations
def imo1960_q1.problem_predicate (n : ) :
Prop
Equations
Equations
theorem imo1960_q1.ge_100 {n : } (h1 : imo1960_q1.problem_predicate n) :
100 n
theorem imo1960_q1.lt_1000 {n : } (h1 : imo1960_q1.problem_predicate n) :
n < 1000
def imo1960_q1.search_up_to (c n : ) :
Prop
Equations
theorem imo1960_q1.search_up_to_step {c n : } (H : n) {c' n' : } (ec : c + 1 = c') (en : n + 11 = n') {l : list } (el : 10.digits n = l) (H' : c = 50 c = 73) :
theorem imo1960_q1.search_up_to_end {c : } (H : 1001) {n : } (ppn : imo1960_q1.problem_predicate n) :
theorem imo1960_q1 (n : ) :