"A Mathematician" (Lenat and co.) did indeed attempt to approach creative theorem development from a radically different approach (syllogistic search-space expl

"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.glam.ac.uk/pages/staff/efurse/Abstracts/Why-did-AM-halt.html https://web.archive.org/web/20060528011654/http://www.comp.g...