So they could also dump a 100 quadrillion line proof in Bourbaki notation and call it a day?

The proof was released in the spirit of being first at all costs without any attempt to clean it up. I doubt that OpenAI mathematicians could give a coherent talk about it, certainly not using a blackboard.