We arrived at an independent proof of Petrov's theorem: for every irreducible $f \in \mathbb{Z}[x]$ of positive degree there are $g \in \mathbb{Z}[x]$ and an irreducible $F \in \mathbb{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 $\mathbb{Z}[x]$ is exactly $\overline{\mathbb{Q}}$. The construction is explicit. The proof was assisted by AI, and has been formalized in Lean.