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 you have read our privacy policy.