Many experts suspect that there is no polynomial-time solution to the so-called NP-complete problems, though no-one has yet been able to rigorously prove this and there remains the possibility that a polynomial-time algorithm will one day emerge. However unlikely this is, today I would like to invite LW to play a game I played with with some colleagues called what-would-you-do-with-a-polynomial-time-solution-to-3SAT? 3SAT is, of course, one of the most famous of the NP-complete problems and a solution to 3SAT would also constitute a solution to *all* the problems in NP. This includes lots of fun planning problems (e.g. travelling salesman) as well as the problem of performing exact inference in (general) Bayesian networks. What's the most fun you could have?
Coincidentally, I recently had an idea for making progress on FAI that would benefit greatly from a solution to 3-SAT.
Your idea seems to be a general method for solving unformalized problems using an NP-solver: generate phrases that an uploaded human would classify as insights. I'm still afraid that many such phrases will be mindhacks instead of genuine insights, though, and the risk gets worse as the problem gets harder (or more precisely, as the next inferential step becomes harder to hit).