One of the old classic MO questions is a big-list of proofs of the fundamental theorem of algebra. Here is a second big-list question about this big list:
Which of the FTA proofs can, even in principle, be mined to produce bounds on where the roots of a complex polynomial $f(z) = z^n + a_{n-1} z^{n-1} + \dots + a_0 = 0$ are, as a function of its coefficients? Which of them can further be mined to produce algorithms for locating roots?
Here my interest is not in actually having such bounds or algorithms, since clearly there are more direct ways to find them; it's in classifying the proofs based on how effective or explicit they are or can be made.
Example. The proof via Rouche's theorem proceeds as follows: we want to find $R$ such that Rouche's theorem guarantees that $z^n$ and $f(z)$ have the same number of roots in the disk of radius $R$. Rouche's theorem says that it suffices to find $R$ such that $|z^n| > |a_{n-1} z^{n-1} + \dots + a_0|$ for all $|z| = R$. This is guaranteed if we guarantee
$$R^n > |a_{n-1}| R^{n-1} + \dots + |a_0|$$
so we can pick, for example, $R > \text{max}(|a_{n-1}| + \dots + |a_0|, 1)$, and then Rouche's theorem guarantees that $f(z)$ has $n$ roots in the disk of radius $R$.
(Note that the assumption that $z$ is a root of $f(z)$ immediately gives $|z^n| = |a_{n-1} z^{n-1} + \dots + a_0| \ge |a_{n-1}| |z|^{n-1} + \dots + |a_0|$, so we already know that if any roots exist they must lie in this disk; again, my interest isn't in actually having bounds, it's in knowing what bounds can be mined from what proofs!)
This example is relatively straightforward; it's much less clear whether the proofs that proceed via e.g. Liouville's theorem, degree arguments, fundamental group computations, cohomology computations, the Lefschetz fixed point theorem, etc. can be mined to produce bounds, but I have hope that at least some of them can, possibly after substantial effort, and possibly with terrible bounds. For example one might hope to mine a bound from the Lefschetz fixed point argument by bounding how complicated the simplicial subdivision + homotopy to a simplicial map you need is, etc.