But when you talk about "getting a lot more done," I want to ask, get a lot more done to what end? Despite what mathematicians sometimes write in their grant applications, resolving most of the big open problems in the field probably won't lead to new technologies or anything. To use the Riemann Hypothesis example again, most number theorists already think it's probably true, and there are a lot of papers being published already which prove things like "if the Generalized Riemann Hypothesis is true, then [my new result]".
No one is really waiting around just for the literal, one-bit answer to the question of whether RH is true; if we got that information and nothing else, I'm sure number theorists would be happy to know, but not a whole lot about the work being done in the field would change. It's not just being "satisfying to the curious"; virtually the entire reason we want a proof is to use the new ideas it would presumably contain to do more mathematics. This is exactly what's happened with the proof of the Poincare Conjecture, the only one of the Millennium Problems that's been resolved so far.
This is what I was lamenting in my comment earlier: the thing you're describing, where we set proof-finding models to work and they spit out verifiable but totally opaque proofs of big open problems in math, very well might happen someday, but it wouldn't actually be all that useful for anything, and it would also mean the end of the only thing about the whole enterprise that the people working in it actually care about.