$K[[X]]$ is not a finitely generated $K[X]$-module.

The inclusion of rings $j:K[X] \hookrightarrow K[[X]]$ induces a map $j^\ast: \operatorname {Spec}(K[[X]])\to \operatorname {Spec}(K[X])$ between the corresponding sets of prime ideals of these rings.
If $K[[X]]$ were module-finite (or even just integral) over $K[X]$, the map $j^\ast: \operatorname {Spec}(K[[X]])\to \operatorname {Spec}(K[X])$ would be surjective: Atiyah-Macdonald, Theorem 5.10 .
But this is impossible since $K[[X]]$ (like all discrete valuation rings) has only two prime ideals, whereas $K[X]$ has infinitely many (by a variation of Euclid's proof of the infinitude of prime integers).


In $K[[X]]$, the element $f=\sum_{i=0}^\infty X^i$ is an inverse of $1-X$. Since $K[X]$ is integrally closed (even a PID), $(1-X)^{-1}$ can't be integral over $K[X]$. Therefore $K[X][f] \subseteq K[[X]]$ is a not f.g submodule. Since $K[X]$ is Noetherian (by Hilbert Basis Theorem), we can conclude that $K[[X]]$ can't be finitely generated either.


Inspired by the counting suggested by Hagen, here is a proof that shows $K[[X]]$ is not even of finite type over $K[X]$.

First, note that this holds when $K$ is at most countable, for in this case $K[X]$ is countable while $K[[X]]$ is uncountable, and any ring of finite type over a countable ring is still countable.

Now the general case. Suppose $K[[X]]=K[X,f_1,\dots,f_n]$. Let $k$ be the field generated by the prime field of $K$ (namely $\mathbb Q$ or $\mathbb F_p$) and the (countably many) coefficients of $f_i$. Then $k$ is countable. By the above argument, $k[[X]]$ is not of finite type over $k[X]$, so there is $g\in k[[X]]$ such that $g\notin k[X,f_1,\dots,f_n]$. This means that, for any $N\in\mathbb N$, the equation

$$ g=\sum_{\alpha_i\le N\atop\deg p_\alpha\le N} p_\alpha f_1^{\alpha_1}\cdots f_n^{\alpha_n} \tag{*}$$

has no solution $p_{\alpha}\in k[X]$. This can be thought of an (infinite) system of linear equations in the finitely many (in fact $(N+1)^{n+1})$ coefficients of $p_\alpha$, whose own coefficients lie in $k$. Since it has no nonzero solution in $k$, finitely many of the equations already has no nonzero solution in $k$. Since the existence of nonzero solutions to a system of linear equations does not depend on the ground field, the same finitely many equations has no nonzero solution in the larger field $K$, and hence the system as a whole has no nonzero solution $K$. This implies that (*) is not satisfiable either in $K$. Since this is true for any $N\in\mathbb N$, $g\notin K[X,f_1,\dots,f_n]$.