Enumeration of proofs Is it possible to enumerate short proofs of short statements, so as to make sure that, say, Goldbach's conjecture doesn't have one of those? How hard would it be? Is it being done?
It's seems likely to me that something interesting might have been missed among short proofs. Though I wouldn't know how short they'd have to be to make it a computationally feasible endeavor, or how hard it would be to tell which statements are interesting.
 A: Yes, it is possible to enumerate short proofs -- in fact, to enumerate all proofs in order from shortest to longer.
However, we should not really expect to learn something interesting that way. There are very many short proofs of completely trivial or inane truths, such as $2+2=4$ or $\forall x.(2+x=1+x+1)$, and simply getting past them in order to find a proof of something interesting would -- for any practical purpose -- take "forever".
The classical way to enumerate all proofs is to enumerate all possible strings of symbols and check for each of them whether it happens to be a valid proof or not. This is nice and simple to explain that an enumeration is possible in principle, but as a practical procedure for anything it fails horribly. Even with the fastest computers, a proof of something like $2+2=4$ wouldn't emerge within a lifetime.
It's easy to think up some local improvements to this procedure and find a search strategy that would happen across a proof of $2+2=4$ (say, in Peano Arithmetic) in a more or less reasonable time. However, if we up the ante to for example $10+10=20$, that probably still wouldn't happen within any human lifetime -- unless we envisage some kind of guided search that aims to prove $10+10=20$ specifically rather than just searching through all proofs until one for $10+10=20$ pops up.
And by these measures, Goldbach's conjecture is not a "short" sentence -- stating it formally would need about 100 symbols, drawn from an alphabet of more than a handful of different symbols. So even if we just enumerate all sentences, without even requiring proof of them, we should expect to wait for not less than $5^{100}$ tries before it comes up. That's much, much longer than the number of nanoseconds in the lifetime of the universe.
