Let $X$ be a set. If $X$ is finite then all ultrafilters on $X$ are principal, i.e. have the form $\{A \subseteq X : x \in A\}$ for some $x\in X$.
But now suppose $X$ is infinite, say $X=\mathbb N$. Is there any concrete example of a non-principal ultrafilter on $X$? And does one need the axiom of choice to prove their existence?
There is no explicit example of a non-principal ultrafilter over the natural numbers without appealing to choice.
We know this because there are models of $\sf ZF$ where every ultrafilter over the natural numbers is principal. In fact there are models where every ultrafilter over any set is principal.
The proofs are quite technical and require understanding of forcing and symmetric extensions, or relative constructibility.