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.

Equations
Instances For
    Equations
    Instances For
      def Imo1960Q1.SearchUpTo (c : ) (n : ) :
      Equations
      Instances For
        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 lc = 50 c = 73) :