Comment by curling_grad

Actually, OpenAI did a research[0] on solving some hard math problems by integrating language model and Lean theorem prover some time ago.

[0]: https://openai.com/research/formal-math