This must be one of the best applications for LLMs, as you can always automatically verify the results, or reject them otherwise, right?
replies(5):
But generating useless code, or proofs, just to discard them is hardly a consequence and externality free effort.