# Documentation

Archive.Imo.Imo1960Q1

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

Instances For
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 : ) :
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 : ) :