Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2012P6

import Mathlib

/-!
# International Mathematical Olympiad 2012, Problem 6

Find all positive integers n for which there exist non-negative
integers a₁, a₂, ..., aₙ such that
1/2^a₁ + 1/2^a₂ + ··· + 1/2^aₙ = 1/3^a₁ + 2/3^a₂ + ··· + n/3^aₙ = 1
-/

namespace Imo2012P6


/- determine -/ abbrev solution_set : Set ℕ := sorry

def IsSolution (n : ℕ) : Prop := ∃ a : ℕ → ℕ, 0 < n ∧
  (∑ i ∈ Finset.Icc 1 n, (1 : ℚ) / (2 ^ a i)) = 1 ∧
  (∑ i ∈ Finset.Icc 1 n, (i : ℚ) / (3 ^ a i)) = 1

theorem imo2012_p6 : { n | IsSolution n } = solution_set := sorry

end Imo2012P6

File author(s): Markus Rydh, Codex

This problem has a complete formalized solution.