> exceptional guesser This IMO describes how mathematics itself moves forward... A matematician is an extremely well-trained 'guesser' who is also able to sink

> exceptional guesser This IMO describes how mathematics itself moves forward... A matematician is an extremely well-trained 'guesser' who is also able to sink a lot of time into formal verification. The process is essentially: a) Find an interesting conjecture that you've got a strong guess to be true. b) Check for obvious (or less obvious) counterexamples, or conflicting theorems. c) Prove the thing is true. A large part of the art of being a working mathematician is in part (a): you need to make a really good guess. An ideal conjecture is correct AND proveable AND leads to other interesting results, or says interesting things about bigger problems. So what happens when we apply really good versions of current AI to this area? Picking out an 'interesting' conjecture is still Strong-AI-Complete: it requires lots of domain knowledge, and an understanding of what this particular conjecture would 'unlock.' But we could perhaps come up with good 'guessers' which quickly tell us whether a given idea might work out, perhaps saving a bunch of effort. Perhaps we could even get to the point of generating a proposed proof which can be fed to an automated proof checking system, allowing for inspection and modification by the human in the loop.