Solution (source code)

= Solution

Use the usual commutative unital-ring convention for <Noetherian rings>. A ring is Noetherian exactly when every <ideal> is finitely generated, equivalently when ascending chains of <ideals> stabilize. Indeed, the union of an ascending chain is an <ideal>; finitely many generators all lie in a single chain member. Conversely, if an <ideal> cannot be finitely generated, adjoining a new element at each stage constructs a strictly ascending chain.

First assume $R[X]$ is Noetherian. Evaluation at zero gives a surjective <ring homomorphism> $R[X]\to R$ with <kernel> $(X)$. A quotient of a <Noetherian ring> is Noetherian: lift an <ideal> to the source, take finitely many generators there, and map those generators down. Thus $R\cong R[X]/(X)$ is Noetherian.

For the converse, assume $R$ is Noetherian and take any <ideal> $I\subseteq R[X]$. For $d\ge0$, let $J_d$ be the set of coefficients of $X^d$ in elements of $I$ of degree at most $d$. It is an <ideal> of $R$, since sums and scalar multiples of such <polynomials> stay in $I$. Multiplication by $X$ shows $J_d\subseteq J_{d+1}$. The ascending chain stabilizes, say at $N$.

For each $0\le d\le N$, choose finitely many generators $a_{d,j}$ of $J_d$ and corresponding $f_{d,j}\in I$ of degree at most $d$ having coefficient $a_{d,j}$ at $X^d$. Discard zero generators. We claim these finitely many <polynomials> generate $I$. If a nonzero $f\in I$ has degree $m\le N$, express its leading coefficient as $\sum_jr_j a_{m,j}$ and subtract $\sum_jr_jf_{m,j}$. The degree decreases. If $m>N$, use $J_m=J_N$, express the leading coefficient using the $a_{N,j}$, and subtract
$$
\sum_jr_jX^{m-N}f_{N,j}.
$$
Again the leading term cancels and the degree decreases. Induction on degree, including degree zero, expresses every $f$ in the claimed <ideal>. Therefore every <ideal> of $R[X]$ is finitely generated, proving the <Hilbert basis theorem> and
$$
\boxed{R[X]\text{ is Noetherian}\iff R\text{ is Noetherian}.}
$$
The argument is the <bounded-degree coefficient proof of Hilbert basis theorem>; it never divides by a leading coefficient and therefore does not require $R$ to be an <integral domain>. With the analogous left-ideal convention the same proof applies to left-Noetherian rings with a central indeterminate.