Deepmind's recent model is trained with Lean. It scored a silver olympiad medal (and only one point away from gold).

> AlphaProof is a system that trains itself to prove mathematical statements in the formal language Lean. It couples a pre-trained language model with the AlphaZero reinforcement learning algorithm, which previously taught itself how to master the games of chess, shogi and Go

https://deepmind.google/discover/blog/ai-solves-imo-problems...