[proofplan]
Since $K$ is [compact](/page/Compact%20Space) and [metrizable](/page/Metrizable%20Space), it is second-[countable](/page/Countable%20Set), and from the countable base we extract a countable family of [continuous](/page/Continuity) functions that separates the points of $K$. We then form the algebra of all polynomials in these functions with rational coefficients — a countable set. This algebra separates points and contains the constants, so the [Stone-Weierstrass Theorem](/theorems/886) guarantees it is [dense](/page/Dense%20Subset) in $C(K; \mathbb{R})$.
[/proofplan]
[step:Construct a countable family of continuous functions separating points of $K$]
Since $K$ is [compact](/page/Compact%20Space) and metrizable, it is in particular separable (every compact [metrizable space](/page/Metrizable%20Space) has a [countable](/page/Countable%20Set) [dense subset](/page/Dense%20Subset), since one can cover $K$ by finitely many balls of radius $1/m$ for each $m \in \mathbb{N}$ and collect the centres). By the [Equivalence of Separability Conditions in Metrizable Spaces](/theorems/545), $K$ is second-countable: there exists a countable base $\mathcal{B} = \{B_1, B_2, \ldots\}$ for the [topology](/page/Topology) of $K$.
Since $K$ is compact and metrizable, it is a compact Hausdorff space. Every compact Hausdorff space is normal (disjoint [closed sets](/page/Closed%20Set) can be separated by [open sets](/page/Open%20Set)). For each pair $(i, j) \in \mathbb{N} \times \mathbb{N}$ with $\overline{B_i} \subset B_j$, apply [Urysohn's Lemma](/theorems/887) to the normal space $K$ with the disjoint closed sets $\overline{B_i}$ and $K \setminus B_j$: there exists a [continuous function](/page/Continuity%20(Real%20Analysis))
\begin{align*}
g_{ij}: K &\to [0, 1] \\
x &\mapsto \begin{cases} 0 & \text{if } x \in K \setminus B_j \\ 1 & \text{if } x \in \overline{B_i} \end{cases}
\end{align*}
with $0 \le g_{ij}(x) \le 1$ for all $x \in K$, $g_{ij}|_{\overline{B_i}} \equiv 1$, and $g_{ij}|_{K \setminus B_j} \equiv 0$.
The collection $\{g_{ij} : (i,j) \in \mathbb{N} \times \mathbb{N}, \, \overline{B_i} \subset B_j\}$ is countable (as a subset of a countable product $\mathbb{N} \times \mathbb{N}$) and separates points of $K$: given distinct $x, y \in K$, there exists $B_j \in \mathcal{B}$ with $x \in B_j$ and $y \notin B_j$. Since $K$ is regular (compact Hausdorff spaces are regular), there exists $B_i \in \mathcal{B}$ with $x \in B_i$ and $\overline{B_i} \subset B_j$. Then $g_{ij}(x) = 1$ and $g_{ij}(y) = 0$.
Enumerate this family as $\{f_1, f_2, f_3, \ldots\}$.
[guided]
The goal of this step is to find a *countable* family of continuous functions on $K$ that separates points — meaning that for any two distinct points $x, y \in K$, at least one function in the family takes different values at $x$ and $y$. Why is this the right starting point? Because the Stone-Weierstrass theorem tells us that a subalgebra separating points (and satisfying one additional condition) is dense in $C(K; \mathbb{R})$. If we can build such a subalgebra from a *countable* generating set, the resulting algebra of rational-coefficient polynomials will be countable, giving us our countable dense subset.
**Obtaining a countable base.** Since $K$ is compact and metrizable, $K$ is separable: cover $K$ by finitely many open balls of radius $1/m$ for each $m \in \mathbb{N}$ and collect the centres to obtain a countable dense subset. By the [Equivalence of Separability Conditions in Metrizable Spaces](/theorems/545), separability implies second countability in any metrizable space. Fix a countable base $\mathcal{B} = \{B_1, B_2, \ldots\}$ for the topology of $K$.
**Using Urysohn's Lemma to build separating functions.** A compact Hausdorff space is normal (disjoint closed sets can be separated by disjoint open sets), so [Urysohn's Lemma](/theorems/887) applies. For each pair of indices $(i, j) \in \mathbb{N} \times \mathbb{N}$ satisfying $\overline{B_i} \subset B_j$, the sets $\overline{B_i}$ and $K \setminus B_j$ are disjoint and closed. Urysohn's Lemma provides a continuous function
\begin{align*}
g_{ij}: K &\to [0, 1] \\
x &\mapsto \begin{cases} 0 & \text{if } x \in K \setminus B_j \\ 1 & \text{if } x \in \overline{B_i} \end{cases}
\end{align*}
with $g_{ij}|_{\overline{B_i}} \equiv 1$ and $g_{ij}|_{K \setminus B_j} \equiv 0$.
**Why does this family separate points?** Take distinct $x, y \in K$. Since $K$ is Hausdorff, there exists an open set containing $x$ but not $y$; since $\mathcal{B}$ is a base, there exists $B_j \in \mathcal{B}$ with $x \in B_j$ and $y \notin B_j$. Compact Hausdorff spaces are regular, so we can find $B_i \in \mathcal{B}$ with $x \in B_i$ and $\overline{B_i} \subset B_j$. The function $g_{ij}$ then satisfies $g_{ij}(x) = 1$ (since $x \in \overline{B_i}$) and $g_{ij}(y) = 0$ (since $y \in K \setminus B_j$).
**Countability.** The set of pairs $(i,j)$ with $\overline{B_i} \subset B_j$ is a subset of $\mathbb{N} \times \mathbb{N}$, hence countable. Enumerate the resulting family as $\{f_1, f_2, f_3, \ldots\}$.
[/guided]
[/step]
[step:Form the countable algebra of rational polynomials in these functions]
Define the set
\begin{align*}
\mathcal{A}_\mathbb{Q} := \left\{\sum_{\alpha \in F} q_\alpha \, f_1^{\alpha_1} f_2^{\alpha_2} \cdots f_N^{\alpha_N} \;:\; N \in \mathbb{N}, \; F \subset \mathbb{N}_0^N \text{ finite}, \; q_\alpha \in \mathbb{Q}\right\},
\end{align*}
where each element is a finite polynomial expression in the functions $f_1, \ldots, f_N$ (for some $N$) with rational coefficients and non-negative integer exponents, evaluated pointwise on $K$.
The set $\mathcal{A}_\mathbb{Q}$ is [countable](/page/Countable%20Set). For each fixed $N \in \mathbb{N}$, the collection of polynomials in $f_1, \ldots, f_N$ with rational coefficients and total degree at most $D$ is a finite-dimensional rational vector space, hence countable. Taking the union over all $N \in \mathbb{N}$ and all degrees $D \in \mathbb{N}_0$ produces a countable union of countable sets, which is countable.
[guided]
We now build a *countable* subset of $C(K; \mathbb{R})$ that we will show is [dense](/page/Dense%20Subset). The idea is to take all polynomial expressions in the countably many functions $f_1, f_2, \ldots$, but with *rational* coefficients — the rationality is what ensures countability, just as replacing real coefficients by rational ones makes the set of polynomials on $[0,1]$ countable.
Formally, define $\mathcal{A}_\mathbb{Q}$ to be the set of all functions of the form
\begin{align*}
\sum_{\alpha \in F} q_\alpha \, f_1^{\alpha_1} f_2^{\alpha_2} \cdots f_N^{\alpha_N},
\end{align*}
where $N \in \mathbb{N}$, $F$ is a finite subset of multi-indices $\alpha = (\alpha_1, \ldots, \alpha_N) \in \mathbb{N}_0^N$, and $q_\alpha \in \mathbb{Q}$. Each such expression defines a [continuous function](/page/Continuity%20(Real%20Analysis)) on $K$ (being a finite sum of products of continuous functions scaled by constants).
**Counting $\mathcal{A}_\mathbb{Q}$.** Fix $N$ and a degree bound $D$. The set of multi-indices $\alpha \in \mathbb{N}_0^N$ with $|\alpha| = \alpha_1 + \cdots + \alpha_N \le D$ is finite — it has $\binom{N + D}{N}$ elements. A polynomial with these monomials and rational coefficients is determined by a choice of $q_\alpha \in \mathbb{Q}$ for each such $\alpha$, giving a subset of $\mathbb{Q}^{\binom{N+D}{N}}$, which is countable. Taking the union over $N \in \mathbb{N}$ and $D \in \mathbb{N}_0$ yields a countable union of countable sets, hence $\mathcal{A}_\mathbb{Q}$ is countable.
[/guided]
[/step]
[step:Verify that $\mathcal{A}_\mathbb{Q}$ separates points and contains an approximation to every constant]
The family $\{f_1, f_2, \ldots\}$ separates points of $K$ by construction (Step 1). Since each $f_k \in \mathcal{A}_\mathbb{Q}$ (take $N = k$, $\alpha = e_k$, $q_{e_k} = 1$), the set $\mathcal{A}_\mathbb{Q}$ also separates points.
The constant function $\mathbf{1}$ belongs to $\mathcal{A}_\mathbb{Q}$: take $N = 1$, $F = \{0\}$, and $q_0 = 1$, giving the polynomial $1 \cdot f_1^0 = \mathbf{1}$. Therefore $\mathcal{A}_\mathbb{Q}$ contains the constants. In particular, $\mathcal{A}_\mathbb{Q}$ does not vanish identically at any point of $K$.
[/step]
[step:Apply Stone-Weierstrass to the closure of $\mathcal{A}_\mathbb{Q}$]
Let $A$ denote the $\mathbb{R}$-subalgebra of $C(K; \mathbb{R})$ generated by $\{f_1, f_2, \ldots\}$ and the constant functions. Concretely, $A$ consists of all real polynomial expressions in the $f_k$. Since $\mathcal{A}_\mathbb{Q} \subset A$ (every rational polynomial is a real polynomial), we have $\overline{\mathcal{A}_\mathbb{Q}} \supset \overline{A}$ once we show $A \subset \overline{\mathcal{A}_\mathbb{Q}}$ — or we can bypass $A$ entirely and proceed as follows.
The set $\mathcal{A}_\mathbb{Q}$ is itself a subalgebra of $C(K; \mathbb{R})$ over $\mathbb{Q}$, but the Stone-Weierstrass theorem requires an $\mathbb{R}$-subalgebra. Consider instead the closure $\overline{\mathcal{A}_\mathbb{Q}}$ in the [supremum](/page/Supremum%20and%20Infimum) norm. This closure is a closed $\mathbb{R}$-subalgebra of $C(K; \mathbb{R})$: it is closed under addition and scalar multiplication by reals (approximate any real scalar by rationals), and closed under pointwise multiplication (if $g_m \to g$ and $h_m \to h$ uniformly on $K$, then $g_m h_m \to g h$ uniformly, since $K$ is [compact](/page/Compact%20Space) and [continuous](/page/Continuity) functions on $K$ are bounded).
The closed subalgebra $\overline{\mathcal{A}_\mathbb{Q}}$ separates points of $K$ (since $\mathcal{A}_\mathbb{Q} \subset \overline{\mathcal{A}_\mathbb{Q}}$ and $\mathcal{A}_\mathbb{Q}$ separates points) and contains the constant function $\mathbf{1}$ (since $\mathbf{1} \in \mathcal{A}_\mathbb{Q}$). In particular, $\overline{\mathcal{A}_\mathbb{Q}}$ does not vanish at any point.
By the [Stone-Weierstrass Theorem](/theorems/886), applied to the compact Hausdorff space $K$ and the subalgebra $\overline{\mathcal{A}_\mathbb{Q}}$: since $\overline{\mathcal{A}_\mathbb{Q}}$ separates points and does not vanish identically at any point, conclusion (ii) of the theorem (that the closure equals the set of functions vanishing at some $x_0$) is excluded. Therefore conclusion (i) holds:
\begin{align*}
\overline{\overline{\mathcal{A}_\mathbb{Q}}} = C(K; \mathbb{R}).
\end{align*}
Since $\overline{\mathcal{A}_\mathbb{Q}}$ is already closed, $\overline{\mathcal{A}_\mathbb{Q}} = C(K; \mathbb{R})$.
[guided]
This is the heart of the proof: connecting the [countable](/page/Countable%20Set) algebra to all of $C(K; \mathbb{R})$ via Stone-Weierstrass. The key subtlety is that the Stone-Weierstrass theorem applies to *real* subalgebras, while $\mathcal{A}_\mathbb{Q}$ is only closed under rational operations. How do we bridge this gap?
The simplest approach is to take the closure $\overline{\mathcal{A}_\mathbb{Q}}$ in the supremum norm and verify that it is a closed $\mathbb{R}$-subalgebra.
**Closure under real scalar multiplication.** Let $g \in \overline{\mathcal{A}_\mathbb{Q}}$ and $c \in \mathbb{R}$. Choose a sequence $\{p_m\} \subset \mathcal{A}_\mathbb{Q}$ with $\|p_m - g\|_{C(K)} \to 0$. For each $m$, choose $r_m \in \mathbb{Q}$ with $|r_m - c| < 1/m$. Then $r_m p_m \in \mathcal{A}_\mathbb{Q}$ and
\begin{align*}
\|r_m p_m - c g\|_{C(K)} &\le \|r_m p_m - c p_m\|_{C(K)} + \|c p_m - c g\|_{C(K)} \\
&= |r_m - c| \cdot \|p_m\|_{C(K)} + |c| \cdot \|p_m - g\|_{C(K)}.
\end{align*}
Since $\|p_m\|_{C(K)}$ is bounded (convergent sequences are bounded) and both $|r_m - c|$ and $\|p_m - g\|_{C(K)}$ tend to $0$, we conclude $r_m p_m \to cg$ in $C(K)$, so $cg \in \overline{\mathcal{A}_\mathbb{Q}}$.
**Closure under multiplication.** If $g, h \in \overline{\mathcal{A}_\mathbb{Q}}$ with approximating sequences $\{p_m\}, \{q_m\} \subset \mathcal{A}_\mathbb{Q}$, then $p_m q_m \in \mathcal{A}_\mathbb{Q}$ and
\begin{align*}
\|p_m q_m - g h\|_{C(K)} &\le \|p_m q_m - g q_m\|_{C(K)} + \|g q_m - g h\|_{C(K)} \\
&\le \|p_m - g\|_{C(K)} \cdot \|q_m\|_{C(K)} + \|g\|_{C(K)} \cdot \|q_m - h\|_{C(K)} \to 0,
\end{align*}
so $gh \in \overline{\mathcal{A}_\mathbb{Q}}$.
Thus $\overline{\mathcal{A}_\mathbb{Q}}$ is a closed $\mathbb{R}$-subalgebra of $C(K; \mathbb{R})$. It separates points (since $\{f_1, f_2, \ldots\} \subset \mathcal{A}_\mathbb{Q} \subset \overline{\mathcal{A}_\mathbb{Q}}$) and contains the constant function $\mathbf{1}$ (since $\mathbf{1} \in \mathcal{A}_\mathbb{Q}$). The Stone-Weierstrass theorem presents a dichotomy for a point-separating subalgebra $A$: either $\overline{A} = C(K; \mathbb{R})$, or $\overline{A}$ consists of all functions vanishing at some [fixed point](/page/Fixed%20Points%20of%20Maps) $x_0$. Since $\overline{\mathcal{A}_\mathbb{Q}}$ contains $\mathbf{1}$, which does not vanish anywhere, the second alternative is impossible. Therefore:
\begin{align*}
\overline{\mathcal{A}_\mathbb{Q}} = C(K; \mathbb{R}).
\end{align*}
[/guided]
[/step]
[step:Conclude that $C(K; \mathbb{R})$ is separable]
The set $\mathcal{A}_\mathbb{Q}$ is a [countable](/page/Countable%20Set) subset of $C(K; \mathbb{R})$ (established in Step 2) and is [dense](/page/Dense%20Subset) in $C(K; \mathbb{R})$ with respect to the [supremum](/page/Supremum%20and%20Infimum) norm (established in Step 4: $\overline{\mathcal{A}_\mathbb{Q}} = C(K; \mathbb{R})$). Therefore $C(K; \mathbb{R})$ contains a countable dense subset, which is the definition of separability.
[/step]