Recognizing and generalizing nontrivial mathematical patterns from the world, at the level you mean, seems (to me) to be AI-complete; on the other hand, in a domain with lots of variables and unreliable human intuition, Eurisko did pretty well at basically that.
Funny that you should mention Eurisko and not Automated Mathematician by the same guy, because the postulated agent sound pretty close to AM.
Suppose we made an algorithm capable of forming empirical conjectures for mathematics. How might such an algorithm discover the principle of mathematical proof?
I would like to see an article on the relevant philosophy and mathematical logic background for this problem. Since I currently lack the inclination to research and write up such an article, I instead made this post.