This is a special post for quick takes by ESRogs. Only they can create top-level comments. Comments here also appear on the Quick Takes page and All Posts page.
If I've heard him right, it sounds like Dan Selsam (NeuroSAT, IMO Grand Challenge) thinks ML systems will be able to solve IMO geometry problems (though not other kinds of problems) by the next IMO.