Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2006P4

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2006, Problem 4

Determine all pairs $(x, y)$ of integers satisfying the equation  $$ 1+2^{x}+2^{2 x+1}=y^{2} . $$
-/

namespace Imo2006P4

/- determine -/ abbrev solution : Set (ℤ × ℤ) := sorry

theorem imo2006_p4 :
    {(x, y) : ℤ × ℤ | 1 + (2 : ℝ) ^ x + 2 ^ (2 * x + 1) = y ^ 2} =
    solution := sorry


end Imo2006P4

File author(s): Project Numina Contributors

This problem has a complete formalized solution.

The solution was imported from https://huggingface.co/datasets/AI-MO/NuminaMath-LEAN.