This question arose from a [now removed] MathOverflow discussion, where a Null result from a FindInstance query was used to prove that $f(x_1,x_2,\ldots x_n)\neq 0$ has no solution in $\mathbb{R}$. My question is under which conditions does FindInstance perform an exhaustive search, so that a Null answer can indeed be interpreted as a proof.

An older question answers "No, a Null result does not prove anything", which may well be the case in general, but I suspect there are cases when FindInstance does perform an exhaustive search. In particular, if the search domain is compact and the function $f$ is continuous, is the search exhaustive?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.