import Mathlib.Tactic
/-!
# British Mathematical Olympiad 2024, Round 1, Problem 4
Find all positive integers n such that n × 2ⁿ + 1 is a square.
The answer is n = 2 and n = 3.
We follow the presentation by the problem author in https://eventuallyalmosteverywhere.wordpress.com/2024/01/10/finitely-many-solutions/, with modifications.
-/
namespace UK2024R1P4
/- determine -/ abbrev SolutionSet : Set ℕ := sorry
theorem uk2024_r1_p4 (n : ℕ) (hn : 0 < n) :
n ∈ SolutionSet ↔ IsSquare (n * 2 ^ n + 1) := sorry
end UK2024R1P4
This problem has a complete formalized solution.