We could encode several interesting YES/NO questions into one YES/NO question with a suitable function, for example XOR:

Is it true that the number of YES answers to the following questions is even? 1. Is P=NP? 2. Is the Riemann hypothesis true? 3. Is Goldbach's conjecture true? ... 100. Is $\pi$ normal?

Since we are promised a proof, it would seem we would get a lot of proofs for the price of one (reminiscent of the fairy-tale trick "I wish for 100 more wishes"). It is difficult to see how one could prove that number to be even (or odd) without proving all sub-questions.

Not sure if the alien civilization would accept this trick. Maybe we should first ask if this is allowed. (Oops, there went our one question.)