"A Mathematician" (Lenat and co.) did indeed attempt to approach creative theorem development from a radically different approach (syllogistic search-space exploration, not dissimilar to forward-chaining in Prolog), although they ran into problems distinguishing "interesting" results from merely true results: https://web.archive.org/web/20060528011654/http://www.comp.g...