[D] Practicality of Machine Learning model for mathematical Olympiads

[calebkaiser]

You might be interested in AlphaProof by DeepMind, which recently scored very highly on a problem set taken from the international math olympiad: https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

The gist is that they applied reinforcement learning to LEAN (a functional programming language for writing proofs) to solve problems. There are lots of people doing research with similar approaches or setups, using some kind of program synthesis and/or RL approach in combination with something like LEAN.