[proofplan]
We construct the natural homomorphism from the polynomial algebra on formal generators $t_r$ to symmetric functions by sending $t_r$ to the stable elementary symmetric function $e_r$. The key finite input is the finite fundamental theorem: in $n$ variables, the elementary symmetric polynomials $e_{1,n},\dots,e_{n,n}$ form algebraically independent generators of $k[x_1,\dots,x_n]^{S_n}$. Injectivity follows by specialising to sufficiently many variables, while surjectivity follows degree by degree: a homogeneous symmetric function of degree $d$ is already determined in $d$ variables and is therefore a polynomial in $e_1,\dots,e_d$.
[/proofplan]
[step:Define the stable elementary symmetric functions and the comparison map]
For each $n \geq 1$, let
\begin{align*}
R_n := k[x_1,\dots,x_n]^{S_n}
\end{align*}
be the $k$-algebra of symmetric polynomials in $n$ variables. For $n \geq 1$, define the specialisation homomorphism
\begin{align*}
\rho_n: R_{n+1} &\to R_n \\
f(x_1,\dots,x_{n+1}) &\mapsto f(x_1,\dots,x_n,0).
\end{align*}
The graded ring $\operatorname{Sym}(k)$ consists of compatible sequences $(f_n)_{n\geq 1}$, with $f_n \in R_n$, satisfying $\rho_n(f_{n+1})=f_n$, and with bounded total degree.
For $1 \leq r \leq n$, define the $r$th elementary symmetric polynomial in $n$ variables by
\begin{align*}
e_{r,n} := \sum_{1 \leq i_1 < \cdots < i_r \leq n} x_{i_1}\cdots x_{i_r} \in R_n,
\end{align*}
and set $e_{r,n}:=0$ when $r>n$. Since $\rho_n(e_{r,n+1})=e_{r,n}$, the sequence
\begin{align*}
e_r := (e_{r,n})_{n\geq 1}
\end{align*}
defines a homogeneous element of $\operatorname{Sym}(k)$ of degree $r$.
Therefore there is a unique graded $k$-algebra homomorphism
\begin{align*}
\Phi: k[t_1,t_2,t_3,\dots] &\to \operatorname{Sym}(k) \\
t_r &\mapsto e_r,
\end{align*}
where $\deg(t_r)=r$.
[/step]
[step:Use the finite fundamental theorem in each number of variables]
We use the following finite form of the [fundamental theorem of symmetric polynomials](/theorems/5179): for each $n \geq 1$, the homomorphism
\begin{align*}
k[t_1,\dots,t_n] &\to R_n \\
t_r &\mapsto e_{r,n}
\end{align*}
is an isomorphism of graded $k$-algebras.
Here is the proof. Order monomials $x_1^{a_1}\cdots x_n^{a_n}$ lexicographically, and for a symmetric polynomial choose a highest monomial whose exponent vector is weakly decreasing:
\begin{align*}
a_1 \geq a_2 \geq \cdots \geq a_n \geq 0.
\end{align*}
Define non-negative integers
\begin{align*}
b_i := a_i-a_{i+1} \quad (1 \leq i < n), \qquad b_n := a_n.
\end{align*}
Then the product
\begin{align*}
(e_1^{(n)})^{b_1}(e_2^{(n)})^{b_2}\cdots(e_n^{(n)})^{b_n}
\end{align*}
has highest monomial $x_1^{a_1}\cdots x_n^{a_n}$ with coefficient $1$. Subtracting the corresponding scalar multiple eliminates the highest monomial of the given symmetric polynomial. Since a polynomial has only finitely many monomials, repeating this process terminates and expresses every element of $R_n$ as a polynomial in $e_{1,n},\dots,e_{n,n}$.
The same triangular highest-monomial argument also proves algebraic independence: distinct monomials in $e_{1,n},\dots,e_{n,n}$ have distinct highest monomials in $k[x_1,\dots,x_n]$. Hence no non-zero polynomial relation among $e_1^{(n)},\dots,e_n^{(n)}$ can vanish. Thus the displayed homomorphism is an isomorphism.
[guided]
The finite theorem says that symmetric polynomials in $n$ variables are exactly polynomials in the elementary symmetric polynomials. We prove it because this is the only finite-variable input needed later.
Let $f \in R_n$ be a symmetric polynomial. We order monomials lexicographically. Because $f$ is symmetric, if a monomial
\begin{align*}
x_1^{c_1}\cdots x_n^{c_n}
\end{align*}
appears in $f$, then every permutation of the exponent vector also appears with the same coefficient. Therefore the highest monomial appearing in $f$ may be written with weakly decreasing exponents
\begin{align*}
a_1 \geq a_2 \geq \cdots \geq a_n \geq 0.
\end{align*}
Define
\begin{align*}
b_i := a_i-a_{i+1} \quad (1 \leq i < n), \qquad b_n := a_n.
\end{align*}
These are non-negative integers, and they recover the exponent vector by
\begin{align*}
a_j = b_j+b_{j+1}+\cdots+b_n.
\end{align*}
Now consider
\begin{align*}
E := (e_{1,n})^{b_1}(e_{2,n})^{b_2}\cdots(e_{n,n})^{b_n}.
\end{align*}
The highest monomial of $e_{r,n}$ is $x_1\cdots x_r$. Hence the highest monomial of $E$ is
\begin{align*}
\prod_{r=1}^n (x_1\cdots x_r)^{b_r}
=
x_1^{b_1+\cdots+b_n}x_2^{b_2+\cdots+b_n}\cdots x_n^{b_n}
=
x_1^{a_1}\cdots x_n^{a_n},
\end{align*}
and its coefficient is $1$.
If the coefficient of $x_1^{a_1}\cdots x_n^{a_n}$ in $f$ is $c \in k$, then $f-cE$ has strictly smaller highest monomial. Repeating this finite descent expresses $f$ as a polynomial in $e_{1,n},\dots,e_{n,n}$.
The same triangular structure proves algebraic independence. A monomial
\begin{align*}
(t_1)^{b_1}\cdots(t_n)^{b_n}
\end{align*}
maps to an element whose highest monomial has exponent vector
\begin{align*}
(b_1+\cdots+b_n,\ b_2+\cdots+b_n,\ \dots,\ b_n).
\end{align*}
Different exponent vectors $(b_1,\dots,b_n)$ give different highest monomials. Therefore a non-zero polynomial in $t_1,\dots,t_n$ cannot map to zero, because its largest surviving image monomial cannot cancel with any other. Thus
\begin{align*}
k[t_1,\dots,t_n] \cong k[x_1,\dots,x_n]^{S_n}.
\end{align*}
[/guided]
[/step]
[step:Prove injectivity by specialising to sufficiently many variables]
Let $P \in k[t_1,t_2,t_3,\dots]$ satisfy $\Phi(P)=0$. Since $P$ is a polynomial, it involves only finitely many variables; choose $N \geq 1$ such that $P \in k[t_1,\dots,t_N]$.
The $N$-variable component of $\Phi(P)$ is
\begin{align*}
P(e_{1,N},\dots,e_{N,N}) \in R_N.
\end{align*}
Because $\Phi(P)=0$ in $\operatorname{Sym}(k)$, this component is zero. By the finite algebraic independence proved above, the homomorphism
\begin{align*}
k[t_1,\dots,t_N] \to R_N
\end{align*}
is injective. Hence $P=0$. Therefore $\Phi$ is injective.
[/step]
[step:Show that every homogeneous symmetric function is generated by the stable elementary functions]
Let $f=(f_n)_{n\geq 1}\in \operatorname{Sym}(k)$ be homogeneous of degree $d$. If $d=0$, then $f$ is a scalar element of $k$, hence lies in the image of $\Phi$. Assume $d\geq 1$.
By the finite theorem applied in $d$ variables, there exists a polynomial
\begin{align*}
P \in k[t_1,\dots,t_d]
\end{align*}
which is homogeneous for the grading $\deg(t_r)=r$ and satisfies
\begin{align*}
f_d = P(e_{1,d},\dots,e_{d,d}).
\end{align*}
Define
\begin{align*}
g := \Phi(P)=P(e_1,\dots,e_d)\in \operatorname{Sym}(k).
\end{align*}
We prove $g=f$.
For every $n\geq d$, let $R_{n,d} \subset R_n$ denote the homogeneous degree-$d$ component. The degree-$d$ specialisation map
\begin{align*}
\rho_{n,d}: R_{n+1,d} \to R_{n,d}
\end{align*}
is an isomorphism.
To justify this, define a partition of $d$ with length at most $n$ to be a weakly decreasing sequence $\lambda=(\lambda_1,\dots,\lambda_n)$ of non-negative integers with $\lambda_1+\cdots+\lambda_n=d$. For such a partition, define the monomial symmetric polynomial
\begin{align*}
m_{\lambda,n}:=\sum_{\alpha \in S_n\cdot \lambda} x_1^{\alpha_1}\cdots x_n^{\alpha_n}\in R_{n,d},
\end{align*}
where $S_n\cdot \lambda$ denotes the set of distinct permutations of the exponent vector $\lambda$. The monomials $x_1^{\alpha_1}\cdots x_n^{\alpha_n}$ form a $k$-basis of the homogeneous degree-$d$ component of $k[x_1,\dots,x_n]$, and the $S_n$-orbits of exponent vectors of total degree $d$ are indexed exactly by partitions of $d$ of length at most $n$. Therefore a homogeneous polynomial is symmetric if and only if its coefficients are constant on these orbits, so the polynomials $m_{\lambda,n}$ form a $k$-basis of $R_{n,d}$ over the arbitrary base ring $k$.
Every partition of $d$ has length at most $d$. Hence, once $n\geq d$, the specialisation $x_{n+1}=0$ sends $m_{\lambda,n+1}$ to $m_{\lambda,n}$ for every partition $\lambda$ of $d$, and it preserves exactly the same degree-$d$ monomial symmetric basis. Thus $\rho_{n,d}:R_{n+1,d}\to R_{n,d}$ is an isomorphism.
Since both $f$ and $g$ are compatible sequences and have equal $d$-variable component, the isomorphism of the maps $\rho_{n,d}$ for $n\geq d$ implies
\begin{align*}
f_n=g_n
\end{align*}
for every $n\geq d$. For $n<d$, compatibility gives
\begin{align*}
f_n
=
\rho_n\circ\rho_{n+1}\circ\cdots\circ\rho_{d-1}(f_d)
=
\rho_n\circ\rho_{n+1}\circ\cdots\circ\rho_{d-1}(g_d)
=
g_n.
\end{align*}
Thus $f=g=\Phi(P)$, so every homogeneous element of $\operatorname{Sym}(k)$ lies in the image of $\Phi$.
[/step]
[step:Pass from homogeneous elements to the whole graded ring]
Every element of $\operatorname{Sym}(k)$ is a finite sum of homogeneous elements because $\operatorname{Sym}(k)$ is graded by total degree and its elements have bounded degree. The previous step shows that each homogeneous summand lies in the image of $\Phi$. Since $\Phi$ is a graded $k$-algebra homomorphism, the whole finite sum lies in the image of $\Phi$.
Therefore $\Phi$ is surjective. Together with injectivity, this proves that
\begin{align*}
\Phi: k[t_1,t_2,t_3,\dots] \to \operatorname{Sym}(k)
\end{align*}
is an isomorphism of graded $k$-algebras. Renaming $t_r$ as $e_r$ gives
\begin{align*}
\operatorname{Sym}(k)\cong k[e_1,e_2,e_3,\dots],
\end{align*}
with $\deg(e_r)=r$.
[/step]
