OpenAI published a broad set of new mathematical results on October 6, including formalizations in Lean and summaries of work on open questions. The important feature is not a claim that mathematics has been automated. It is the emerging division of labor: models explore candidate paths cheaply; formal systems check local logical steps; human mathematicians judge significance, novelty and hidden assumptions. Open problems are also an unusually clean test bed because a result can fail decisively. The harder sciences will need the same verification culture plus the messier discipline of instruments, samples and physical replication. OpenAI research release