It is known that the fundamental group of a manifold must be countable.
As far as I am aware, a proof of this uses in an essential way the Axiom of Countable Choice.
I was wondering: is it consistent with ZF that there exists a manifold with uncountable fundamental group? I wasn't able to find any reference concerning this.
Edit: This result is found, for instance, as Theorem 7.21 in John Lee's book Introduction to Topological Manifolds.
The fundamental group of a second-countable manifold is countable, without any choice.
First, notice that we can find a countable base $B$ such that each basis element is a subset of a contractible set. This implies that for any $U \in B$ and points $x, y \in U$, any two paths from $x$ to $y$ within $U$ are homotopic in the manifold.
By compactness of $[0,1]$, any loop contains a finite sequence of points $x_0, x_1, x_2, \dots, x_n = x_0$ such that the path from $x_{i-1}$ to $x_i$ lies entirely in some $U_i \in B$. Since $B$ is a basis, we can also choose $x_i \in V_i \in B$ such that $V_i$ is contained in a connected component of $U_i \cap U_{i+1}$.
Thus for each loop, we have a (non-unique) description $U_1 \supset V_1 \subset U_2 \supset \cdots \subset U_n$. Since $B$ is countable, there are only countably many such descriptions. All that remains is to show that any two loops admitting the same description are homotopic.
Let $\gamma$ and $\gamma'$ be two loops that admit the same description. We have corresponding sequences of points $x_0, x_1, \dots, x_n$ and $x'_0, x'_1, \dots, x'_n$. Modify $\gamma$ homotopically as follows:
At each $x_i$, add a path through $U_i \cap U_{i+1}$ from $x_i$ to $x'_i$ and back. This is always possible by our restriction on $V_i$.
The loop obtained this way can be partitioned into paths going from $x'_{i-1}$ to $x'_i$ through $U_i$. By our assumption on $B$, these paths are each homotopic to the corresponding paths of $\gamma'$.
Hence $\gamma$ and $\gamma'$ are homotopic, as required.