[ntoronto]

"I'm sure there's way more complexity I'm overlooking, but that's how one might get started."

That's how I'd start. There's probably a way to make the search a lot smarter. Here's the part you're overlooking, though:

"... there are only so [many] formulas made up of a fixed number of terms and operators..."

"So many" = "countably infinite." Paring it down to finitely many would require understanding tantamount to having solved the problem in the first place.

[Edit: I can words.]