Solution (source code)

= Solution

\b[Yes.] Order the proper filters containing the <cofinite filter> by inclusion. The union of every chain is again a proper filter containing $\mathcal F$: any finite collection of its members already lies in one filter in the chain. <Zorn lemma> gives a maximal proper filter $\mathcal U$.

A maximal proper filter is an <ultrafilter>. Indeed, if $A\notin\mathcal U$, adjoining $A$ cannot generate another proper filter, so some $U\in\mathcal U$ has $U\cap A=\varnothing$. Thus $U\subseteq A^c$, and upward closure gives $A^c\in\mathcal U$. Finally, $\mathcal U$ cannot equal any principal ultrafilter $\mathcal U_n$, because it contains the cofinite set $\mathbb N\setminus\{n\}$ whereas $\mathcal U_n$ does not. Thus $\mathcal U$ is a <nonprincipal ultrafilter> on $\mathbb N$.