AlphaGo. Reinforcement learning on math with proof assistants was clearly going to be workable after that, even if not right away.