IMO 1962 Q1

Find the smallest natural number $n$ which has the following properties:

(a) Its decimal representation has 6 as the last digit.

(b) If the last digit 6 is erased and placed in front of the remaining digits, the resulting number is four times as large as the original number $n$.

Since Lean does not explicitly express problems of the form "find the smallest number satisfying X", we define the problem as a predicate, and then prove a particular number is the smallest member of a set satisfying it.

def Imo1962Q1.ProblemPredicate (n : ℕ) : Prop

Equations

• Imo1962Q1.ProblemPredicate n = ((Nat.digits 10 n).headI = 6 ∧ Nat.ofDigits 10 ((Nat.digits 10 n).tail.concat 6) = 4 * n)

First, it's inconvenient to work with digits, so let's simplify them out of the problem.

@[reducible, inline]

abbrev Imo1962Q1.ProblemPredicate' (c : ℕ) (n : ℕ) : Prop

Equations

• Imo1962Q1.ProblemPredicate' c n = (n = 10 * c + 6 ∧ 6 * 10 ^ (Nat.digits 10 c).length + c = 4 * n)

theorem Imo1962Q1.without_digits {n : ℕ} (h1 : Imo1962Q1.ProblemPredicate n) : ∃ (c : ℕ), Imo1962Q1.ProblemPredicate' c n

Now we can eliminate possibilities for (digits 10 c).length until we get to the one that works.

theorem Imo1962Q1.case_0_digit {c : ℕ} {n : ℕ} (h1 : (Nat.digits 10 c).length = 0) : ¬Imo1962Q1.ProblemPredicate' c n

theorem Imo1962Q1.case_1_digit {c : ℕ} {n : ℕ} (h1 : (Nat.digits 10 c).length = 1) : ¬Imo1962Q1.ProblemPredicate' c n

theorem Imo1962Q1.case_2_digit {c : ℕ} {n : ℕ} (h1 : (Nat.digits 10 c).length = 2) : ¬Imo1962Q1.ProblemPredicate' c n

theorem Imo1962Q1.case_3_digit {c : ℕ} {n : ℕ} (h1 : (Nat.digits 10 c).length = 3) : ¬Imo1962Q1.ProblemPredicate' c n

theorem Imo1962Q1.case_4_digit {c : ℕ} {n : ℕ} (h1 : (Nat.digits 10 c).length = 4) : ¬Imo1962Q1.ProblemPredicate' c n

theorem Imo1962Q1.helper_5_digit {c : ℤ} (h : 6 * 10 ^ 5 + c = 4 * (10 * c + 6)) : c = 15384

Putting this inline causes a deep recursion error, so we separate it out.

theorem Imo1962Q1.case_5_digit {c : ℕ} {n : ℕ} (h1 : (Nat.digits 10 c).length = 5) (h2 : Imo1962Q1.ProblemPredicate' c n) : c = 15384

theorem Imo1962Q1.case_more_digits {c : ℕ} {n : ℕ} (h1 : (Nat.digits 10 c).length ≥ 6) (h2 : Imo1962Q1.ProblemPredicate' c n) : n ≥ 153846

linarith fails on numbers this large, so this lemma spells out some of the arithmetic that normally would be automated.

Now we combine these cases to show that 153846 is the smallest solution.

theorem Imo1962Q1.satisfied_by_153846 : Imo1962Q1.ProblemPredicate 153846

theorem Imo1962Q1.no_smaller_solutions (n : ℕ) (h1 : Imo1962Q1.ProblemPredicate n) : n ≥ 153846

theorem imo1962_q1 : IsLeast {n : ℕ | Imo1962Q1.ProblemPredicate n} 153846