Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1968P6

import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Data.Nat.Log
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1968, Problem 6

For every natural number n, evaluate the sum
∑_{k=0}^{∞} [(n + 2^k) / 2^(k+1)]
where [x] denotes the greatest integer less than or equal to x.
-/

namespace Imo1968P6

/--
The answer is n. We pull this into a `determine` statement as required.
-/
/- determine -/ abbrev n_ans (n : ℕ) : ℕ := sorry

theorem imo1968_p6 (n : ℕ) : ∑' k, (n + 2^k) / 2^(k+1) = n_ans n := sorry

end Imo1968P6

File author(s): lean-tom (with assistance from Gemini)

This problem has a complete formalized solution.