Just so everyone knows, although openAI pretends that the model generated solution and wrote the paper by itself ""with very little human input"" as Buckmaster himself mentioned in his statement. In reality they have team of researchers guiding the system, along with, probably training on user data, probably Buckmaster in this case, in order to come up with the proof.