In the book ‘Computational Complexity’ by Arora and Barak the following question is posed (exercise 2.20.):
Let REALQUADEQ be the language of all satisfiable sets of quadratic equations over real variables. Show that REALQUADEQ is NP-complete.
I know how to show NP-hardness, but I’m stuck when it comes to proving that this problem is in NP, in particular how to show that we can describe a solution using a polynomial number of bits.
I did some research and found out that over the complex numbers, it remains an open question if the problem is in NP . It also seems closely related to the existential theory of the reals, which again is not known to be in NP.
Thus my question: Is this problem known to be in NP? And if so, could somebody point me in the right direction regarding the proof.
 Pascal Koiran, Hilbert’s Nullstellensatz is in the Polynomial Hierarchy, Journal of Complexity 12 (1996), no. 4, pp. 273–286.