OpenAI posts 722 math manuscripts from an unreleased model on GitHub, but their verification is uneven

• Model: an unnamed, unreleased internal frontier model. There is no public access, no API and no model card (GitHub).
• Procedure: OpenAI says almost every result came from a single prompt given to a single agent, under a fixed procedure (ExplainX).
• What is public: the preprint PDFs with source files, Lean files, abbreviated reasoning summaries for 10 families, and BibTeX entries (GitHub).

• Verification is uneven. Not every manuscript comes with Lean. Unite.AI counts 162 papers whose main result is formalized in Lean. ExplainX counts Lean links on 235 of the 372 families, but notes that the Lean coverage can be narrower than what the abstract claims. The two counts measure different units (papers vs. families), and neither is official.
• What Lean does and doesn't show. A Lean proof certifies that the logic is valid. It does not show that the formal statement matches the open problem as posed, and it says nothing about novelty or significance.
• Not every result followed the standard pipeline. The repository lists the Riemann zeta zero-free region and the Hodge result as exceptions (GitHub).
• Reproducibility: nobody outside OpenAI can rerun the model. The roughly 4,000 problems attempted give a denominator for the results, but the selection criteria are not documented.

• Batch size, compute and attempts (722 manuscripts, 372 families, about 3 hours per result, about 4,000 problems): vendor-reported (GitHub).
• "Hundreds" of unresolved points solved: this description comes from AGMAI, not from OpenAI (The Verge). No independent audit of correctness has been reported.
• Specific claimed results (quasi-RH, Unique Games, the free group factor problem): vendor-reported, with no completed independent verification (IBTimes Australia).
• "90 of the top 500" open problems: commentary in Latent Space with no source document behind it.
• Quality of earlier work: Timothy Gowers has said he would recommend at least one earlier proof to a top journal (Startup Fortune). That is a single expert view, not an assessment of this batch.

This batch follows Astra's 10 results (August) and the Navier–Stokes claim (September). In that earlier work, about 10,000 agents ran for 88 hours on a single problem. The new batch reports roughly 3 hours per result (Express Tribune; Latent Space). Anthropic and other rival labs are publishing math results too (The Verge). AGMAI asked labs to release through academic channels and to disclose the model, prompts and compute.

• OpenAI's own caveat: unformalized results "could have issues" (GitHub).
• Disregarded guidance: AGMAI recommended posting in a repository that no AI lab controls. OpenAI used its own GitHub account instead (Verge).
• Fields Medalists' letter: 25 Fields Medalists signed "A Severe Misalignment of AI in Mathematics." It argues that solving problems is only a proxy for understanding. Gowers warned that the literature could grow beyond what any human community can absorb (The Decoder).
• Credit and provenance: OpenAI denies that it accessed Buckmaster's private work directly. It has said it cannot rule out benefiting from de-identified product data (Express Tribune).
• Expected attrition: Will Depue expects some results not to survive scrutiny (Latent Space).

• Pace and cost: if most results hold up, frontier models are producing research-grade math at about three Pro-hours per result. That is far cheaper than the agent swarms used weeks earlier.
• Lean checking is a requirement now: for AI-generated proofs, Lean checking plus human review of the formal statements is becoming the minimum standard.
• No access: practitioners can't use the capability itself. The only usable artifacts are the papers and the Lean code.
• Reputational and legal exposure: labs face it over attribution and training-data provenance. Product terms that cover research done with user data deserve scrutiny.
• Citation risk: citing these results before they are independently checked is risky. Track the repository's versioned corrections.