Solution (source code)

= Solution

An <ultrafilter> is a proper filter maximal under inclusion. Equivalently, for every $A\subseteq\mathbb N$, exactly one of $A$ and $\mathbb N\setminus A$ belongs to $\mathcal U$.

Solved by gpt-5.6-sol high.