Comment by alangibson

This is not the simplest explanation.

The most direct line from problem to proof is OpenAI building off of conversations the mathematicians had with their AI.