From: peter.luschny@gmail.com   
      
   Richard Fateman asked this recently.   
      
   They are probably closer than you think, if they are not already here.   
      
   Kevin Buzzard today said: "You know how these AI people say that they're going   
   to get 'Lean' to solve an IMO problem automatically? And we math people know   
   this will never happen because IMO problems are hard."   
      
   According to this new blog post of the OpenAI people they solved not one but   
   two:   
      
   "Solving (Some) Formal Math Olympiad Problems"   
   https://openai.com/blog/formal-math/   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)