Can automated theorem provers solve mathematical olympiad problems in a reasonable time given enough compute? LLMs are quite good at generating semantically co

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 https://arxiv.org/pdf/2305.11014.pdf