> I heard it was human mathematicians using a sophisticated machine as a tool.

where did you "hear" this? OpenAI said they only prompted it and it solved the problem in one shot without any help