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
      def Imo1960Q1.SearchUpTo (c : ) (n : ) :
      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) :