[mag487]

There's only a countable number of formulas of ZFC. Therefore, there's only a countable number ways of writing out a formula of ZFC that uniquely specifies a real number. Therefore, only countably many real numbers exist that have such definitions. And all countable sets of reals have zero Lebesgue measure.

[nawitus]

Additional question: what's the Kolmogorov complexity of a irrational numberwhich is not described with a ZFC formula? And how is it described?

[mag487]

I haven't really studied algorithmic information theory, but I'd assume that Kolmogorov complexity isn't defined for uncomputable/undefinable numbers. Or maybe it's defined as "infinite," but either way, my guess is that such numbers are simply ignored. (Interestingly, the function which takes a computable number and outputs its Kolmogorov complexity is itself uncomputable!)

[nawitus]

The article at least implies that the Kolmogorov complexity of uncomputable irrational numbers is larger than computable irrational numbers.