It's true that it would need to be insanely powerful. Even clever humans haven't managed to prove that one-way hash functions exist (though we know a function that is one-way if and only if they exist...).

Note theorem proving is isomorphic to programming. Even if it wasn't quite so equivalent, you could just ask for a constructive proof of a program satisfying whatever and the proof would contain the program.