IMO_2006_Pb_4.lean

import data.pnat.basic
import data.int.basic
import data.real.basic
import analysis.special_functions.exp_log
import algebra.order.ring
import algebra.ring.basic
import tactic
 

theorem IMO_2006_Pb_4 (a b: ℤ)(h:1+(2:ℝ)^a+(2:ℝ)^(2*a+1)=b^2): (a=0 ∧ (b= 2 ∨ b=-2))∨ (a=4∧ (b=23∨ b=-23)):=
begin
  sorry
end