Can automated theorem provers solve mathematical olympiad problems in a reasonable time given enough compute?

LLMs are quite good at generating semantically correct language. I remember reading a paper about extending the planning capabilities of GPT-4 by using a Planning Domain Definition Language [0]. By that same logic could an LLM not translate the olympiad problem into a form suitable for a theorem prover?

[0] https://arxiv.org/pdf/2305.11014.pdf