Every algebraic number is a critical value of an integer polynomial

A mix of human-written and AI-generated textHuman understanding: all partsmath.NT — Number Theory

Contributed by RJ Acuna

Version 2 / Oct 21, 2026 / CC BY 4.0

Abstract

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. We classify

g \in \mathbb{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.

Richard Dedekind. Über den Zusammenhang zwischen der Theorie der Ideale und der Theorie der höheren Kongruenzen. Abhandlungen der Königlichen Gesellschaft der Wissenschaften zu Göttingen , 1878.
Albert Schwarz, Vadim Vologodsky, and Johannes Walcher. Integrality of Framing and Geometric Origin of 2-functions . https://arxiv.org/abs/1702.07135, 2017.link
The mathlib Community. The L ean Mathematical Library. In Certified Programs and Proofs (CPP 2020) . ACM, 2020.
Leonardo de Moura and Sebastian Ullrich. The L ean 4 Theorem Prover and Programming Language. In Automated Deduction -- CADE 28 , Lecture Notes in Computer Science. Springer, 2021.
Fedor Petrov. Answer to ``When $p(x)^{2} \mid f(g(x))$ ?''. https://mathoverflow.net/q/397800, 2021.link
RJ Acuña. Critical values of integer polynomials: an online calculator . https://rjacuna.github.io/CriticalValues/, 2026.link
RJ Acuña. CriticalValues : paper, L ean 4 formalization and calculator . https://github.com/rjacuna/CriticalValues, 2026.link