You may be interested in Richardson's theorem, which implies that the problem of determining for a given mathematical expression $E(x)$ whether $E(x)=0$ for all $x$ is undecidable. Not only is there no computable algorithm to determine the answers to all such questions, but for any given axiomatic system such as ZFC there are some expressions $E$ for which the fact of the matter of whether $E(x)$ is identically $0$ is not settled by those axioms.

You may be interested in Richardson's theorem, an amazing theorem which implies that the problem of determining for a given mathematical expression $E(x)$, of particularly simple form, whether $E(x)=0$ for all real $x$ is undecidable. Not only is there no computable algorithm to determine the answers to all such questions, but for any given axiomatic system such as ZFC there are some expressions $E$ for which the fact of the matter of whether $E(x)$ is identically $0$ is not settled by those axioms.