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.
>After the release of GPT Sol 5.6, I used a very long prompt, 10 pages long in my paper