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.

def Imo1960Q1.sumOfSquares (L : List ℕ) : ℕ

def Imo1960Q1.ProblemPredicate (n : ℕ) : Prop

def Imo1960Q1.SolutionPredicate (n : ℕ) : Prop

theorem Imo1960Q1.not_zero {n : ℕ} (h1 : Imo1960Q1.ProblemPredicate n) : n ≠ 0

theorem Imo1960Q1.ge_100 {n : ℕ} (h1 : Imo1960Q1.ProblemPredicate n) : 100 ≤ n

theorem Imo1960Q1.lt_1000 {n : ℕ} (h1 : Imo1960Q1.ProblemPredicate n) : n < 1000

def Imo1960Q1.SearchUpTo (c : ℕ) (n : ℕ) : Prop

theorem Imo1960Q1.searchUpTo_start : Imo1960Q1.SearchUpTo 9 99

theorem Imo1960Q1.searchUpTo_step {c : ℕ} {n : ℕ} (H : Imo1960Q1.SearchUpTo c n) {c' : ℕ} {n' : ℕ} (ec : c + 1 = c') (en : n + 11 = n') {l : List ℕ} (el : Nat.digits 10 n = l) (H' : c = Imo1960Q1.sumOfSquares l → c = 50 ∨ c = 73) : Imo1960Q1.SearchUpTo c' n'

theorem Imo1960Q1.searchUpTo_end {c : ℕ} (H : Imo1960Q1.SearchUpTo c 1001) {n : ℕ} (ppn : Imo1960Q1.ProblemPredicate n) : Imo1960Q1.SolutionPredicate n

theorem Imo1960Q1.right_direction {n : ℕ} : Imo1960Q1.ProblemPredicate n → Imo1960Q1.SolutionPredicate n

theorem Imo1960Q1.left_direction (n : ℕ) (spn : Imo1960Q1.SolutionPredicate n) : Imo1960Q1.ProblemPredicate n

theorem imo1960_q1 (n : ℕ) : Imo1960Q1.ProblemPredicate n ↔ Imo1960Q1.SolutionPredicate n