Hooray for proof search techniques. How much data would the Godel-numbering process generate, though? I'm assuming such a search would use this, unless I'm mistaken about my mathematical logic.