Wow, this could eventually enable some pretty amazing stuff. I'm just a hobbyist, but this makes me think about how machine search through the space of possible theorems butts up against the halting problem and/or Godel's theorems (though one could argue that human searching of the space is subject to the same limitations if our minds on some level represent formal systems as Hofstadter thinks).

And I wonder about whether certain mathematical truths will be inherently difficult to locate because they are far away from the space of other existing problems, and thus subject to problems of a search algorithm getting stuck in a local maximum.

In any case, an accelerated search through this space sounds really promising and exciting!