I wanted to give an easy example of a non-constructive proof, or, more precisely, of a proof which states that an object exists, but gives no obvious recipe to create/find it.
Euclid's proof of the infinitude of primes came to mind, however there is an obvious way to "fix" it: just try all the numbers between the biggest prime and the constructed number, and you'll find a prime in a finite number of steps.
Are there good examples of simple non-constructive proofs which would require a substantial change to be made constructive? (Or better yet, can't be made constructive at all).
The standard proof is non-constructive as it proceeds by showing that the set of non-normal numbers has Lebesgue-measure zero, hence must have non-empty complement.
I don't know if the existence of a computable normal number can be proved, and if yes, if that proof can be made constructive in the sense that one can explicitly write down an algorithm for the construction of a normal number. I'd be most interested in hearing about such a thing in case anyone knows more about it. Until then, I'm not convinced that normal numbers exist in a real sense, but only that they are unavoidable artefacts in a certain logical and set theoretical framework for the real numbers.