Actually, OpenAI did a research[0] on solving some hard math problems by integrating language model and Lean theorem prover some time ago.
PS: also I thought GPT4 already achieved 90% in some university math grades? Oh I remember that was multiple-choice