Discussion on Reddit: https://old.reddit.com/r/math/comments/1uxj3cy/after_openais...

Of note: the author had AI help synthesizing the actual 10-page prompt that resulted in the proof! A powerful tool when you know what you're doing.

Did you have first an AI help designing the prompt?

> yes, I did! I basically had 5.6 Sol synthesize existing closely related work and their approaches, the past ideas I had, with OpenAI's prompt that had a lot of the presumably important mechanisms for how exactly the agent should act. Especially from the "results that do not count" section onwards is a lot of input from Sol.

For anyone dooming I’ll just leave you with this bit. It still takes quite a bit of knowledge to get it going:

After the release of GPT Sol 5.6, I used a very long prompt, 10 pages long in my paper