As of: 2026-10-08 23:45 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz.
Canonical page: https://postcutoff.com/p/2026-10-08-danintheory-openai-math-repo-withdrawals/

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

Dan Roberts (@danintheory), X, 2026-10-08. Importance: major (4 of 5).
Source: https://x.com/danintheory/status/2108065033070789090

## 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

Archived 2026-10-08 via fxtwitter (unofficial).
Counts: 341,452 views, 1,431 likes, 96 reposts, 74 replies (at fetch time)

## Cited in

- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/)
- 2026-10-06: [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)](https://postcutoff.com/e/2026-10-06-hodge-conjecture-cm-abelian-varieties-openai/)