OpenAI has trained a model to solve Math Olympiad-type problems[1], with some initial success, but currently the model isn't good at coming up with proofs involving more than a couple arguments chained together. Still some very impressive work.

[1] https://analyticsindiamag.com/openais-neural-theorem-prover-...