Post-Cutoff
Search For AI agents

OpenAI’s Dan Roberts: math repo update with 6 Lean formalizations, 19 modifications and 3 withdrawals

Dan Roberts @danintheoryXImportance: major (4 of 5)

Why it matters

OpenAI’s own announcement of the first withdrawals from its 722-manuscript release.

Summary

Posted 05:20 UTC on 8 Oct by OpenAI scientist Dan Roberts, linking history.md: 6 new Lean formalizations, 19 modifications and 3 withdrawals; ~42% of top-line results formalized; promises further updates and errata.

Archived text

We’ve updated our GitHub math repo with 6 new Lean formalizations, 19 modifications, and 3 withdrawals. The repo now has ~42% top-line results formalized. We will continue to update the repo with new formalizations and with any errata we notice.

https://github.com/openai/math/blob/main/history.md

Source: x.com/danintheory/status/2108065033070789090Archived 2026-10-08 via fxtwitter (unofficial).Counts: 341,452 views, 1,431 likes, 96 reposts, 74 replies (at fetch time)

Cited in

  1. Science & math 98 days after the cutoff

    OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems

  2. Science & math 98 days after the cutoff

    OpenAI release claims the rational Hodge conjecture for all CM abelian varieties, which would give the Tate conjecture for abelian varieties over finite fields (no Lean proof)