The axiom of constructibility $V=L$ leads to some very interesting consequences, one of which is that it becomes possible to give explicit constructions of some of the "weird" results of AC. For instance, in $L$, there is a definable well-ordering of the real numbers (since there is a definable well-ordering of the universe).
Since AC holds true in $L$, the ultrafilter lemma must be true. Does this mean that a definable non-principal ultrafilter on $\mathbb{N}$ exists in $L$, given by an explicit formula?
If so, what is the formula?