Most open problems, when formalized, naturally involve quantification over infinite sets, thereby obviating the possibility, even in principle, of "just putting it on a computer."

Some questions (e.g. the existence of a projective plane of order 12) naturally resolve after a finite computation but not feasibly.

I'd like examples of reasonably important open problems that have now been *reduced*, via nontrivial arguments, to finite but infeasible computations. 

I'm sure that additive number theory gives examples (certain questions along the lines of Goldbach conjecture and Waring's problem, but I don't have the details handy).  I'd love especially to see examples that don't seem to originate in discrete mathematics.