Thanks for the heads-up. So I was indeed right to be surprised :D At least my answer wasn't completely redundant by contributing some new pieces of information behind the story.

indicative of scientific marketing departments (overly optimistic, using a type of survival bias to selectively highlight only those few milestone conjectures that were experimentally discovered); also, their framework isn't as new as one might think it is, see e.g. link.springer.com/article/10.1007/JHEP09(2017)157 ) or 2) by someone who is rather very skeptical of the impact of their method and tries to see, aside from the AI aspect, how important their mathematical result is considered to be by the larger community.

Reading the edits (and taking into account the original title), as well as the language of the question as it stands now, this question seems to be posed either 1) by someone at DeepMind to hype their paper and increase visibility by asking related questions about their result (lately they seem to have been promoting their research rather aggressively; if one reads the Nature paper, their abstract is ridiculous, as the language they use is [...]

Thanks, this really was very helpful!

@WillSawin Just for fun, could you link one paper (perhaps a survey paper, if there is one) that describes some unknown things in case of the rationals?

@tim Thanks a lot, that library would be perfect - if it were open-source. I will need eventually to publish some part of the code and using non open-source software is not so well received in my community. Do you happen to know if there are any open-source packages that offer similar functionality? If I were to use RAGlib, do you now of any publication or article that provides details about the algorithms RAGlib uses internally? I couldn't find much documentation on the website; if I download it, there are only a few files containing examples and explanations how to use the library.

[...] I guess for (1) you are alluding to something like Khovanskii's fewnomials approach, about which I learned in the previous question, that seems to be a generalization of Descartes' rules of signs?

[...] Now that this is clarified, could you please let me know of some (ideally introductory) references regarding the quantifier elimination method that you mentioned, as well as decidability procedure to decide whether a semi-algebraic set is a neighbourhood of 0?

@FrançoisBrunault From your last comment, I realized that I think you misunderstood me, resp. I misunderstood you (depending on the viewpoint). When I mentioned I was doing computations in floating-point, I referred to the fact that the input of my coefficients are only with floating point numbers (since that is what I can input in a CAS; and I'm happy with that, that is ok) - and not that my coefficients are other some numbers that I then approximate with floating-point precision before running any algo on them (which is what you had in mind). So in this sense my coefficients are exact! [...]

Regarding floating-point: I can't quite follow you: Why is it not possible to decide if the answer is correct? Would you say, from an algorithmic/simulation standpoint, that it would be better to work with $\mathbb{Z}[x_1,\ldots,x_n]$?

@FrançoisBrunault Well, by necessity I need to use floating point, since I don't know of a different way to carry out solving the mentioned $10^4$ systems, where the coefficients discretize a high-dimensional cube (though, afterwards, when I want to prove theorems, which is the final goal, of course I will work with coefficient from $\mathbb{R}$).