OpenAI opens 719 AI-generated math manuscripts for checking
OpenAI has released 719 manuscripts from an internal model, giving mathematicians a large public set of AI-generated results to verify, reuse, or challenge. The repository groups them into 372 result families and includes source files, PDFs, citation instructions, and Lean proofs, which let a computer check some of the mathematics. About 42% of the catalogue's top-line results currently have Lean formalizations; the model was posed roughly 4,000 problems and used about three hours of ChatGPT Pro thinking compute per result on average.