This is not necessarily true. It is possible for all real numbers (and indeed all mathematical objects) to be definable under ZFC. It is also possible for that not to be the case. ZFC is mum on the issue.

I've commented on this several times. Here's the most recent one: https://news.ycombinator.com/item?id=44366342

Basically you can't do a standard countability argument because you can't enumerate definable objects because you can't uniformly define "definability." The naive definition falls prey to Liar's Paradox type problems.

I think you're overthinking it. Define a "number definition system" to be any (maybe partial) mapping from finite-length strings on a finite alphabet to numbers. The string that maps to a number is the number's definition in the system. Then for any number definition system, almost all real numbers have no definition.