OpenAI releases 722 math manuscripts produced by an internal AI model

OpenAI says an unreleased internal model was posed about 4,000 problems during the evaluation behind its collection of 722 mathematical manuscripts, organized into 372 families. The repository includes Lean formalizations for many proofs and 10 abridged summaries of the model’s reasoning. OpenAI warns that some unformalized results could have issues and says it will add more formalizations as it obtains them.