We don't.

But I imagine they took some lemmas from modern research which hasn't been publicized as much as the erdos problems for instance. Something very niche that only the mathematician who proposed it likely works on.

In any event, seems like openAI took on the challenge: https://cdn.openai.com/pdf/a430f16e-08c6-49c7-9ed0-ce5368b71d3c/1stproof_oai.pdf