Let $I \subseteq R[x]$ be an ideal. We must show $I$ is finitely generated.

For each $n \geq 0$, define: $I_n = \{a \in R : \text{there exists } f \in I \text{ of degree } \leq n \text{ with leading coefficient } a\} \cup \{0\}$

Claim 1: Each $I_n$ is an ideal of $R$.

If $a, b \in I_n$ with polynomials $f, g \in I$ of degrees $\leq n$ having leading coefficients $a, b$, then (adjusting degrees): $x^{n-\deg f}f + x^{n-\deg g}g \in I$ has degree $\leq n$ and leading coefficient $a + b$. Similarly, for $r \in R$, the polynomial $rf$ has leading coefficient $ra$, so $ra \in I_n$.

Claim 2: We have $I_0 \subseteq I_1 \subseteq I_2 \subseteq \cdots$.

If $a \in I_n$ via polynomial $f$ of degree $\leq n$, then $xf$ has degree $\leq n+1$ with leading coefficient $a$, so $a \in I_{n+1}$.

Claim 3: Since $R$ is Noetherian, the chain stabilizes: $I_N = I_{N+1} = \cdots$ for some $N$.

Step 4: For each $n \leq N$, choose finitely many generators $a_{n,1}, \ldots, a_{n,k_n}$ for $I_n$ (possible since $R$ is Noetherian). For each $a_{n,i}$, choose $f_{n,i} \in I$ of degree $\leq n$ with leading coefficient $a_{n,i}$.

Let $J$ be the ideal generated by all $f_{n,i}$ for $0 \leq n \leq N$. This is a finite set, so $J$ is finitely generated. Clearly $J \subseteq I$.

Step 5: We prove $I \subseteq J$ by induction on degree.

Base case: If $f \in I$ has degree $0$ (constant), then $f \in I_0$, so $f = \sum r_i a_{0,i}$ for some $r_i \in R$. Thus $f = \sum r_i f_{0,i} \in J$.

Inductive step: Suppose $f \in I$ has degree $d > 0$ with leading coefficient $a$.

If $d \leq N$: Then $a \in I_d$, so $a = \sum r_i a_{d,i}$ for $r_i \in R$. Consider: $g = f - \sum r_i f_{d,i}$

Each $f_{d,i}$ has degree $\leq d$, so after adjustment, $g \in I$ has degree $< d$. By induction, $g \in J$, so $f = g + \sum r_i f_{d,i} \in J$.

If $d > N$: Then $a \in I_d = I_N$, so $a = \sum r_i a_{N,i}$. Consider: $g = f - \sum r_i x^{d-N} f_{N,i}$

This polynomial has degree $< d$ (the leading term cancels). By induction, $g \in J$, so $f \in J$.

Therefore $I = J$ is finitely generated, so $R[x]$ is Noetherian.

By induction, if $R$ is Noetherian, then $R[x_1, \ldots, x_n] = R[x_1][x_2]\cdots[x_n]$ is Noetherian, since each single-variable extension preserves the property.

A similar proof shows $R[[x]]$ is Noetherian when $R$ is. The key difference: for power series, "leading coefficient" means the first non-zero coefficient, and degree is replaced by order.

The construction of $I_n$ uses series with order $\geq n$, and stabilization again comes from the Noetherian property of $R$.