OpenAI发布数百份数学手稿，附计算机可验证证明

OpenAI has published a collection of mathematical research generated by an unreleased internal AI model, giving researchers access to manuscripts and supporting materials for examination. Announced October 6, the release contains 722 manuscripts organized into 372 families of related results. Many have accompanying formal proofs written in Lean, a language and proof assistant that allows computers to check mathematical reasoning. The collection follows an evaluation involving approximately 4,000 problems. That figure describes the problems presented to the model—not 4,000 verified solutions. OpenAI also cautions that the results are at different stages of verification and that some unformalized arguments may contain errors. UNDERSTANDING THE NUMBERS The distinction between problems, manuscripts, and result families is essential to interpreting the announcement. …