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 ℕ) : ℕ

Equations

• Imo1960Q1.sumOfSquares L = (List.map (fun (x : ℕ) => x * x) L).sum

def Imo1960Q1.ProblemPredicate (n : ℕ) : Prop

Equations

• Imo1960Q1.ProblemPredicate n = ((Nat.digits 10 n).length = 3 ∧ 11 ∣ n ∧ n / 11 = Imo1960Q1.sumOfSquares (Nat.digits 10 n))

def Imo1960Q1.SolutionPredicate (n : ℕ) : Prop

Equations

• Imo1960Q1.SolutionPredicate n = (n = 550 ∨ n = 803)

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

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

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

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

Equations

• Imo1960Q1.SearchUpTo c n = (n = c * 11 ∧ ∀ m < n, Imo1960Q1.ProblemPredicate m → Imo1960Q1.SolutionPredicate m)

theorem Imo1960Q1.searchUpTo_start : SearchUpTo 9 99

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

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

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

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

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