We assume we are given an entire function $f: \mathbb C \to \mathbb C$ with $f(0)=1$ and $f'(0)=0$ and $f$ is real on the real axis.

We assume (as a fact about $f$, that we want to demonstrate computationally using other facts about $f$) that $f$ has a zero of order $2$ at some real $z_0 \in \mathbb R$ and that there is no other zero of $f$ inside the disc of radius $2\vert z_0 \vert$ apart from this one.

We assume we have access to the Taylor expansion of $f$ and any of its derivatives, i.e. we have access to coefficients $a_k(n)$

$$f^{(n)}(z) = \sum_{k=0}^N a_k(n) z^k + R_{N,n}(z),$$ where we also have a bound on $\lvert R_{N,n}(z)\rvert$ for any $z,N,n.$

The task is now: Given $\varepsilon>0$, is it possible to show with the help of a computer that there exists $z_0^* \in \mathbb R$ with $\lvert z_0^*-z_0 \rvert \le \varepsilon$ such that $f$ has a zero of order $2$ at $z_0^*$? Does there exist an algorithmic way for a computer to show this?

To see why the order $2$ is subtle here. If one wanted to show the existence of a zero of order $1$ instead, this would be trivial as it would suffice to show that $f$ changes sign and $f'$ is non-zero in a neighbourhood of where the sign change happens.

8more comments