% The abstract, shared by paper/, arxiv/ and AMM/.
We arrived at an independent proof of Petrov's theorem. For every
irreducible $f \in \Z[x]$ of positive degree there are $g \in \Z[x]$ and an
irreducible $F \in \Z[x]$ of positive degree with $F \mid g'$ and
$F^{2} \mid f \circ g$. Equivalently, every algebraic number is a critical
value of an integer polynomial, so the set of critical values of $\Z[x]$ is
exactly $\overline{\Q}$. The construction is explicit. We classify
$g \in \Z[x]$ with critical value $\alpha$, and find a lower bound for
$\deg g$. The proof was assisted by AI, and has been formalized in Lean.