OpenAI Math Corpus: Progress vs Verification Pipelines

What landed on GitHub

In early October 2026, OpenAI announced a broad release of AI-generated mathematical work: hundreds of manuscript folders, Lean artifacts, revision history, and transparency materials tied to an internal frontier model the public cannot run. The openai/math repository is the canonical home for that dump — Apache-licensed, GitHub-versioned, and explicitly positioned as a way to push human knowledge forward rather than wait on journal latency.

The announcement lit up Hacker News for good reason. A single org publishing at manuscript scale changes how the field argues about correctness, credit, and what "release" even means. My read is narrower and more engineering-shaped: progress velocity and verification velocity are different pipelines, and conflating them is how you ship a green README while most folders still lack a machine-checked main theorem.

Two percentages, one repository

OpenAI's README statistics describe 719 manuscripts grouped into 372 families, with roughly 4,000 problems posed during evaluation and an average of about three hours of ChatGPT Pro thinking compute per surfaced result. On formalization, the README language points to ~42% of top-line results formalized in Lean — a headline that sounds like "nearly half the corpus is machine-checked."

Independent data journalism from Daniel Reyes at Stanford Tech Review did something the headline does not: line up every manuscript folder in the catalogue against entries in lean/formalization.yaml. That match yields 162 manuscripts with a Lean formalization of the main result out of 722 — about 22.4% — with 560 folders still lacking a machine-checked main theorem in the map at analysis time.

Metric	Source	Count	Share
Top-line formalized (Lean)	OpenAI history update, Oct 7	300 / 719	~42%
Main result in formalization.yaml	Stanford Tech Review catalogue match	162 / 722	22.4%
Manuscripts without main-result Lean entry	Same independent count	560	—
Oct 3–6 burst cohort with 0% Lean in catalogue	Same	143 manuscripts	0%

Same repo. Two denominators (719 vs 722). Two definitions of "formalized." Almost 2× apart on what "verified" suggests to a reader skimming stats.

The README is also blunt in a way release notes usually are not:

"Some of the unformalized results could have issues."

That line belongs in every slide deck that treats "published to GitHub" as synonymous with "safe to cite."

Why the gap is a pipeline problem, not a math insult

The contrarian take here is not "AI can't do math." OpenAI clearly moved fast: families of results, companion papers, formal artifacts, and a revision log that already records three withdrawals, fourteen revisions, and six additional formalizations after the initial drop — including a sign error that cascaded through dependent K3 / Hodge-related manuscripts. That is real progress velocity.

Verification velocity lagged in public view. The late-October cohort Reyes analyzed — 143 manuscripts from the Oct 3–6 burst — showed 0% Lean coverage in the catalogue when the numbers were run, while an earlier Sep 23–27 burst (567 manuscripts, ~79% of the collection) still only reached 28.0% formalization within that slice (159 formalized). Release batches and formalization batches are not the same train.

Lean checks a formal statement in a proof assistant kernel. It does not, by itself, guarantee that the PDF prose matches the formal theorem, that the theorem is the result a human expert would state, or that the mathematics is culturally "understood" in the sense AGMAI's community recommendations describe for tier-two releases. Those are separate gates — and the ecosystem debate (Fields Medalist misalignment declaration, Terence Tao's strip-miner warnings, access threads on HN) is largely about which gates society wants, not whether kernels compile.

For builders, the analogy is familiar: a monorepo dump where README badges and actual CI coverage diverge. Green at the top; most packages never ran the job you care about.

Progress pipeline vs verification pipeline

Think in two lanes:

Lane	Question it answers	What "done" looks like	OpenAI math example
Progress	Did we generate candidate knowledge fast enough to matter?	Manuscript in preprints/, family aggregated, compute logged	719–722 folders, ~3h Pro compute per result (claimed average)
Verification	Did we machine-check the claim we expect others to rely on?	Main result entry in formalization.yaml, Comparator / third-party rebuild	162/722 catalogue match (~22.4%)

Marketing and README stats naturally live in the progress lane. Due diligence lives in the verification lane. When HN celebrates the announcement thread, both lanes get applause — but only one lane protects downstream consumers who treat a star count as peer review.

The Advisory Group on Mathematics and AI sits between camps: OpenAI consulted an independent group at IAS, while AGMAI's public letter asks labs not to strip-mine open problems on inaccessible models — yet still demands disclosure, formalization where feasible, and community-funded understanding when releases outpace human exposition. That is an institutional attempt to name both pipelines even when one runs faster.

A bar your team can actually operationalize

If you own agent outputs — code, proofs, compliance packets, incident narratives — the useful question from the LinkedIn thread still stands: what bar do you use for "released" vs "machine-checked"?

Here is a minimal schema teams can steal without pretending to be a math journal:

type ReleaseTier = "draft" | "released" | "machine_checked" | "human_signed";

interface ArtifactManifest {
  id: string;
  tier: ReleaseTier;
  /** Human-facing claim (PDF, markdown, ticket) */
  proseRef: string;
  /** Optional: Lean, Coq, test suite, policy engine */
  checkerRef?: string;
  /** Must align for tier >= machine_checked */
  statementFingerprint?: string;
  knownGaps: string[];
}

function publicHeadline(m: ArtifactManifest): string {
  if (m.tier === "machine_checked" && m.checkerRef) {
    return `Checked: ${m.id}`;
  }
  if (m.tier === "released") {
    return `Released (unverified main claim): ${m.id}`;
  }
  return `Draft: ${m.id}`;
}

Never let a progress-lane metric stand in for a verification-lane metric in customer-facing copy.

Checklist I would enforce before calling something "verified" in an external channel:

• Catalogue entry exists for the specific artifact ID consumers will cite
• Checker artifact linked and reproducible on neutral infrastructure (compare independent Navier–Stokes Lean rebuilds)
• Statement fingerprint or hash ties prose headline to checked theorem / test contract
• Withdrawal path documented when upstream errors cascade (OpenAI's Oct 7 history is the template)
• README / stats distinguish top-line counts from folder-level coverage

Until those boxes are ticked, you are shipping progress — which can be valuable — not verification.

What changed after Oct 7 (and what did not)

The history.md entry for October 7, 2026 is worth reading as an ops log: withdrawals, repairs, and a restated 300 / 719 ≈ 42% top-line formalization figure after six more formalizations landed. That is verification catching up inside the progress lane's accounting — but it does not erase the independent 22.4% folder match unless every manuscript folder gains a yaml entry humans can audit without re-deriving OpenAI's definition of "top-line."

Secondary coverage (The Decoder's release write-up) emphasizes families, single-agent vs swarm compute for prior splash results like Navier–Stokes, and the tension between GitHub-as-journal speed and traditional review. None of that resolves the counting ambiguity; it amplifies why transparent definitions matter more as volume scales.

Nutshell

OpenAI's math release is a genuine progress pipeline: hundreds of manuscripts, Lean infrastructure, and public revision history at a speed journals cannot match. The verification pipeline — at least measured by independent catalogue matching — covers roughly 22.4% of manuscript folders with a machine-checked main result, not the ~42% top-line figure in README/history stats. Treating those numbers as interchangeable is the same mistake as trusting README badges over CI coverage. The future is not faster theorem dumps alone; it is agreeing which pipeline you are shipping, and labeling outputs so nobody confuses release velocity with verification velocity.