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 [1]. 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.

[1] Pascal Koiran, Hilbert’s Nullstellensatz is in the Polynomial Hierarchy, Journal of Complexity 12 (1996), no. 4, pp. 273–286.