# IMO 1960 Q1 #

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
Instances For
Equations
Instances For
Equations
Instances For
theorem Imo1960Q1.not_zero {n : } (h1 : ) :
n 0
theorem Imo1960Q1.ge_100 {n : } (h1 : ) :
100 n
theorem Imo1960Q1.lt_1000 {n : } (h1 : ) :
n < 1000
def Imo1960Q1.SearchUpTo (c : ) (n : ) :
Equations
Instances For
theorem Imo1960Q1.searchUpTo_step {c : } {n : } (H : ) {c' : } {n' : } (ec : c + 1 = c') (en : n + 11 = n') {l : } (el : Nat.digits 10 n = l) (H' : c = 50 c = 73) :
theorem Imo1960Q1.searchUpTo_end {c : } (H : Imo1960Q1.SearchUpTo c 1001) {n : } (ppn : ) :
theorem Imo1960Q1.left_direction (n : ) (spn : ) :
theorem imo1960_q1 (n : ) :