OpenAI dumps 722 math manuscripts from an unreleased model into a public GitHub repo, many Lean-checked

Released Oct 6 in openai/math, the papers form 372 result families drawn from about 4,000 problems, averaging roughly three hours of ChatGPT Pro thinking each, with Lean formalizations for many (not all) proofs and 10 abridged reasoning summaries. The IAS advisory group asked for the model, prompts, and per-result compute to be public, but OpenAI is sharing only averages and no prompts, and the model itself stays internal for now.