数学ビジュアライズ

AI数学単発記事

OpenAIの数学論文の修正と取り下げの記録OpenAI's math manuscripts: a record of corrections and withdrawals

OpenAIが公開した数学論文のリポジトリ openai/math で、どの論文が取り下げられ、どの論文が直されたかをまとめます。符号の誤りで取り下げられた3本の理由、証明を直した14本の内容、Leanでの形式化の進み具合を、更新のたびに追記します。

A running record of what has been withdrawn and what has been corrected in openai/math, the repository of mathematical manuscripts written by an OpenAI model: the sign error behind three withdrawals, the proof repairs in fourteen manuscripts, and the progress of the Lean formalizations. Updated as the repository changes.

目次Contents
  1. openai/math とは
  2. 今の状態
  3. 2026年10月7日の更新
  4. 版の見つけ方と読むときの注意
  5. この記事の更新記録
  6. 参考文献
  1. What openai/math is
  2. Where things stand
  3. The update of October 7, 2026
  4. Finding versions, and caveats
  5. Changes to this page
  6. References
この記事の要点
何の記録か
OpenAIのモデルが書いた数学論文を集めたリポジトリ openai/math のうち、取り下げられた論文と直された論文の記録です。リポジトリの更新があれば、この記事に書き足します。
最新の更新
2026年10月7日付の更新で、3本が取り下げられ、14本の証明や主張が直されました。ほかに13本が、直された論文を引用し直しています。
取り下げの理由
1本の論文の証明で符号を取り違えていて、打ち消し合うはずの数が0になりませんでした。残りの2本は、同じ構成を使っていたため一緒に取り下げられました。
今の規模
論文は719本(公開時は722本)で、372のファミリーに分かれています。主な結果のうちLeanで形式化されたものは300本、約42%です。

最終確認:2026年10月9日(history.md の2026年10月7日の更新まで)

openai/math とは

2026年10月6日、OpenAIは、未公開の社内モデルが書いた数学の論文をGitHubのリポジトリ openai/math で公開しました[1]。公開時は722本で、関連する論文をまとめた372の「ファミリー」に分かれていました。そのうちの1本は、平面の彩色数の記事で読んでいます。

リポジトリの説明によると、収録された結果は検証の段階がまちまちで、Leanでの形式化がないものもあります。形式化されていない結果には問題があるかもしれず、見つかればすぐ直すよう努めるとしています。

直した論文は新しい版として置き、前の版も読めるように残す方針です。変更は history.md に記録されます[2]。この記事は、その記録を日本語で読めるようにまとめ、論文ごとの変更点を書き添えたものです。

今の状態

公開時(10月6日)今(10月7日の更新のあと)
論文の数722本719本
ファミリーの数372372
取り下げ0本3本
証明や主張の修正—14本
Leanでの形式化「多くの論文で形式化済み」とだけ記載主な結果のうち300本(719本中、約42%)
図1 主な結果がLeanで形式化された論文の割合。719本のうち300本(約42%)です。

2026年10月7日の更新

最初の更新です[2]。内容は、取り下げ3本、証明や主張の修正14本、引用の更新13本、形式化の追加です。GitHubに反映されたのは日本時間の10月8日の午後でした。

取り下げ(3本)

取り下げられたのは次の3本です。1本目の証明に符号の誤りがあり、2本目と3本目はその構成を作り変えて使っていました。

誤りのある論文Algebraicity of Weil classes on split abelian eightfolds
同じ構成を使うAlgebraicity of Kuga–Satake Correspondences for K3 Surfaces
同じ構成を使うThe rational Hodge conjecture for products of K3 surfaces
図2 取り下げられた3本の関係。誤りのある論文の構成を、ほかの2本が作り変えて使っていました。
論文取り下げで証明がなくなった主張資料
Algebraicity of Weil classes on split abelian eightfolds分裂型でワイル型の8次元アーベル多様体の上で、有理ワイル類はすべて代数的である。取り下げのお知らせ
取り下げ前のPDF
Algebraicity of Kuga–Satake Correspondences for K3 Surfaces非特異な複素射影K3曲面のすべてについて、久賀=佐武対応は代数的である。取り下げのお知らせ
取り下げ前のPDF
The rational Hodge conjecture for products of K3 surfaces複素射影K3曲面の有限個の積では、有理ホッジ予想が成り立つ(有理ホッジ類はすべて代数的である)。取り下げのお知らせ
取り下げ前のPDF

3本のお知らせには、どれも同じ断り書きがあります。取り下げたのは証明であって、主張が偽だと言っているのではありません[3]。主張そのものは、証明がない状態に戻りました。

この3本は、ファミリー032に入っていました。ファミリーの題は「すべての射影K3曲面についてのホッジ予想と久賀=佐武の結果」でしたが、更新のあとは「CMアーベル多様体の有理ホッジ予想」になっています。同じファミリーのCMアーベル多様体の論文は取り下げられておらず、引用を更新しただけです。

取り下げの理由:符号の誤り

1本目の取り下げのお知らせには、誤りの中身が数式で書かれています[3]。ここではその筋道をたどります。

証明の途中で、自己交差を許した写像(はめ込み)を扱います。像の2か所が重なる点を二重点と呼び、二重点ごとに向きから +1+1 か −1-1 の符号を決めます。符号を足した数が、符号付きの二重点の数です。はめ込み f1f_1 では、この数が負でした。

I(f1)=−m(m>0)I(f_1)=-m \qquad (m>0)I(f1)=−m(m>0)\begin{gathered}I(f_1)=-m\\(m>0)\end{gathered}I(f1)=−m(m>0)\begin{aligned}I(f_1) &= -m\\[4pt]&(m>0)\end{aligned}

証明では、ある操作(逆向きの安定化の跡、reverse stabilization trace)を mm 回入れて、この数を0にしようとします。論文はこの操作の符号を +1+1 と数えたので、次の計算で合計が0になるはずでした。

−m+(+1)+⋯+(+1)⏟m=0-m+\underbrace{(+1)+\dots+(+1)}_{m}=0−m+(+1)+⋯+(+1)⏟m=0\begin{aligned}-m+\underbrace{(+1)+\dots+(+1)}_{m} &= 0\end{aligned}

しかし、標準的な尖点の2本の枝は、写す前の側(定義域)での向きが互いに逆です。これを数え入れると、1回ごとの符号は −1-1 になり、合計は0になりません。

Inew=I(f1)−m=−2m≠0I_{\mathrm{new}}=I(f_1)-m=-2m\neq0Inew=I(f1)−m=−2m≠0\begin{aligned}I_{\mathrm{new}} &= I(f_1)-m\\&= -2m\\&\neq 0\end{aligned}

証明はこのあと、Eliashberg–Murphyの打ち消しの定理を使います。この定理は、符号付きの二重点の数が0であることを仮定しています。仮定が満たされないので、その先の向き付きの手術と埋め込まれたブレーンの構成は支えを失い、代数性の主定理も示されていないことになりました。

2本目と3本目のお知らせによると、どちらもこの構成を作り変えて使っていました。そのため、同じ符号の問題で二重点の打ち消しができず、主定理の証明に穴が残りました。

証明や主張の修正(14本)

次の14本は取り下げられず、新しい版が出ました。証明の穴を埋めたもの、主張を直したもの、仮定と依存関係をはっきり書いたものがあり、ほかに古い引用を1件直しています。表の内容は、各版の README にある版の注記(Version note)を訳したものです。

history.md が主張の訂正として挙げているのは「Taming implies compatibility on four-manifolds」です。錐が等しいという主張を hJ−=b2+−1h_J^-=b_2^+-1 の場合に限り、等号が成り立たない4次元トーラスの例を加えています。

リプシッツ高さ関数とアシュキン=テラー模型(4本)

論文内容版
Uniform real Lipschitz surfaces on the triangular lattice境界への接続、着地点の比較、多重スケールでの分離の議論を直した(条件付きのウォークとつなぎ合わせの段階を含む)。曲線全体の収束のために、終端側の同定と調和測度の非回帰の議論を補った。9月25日 → 10月6日
新しい版 / 前の版
Gaussian free-field limits of weighted integer Lipschitz heights離散の議論で使う回路の評価に、円環での証明を補った。9月25日 → 10月6日
新しい版 / 前の版
The Gaussian free field limit of integer Lipschitz heights with two-arc boundary data条件付きの切断とループの評価を、姉妹論文の重み付き円環回路の定理(x=1x=1 の場合)から導くようにした。9月25日 → 10月6日
新しい版 / 前の版
The joint scaling limit of critical Ashkin–Teller currents透過と境界の帯の議論を直し、エクスカーションの収束を、同じ極限場に結びつく符号付きループスープと GMC の議論に置き換えた。姉妹論文の引用も更新した。9月25日 → 10月6日
新しい版 / 前の版

ケーラー多様体の極小モデル理論とアバンダンス(6本)

論文内容版
Finite ordinary minimal model programs on compact Kähler fourfoldscarrier-positivity と乗数イデアルの議論を加え、通常の負の端射線のプログラムについて、収縮の帰納法を改めた。10月5日 → 10月6日
新しい版 / 前の版
Termination of generalized-canonical flips on compact Kähler fourfolds姉妹論文から使うのは、独立した負性、余次元2での滑らかさ、サイクルの比較の結果だけだと明記した。10月5日 → 10月6日
新しい版 / 前の版
Termination of generalized log canonical flips on compact Kähler fourfolds証明が使う相対 MMP と双有理比較の入力を明記し、改訂した姉妹論文への引用を更新した。10月5日 → 10月7日
新しい版 / 前の版
Conditional good minimal models for compact Kähler fourfolds独立した通常 MMP の入力を明記し、残る仮定(飯高の劣加法性と有効アバンダンス)をはっきり書いた。10月5日 → 10月6日
新しい版 / 前の版
Log abundance for compact Kähler spaces under logarithmic Iitaka subadditivity帰納法のための底空間の表示と乗数イデアルの議論を補った(随伴類の引き戻しと、収縮で降ろす段階を含む)。10月4日 → 10月6日
新しい版 / 前の版
Numerical semiampleness of nef adjoint classes on compact Kähler manifolds因子分解の議論で使う飯高・モデル・収縮の入力を明記した。10月4日 → 10月6日
新しい版 / 前の版

テイミングとハイパーシンプレクティック変形(2本)

論文内容版
Taming implies compatibility on four-manifolds錐が等しいという主張を直した。両立する錐を交叉の正値性で特徴づけ、錐の和の等式を hJ−=b2+−1h_J^-=b_2^+-1 の場合に限り、包含が真になる4次元トーラスの例を加えた。9月23日 → 10月6日
新しい版 / 前の版
Deforming hypersymplectic four-manifolds to hyperkähler triples変形の議論で使うコホモロジー類の判定条件を明確にし、不要だった錐の比較の引用を外した。姉妹論文の引用も更新した。9月23日 → 10月7日
新しい版 / 前の版

そのほか(2本)

論文内容版
Incompressible Box Transport and Finite Computationトーラスへの射影と共通時計の減衰について、射影した力と圧力の上からの評価を含む、具体的な評価を補った。9月27日 → 10月6日
新しい版 / 前の版
Exact Birch–Swinnerton-Dyer Formula from Low Selmer Corank序論にあった、削除された補助論文への古い引用を外した。改訂版への引用も更新した。10月3日 → 10月7日
新しい版 / 前の版

引用の更新(13本)

次の13本は、内容ではなく引用だけが変わりました。上の修正を受けて、改訂された姉妹論文の新しい版を参照するように直し、版の日付が新しくなっています。

  • A pointwise 2-converse for elliptic curves with rational two-torsion9月24日 → 10月7日 新しい版 / 前の版
  • Abelian covers, Gale correspondences, and the Hodge conjecture for powers9月30日 → 10月6日 新しい版 / 前の版
  • Fontaine–Mazur modularity at the prime 29月23日 → 10月6日 新しい版 / 前の版
  • Goldfeld's analytic density conjecture and the 2-converse for elliptic curves9月23日 → 10月7日 新しい版 / 前の版
  • Hilbert's tenth problem over the rational numbers9月24日 → 10月6日 新しい版 / 前の版
  • Milne's rationality conjecture for abelian varieties9月23日 → 10月7日 新しい版 / 前の版
  • The mean analytic rank of quadratic twists of elliptic curves9月23日 → 10月6日 新しい版 / 前の版
  • The p-adic section conjecture9月24日 → 10月6日 新しい版 / 前の版
  • The rational Hodge conjecture for CM abelian varieties9月30日 → 10月6日 新しい版 / 前の版
  • The Selmer converse for elliptic curves at every prime9月24日 → 10月7日 新しい版 / 前の版
  • The two-primary Birch–Swinnerton-Dyer formula in Selmer corank at most one9月24日 → 10月6日 新しい版 / 前の版
  • Unrestricted pro-modularity at the prime two10月4日 → 10月6日 新しい版 / 前の版
  • Weil classes and Hodge classes on abelian powers9月30日 → 10月6日 新しい版 / 前の版

形式化の追加

Leanでの形式化が6件と、補助的な結果を扱うほかの追加が5件ありました。これで、主な結果が形式化された論文は719本のうち300本(約42%)になりました[2]。公開時のREADMEには割合がなく、「多くの論文で形式化済みだが、すべてではない」とだけ書かれていました。

版の見つけ方と読むときの注意

  • 直された論文:新しい版は、日付を変えた別のディレクトリ(例:…-October-6-2026)に置かれます。その README の版の注記から、前の版へリンクがあります。
  • 取り下げられた論文:もとの場所に取り下げのお知らせが置かれ、取り下げ前のPDFは公開時のコミット adc7f12 で読めます。一覧(CONTENTS.md)からは消えています。
  • 日付のずれ:取り下げのお知らせは10月6日付、history.md の見出しは10月7日、GitHubへの反映は日本時間の10月8日です。この記事では history.md の日付で呼んでいます。
  • 確かさ:論文はどれも査読前のプレプリントです。形式化されていない結果には問題が残っているかもしれない、とリポジトリ自身が書いています[1]。

この記事の更新記録

  • 2026年10月9日 公開。history.md の2026年10月7日の更新までを反映しました。

参考文献

  1. OpenAI, openai/math: mathematical manuscripts and supporting proof artifacts, GitHub, 2026.
  2. OpenAI, openai/math: History, GitHub, 2026.
  3. OpenAI, Withdrawal notice: Algebraicity of Weil classes on split abelian eightfolds, openai/math, October 6, 2026.
In short
What this is
A record of the manuscripts withdrawn from and corrected in openai/math, the repository of mathematical manuscripts written by an OpenAI model. This page is updated whenever the repository changes.
Latest update
In the update dated October 7, 2026, three manuscripts were withdrawn and fourteen had their proofs or statements corrected. Thirteen more were updated to cite the corrected editions.
Why the withdrawals
A proof in one manuscript got a sign wrong, so a count that was supposed to cancel to zero did not. The other two used the same construction and were withdrawn with it.
Current size
719 manuscripts (722 at release) in 372 families. The top-line results of 300 of them, about 42%, are formalized in Lean.

Last checked: October 9, 2026 (history.md up to the update of October 7, 2026)

What openai/math is

On October 6, 2026, OpenAI released mathematical manuscripts written by an unreleased internal model, in the GitHub repository openai/math[1]. At release there were 722 manuscripts, grouped into 372 “families” of related papers. One of them is the subject of our article on the chromatic number of the plane (in Japanese).

The repository says that its results are at different stages of verification and that not all of them have Lean formalizations. Some unformalized results could have issues, and OpenAI says it will endeavor to fix them quickly.

Corrections are released as new versions, and earlier versions stay available. The changes are recorded in history.md[2]. This page follows that record and adds, for each manuscript, what changed.

Where things stand

At release (Oct 6)Now (after the Oct 7 update)
Manuscripts722719
Families372372
Withdrawn03
Proofs or statements corrected—14
Lean formalization“Many, but not all, of the manuscripts have been formalized”Top-line results of 300 of 719 manuscripts (about 42%)
Figure 1 Share of manuscripts whose top-line results are formalized in Lean: 300 of 719, about 42%.

The update of October 7, 2026

This is the first update[2]. It withdraws three manuscripts, corrects proofs or statements in fourteen, updates citations in thirteen, and adds formalizations. It reached GitHub on October 8 (05:03 UTC).

Withdrawals (3)

The three withdrawn manuscripts are below. The first has a sign error in its proof; the second and third used adaptations of its construction.

Contains the errorAlgebraicity of Weil classes on split abelian eightfolds
Uses the constructionAlgebraicity of Kuga–Satake Correspondences for K3 Surfaces
Uses the constructionThe rational Hodge conjecture for products of K3 surfaces
Figure 2 How the three withdrawn manuscripts depend on each other: the other two adapted the construction of the one with the error.
ManuscriptClaim left without a proofDocuments
Algebraicity of Weil classes on split abelian eightfoldsEvery rational Weil class on a split abelian eightfold of Weil type is algebraic.Withdrawal notice
Pre-withdrawal PDF
Algebraicity of Kuga–Satake Correspondences for K3 SurfacesThe Kuga–Satake correspondence is algebraic for every smooth projective complex K3 surface.Withdrawal notice
Pre-withdrawal PDF
The rational Hodge conjecture for products of K3 surfacesThe rational Hodge conjecture holds for every finite product of projective complex K3 surfaces: every rational Hodge class is algebraic.Withdrawal notice
Pre-withdrawal PDF

All three notices carry the same caveat: the withdrawal concerns the proof and does not assert that the statement is false[3]. The statements are simply without a proof again.

The three belonged to family 032. Its title was “Hodge and Kuga–Satake results for all projective K3 surfaces”; after the update it is “The rational Hodge conjecture for CM abelian varieties”. The CM abelian variety manuscript in that family was not withdrawn; only its citations were updated.

Why: a sign error

The notice for the first manuscript spells out the error with formulas[3]. Here is the line of the argument.

The proof works with an immersion, a map allowed to cross itself. A point where two parts of the image meet is a double point, and each double point gets a sign, +1+1 or −1-1, from the orientations. The sum of these signs is the signed double-point count. For the immersion f1f_1 this count is negative:

I(f1)=−m(m>0)I(f_1)=-m \qquad (m>0)I(f1)=−m(m>0)\begin{gathered}I(f_1)=-m\\(m>0)\end{gathered}I(f1)=−m(m>0)\begin{aligned}I(f_1) &= -m\\[4pt]&(m>0)\end{aligned}

The proof then inserts mm reverse stabilization traces to bring the count to zero. It gives each trace the sign +1+1, so the count would become

−m+(+1)+⋯+(+1)⏟m=0-m+\underbrace{(+1)+\dots+(+1)}_{m}=0−m+(+1)+⋯+(+1)⏟m=0\begin{aligned}-m+\underbrace{(+1)+\dots+(+1)}_{m} &= 0\end{aligned}

But the two branches of the standard cusp have opposite source orientations. Taking this into account, each trace has sign −1-1, and the count does not vanish:

Inew=I(f1)−m=−2m≠0I_{\mathrm{new}}=I(f_1)-m=-2m\neq0Inew=I(f1)−m=−2m≠0\begin{aligned}I_{\mathrm{new}} &= I(f_1)-m\\&= -2m\\&\neq 0\end{aligned}

The next step invokes the Eliashberg–Murphy cancellation theorem, which requires the signed double-point count to be zero. That hypothesis fails, so the oriented-surgery and embedded-brane construction that follows is unsupported, and the main algebraicity theorem is not established.

According to the other two notices, both manuscripts relied on an adaptation of this construction. The same sign problem blocks the double-point cancellation there, leaving a gap in their main theorems.

Corrections (14)

The fourteen manuscripts below were not withdrawn; new editions were released. Some fill gaps in proofs, some correct statements, some state their hypotheses and dependencies more clearly, and one removes an obsolete citation. The notes in the tables are the version notes from each edition’s README, lightly shortened.

The one history.md lists as a corrected claim is “Taming implies compatibility on four-manifolds”. It restricts the cone-equality claim to the case hJ−=b2+−1h_J^-=b_2^+-1 and adds a four-torus example where the inclusion is strict.

Lipschitz heights and Ashkin–Teller currents (4)

ManuscriptWhat changedEditions
Uniform real Lipschitz surfaces on the triangular latticeRepairs the boundary-attachment, landing-comparison and multiscale separation arguments, including the conditional walk and hookup steps; supplies terminal-side identification and harmonic-mass nonreturn for whole-curve convergence.Sep 25 → Oct 6
new / previous
Gaussian free-field limits of weighted integer Lipschitz heightsSupplies the annulus proof of the circuit estimate used in the discrete argument.Sep 25 → Oct 6
new / previous
The Gaussian free field limit of integer Lipschitz heights with two-arc boundary dataDerives the conditional cut and loop estimates from the companion weighted annulus circuit theorem at x=1x=1.Sep 25 → Oct 6
new / previous
The joint scaling limit of critical Ashkin–Teller currentsCorrects the transmission and boundary-collar arguments and replaces excursion convergence with a signed-loop-soup/GMC argument tied to the same limiting field; updates the companion citation.Sep 25 → Oct 6
new / previous

Kähler minimal model programs and abundance (6)

ManuscriptWhat changedEditions
Finite ordinary minimal model programs on compact Kähler fourfoldsAdds carrier-positivity and multiplier-ideal arguments and revises the contraction induction for ordinary negative-ray programs.Oct 5 → Oct 6
new / previous
Termination of generalized-canonical flips on compact Kähler fourfoldsClarifies that only independent negativity, codimension-two smoothness and cycle-comparison results are used from the companion fourfold paper.Oct 5 → Oct 6
new / previous
Termination of generalized log canonical flips on compact Kähler fourfoldsClarifies the independent relative MMP and birational-comparison inputs and updates citations to revised companion papers.Oct 5 → Oct 7
new / previous
Conditional good minimal models for compact Kähler fourfoldsClarifies the independent ordinary-MMP input and states the remaining Iitaka-subadditivity and effective-abundance hypotheses explicitly.Oct 5 → Oct 6
new / previous
Log abundance for compact Kähler spaces under logarithmic Iitaka subadditivitySupplies base-presentation and multiplier-ideal arguments for the induction, including the adjoint pullback and contraction-descent steps.Oct 4 → Oct 6
new / previous
Numerical semiampleness of nef adjoint classes on compact Kähler manifoldsStates the Iitaka, model and contraction inputs used in the divisorial-decomposition argument explicitly.Oct 4 → Oct 6
new / previous

Taming and hypersymplectic deformation (2)

ManuscriptWhat changedEditions
Taming implies compatibility on four-manifoldsCorrects the cone-equality claim: characterizes the compatible cone by intersection positivity, restricts the cone-sum equality to hJ−=b2+−1h_J^-=b_2^+-1, and adds a four-torus example of strict inclusion.Sep 23 → Oct 6
new / previous
Deforming hypersymplectic four-manifolds to hyperkähler triplesClarifies the prescribed cohomology-class criterion, removes an unnecessary cone-comparison citation, and updates the companion citation.Sep 23 → Oct 7
new / previous

Others (2)

ManuscriptWhat changedEditions
Incompressible Box Transport and Finite ComputationSupplies effective torus-projection and common-clock decay estimates, including the projected-force and pressure bounds.Sep 27 → Oct 6
new / previous
Exact Birch–Swinnerton-Dyer Formula from Low Selmer CorankRemoves an obsolete introductory citation to a removed supporting manuscript and updates citations to revised manuscripts.Oct 3 → Oct 7
new / previous

Citation updates (13)

In the thirteen manuscripts below only the citations changed, not the content. Following the corrections above, they now cite the revised editions of companion papers, and their version dates moved forward.

  • A pointwise 2-converse for elliptic curves with rational two-torsionSep 24 → Oct 7 new / previous
  • Abelian covers, Gale correspondences, and the Hodge conjecture for powersSep 30 → Oct 6 new / previous
  • Fontaine–Mazur modularity at the prime 2Sep 23 → Oct 6 new / previous
  • Goldfeld's analytic density conjecture and the 2-converse for elliptic curvesSep 23 → Oct 7 new / previous
  • Hilbert's tenth problem over the rational numbersSep 24 → Oct 6 new / previous
  • Milne's rationality conjecture for abelian varietiesSep 23 → Oct 7 new / previous
  • The mean analytic rank of quadratic twists of elliptic curvesSep 23 → Oct 6 new / previous
  • The p-adic section conjectureSep 24 → Oct 6 new / previous
  • The rational Hodge conjecture for CM abelian varietiesSep 30 → Oct 6 new / previous
  • The Selmer converse for elliptic curves at every primeSep 24 → Oct 7 new / previous
  • The two-primary Birch–Swinnerton-Dyer formula in Selmer corank at most oneSep 24 → Oct 6 new / previous
  • Unrestricted pro-modularity at the prime twoOct 4 → Oct 6 new / previous
  • Weil classes and Hodge classes on abelian powersSep 30 → Oct 6 new / previous

New formalizations

Six formalizations and five other additions covering supporting results were added. With them, the top-line results of 300 of the 719 manuscripts (about 42%) are formalized[2]. The README at release gave no percentage, saying only that many, but not all, of the manuscripts had been formalized.

Finding versions, and caveats

  • Corrected manuscripts: a new edition sits in a new directory with a new date (e.g. …-October-6-2026). The version note in its README links to the previous edition.
  • Withdrawn manuscripts: a withdrawal notice replaces the manuscript at its old location, and the pre-withdrawal PDF can be read at the release commit adc7f12. They no longer appear in the manuscript map (CONTENTS.md).
  • Dates: the withdrawal notices are dated October 6, the heading in history.md says October 7, and the commit reached GitHub on October 8 (UTC). This page uses the date in history.md.
  • Reliability: all manuscripts are preprints that have not been peer reviewed. The repository itself says that unformalized results could have issues[1].

Changes to this page

  • October 9, 2026 Published, covering history.md up to the update of October 7, 2026.

References

  1. OpenAI, openai/math: mathematical manuscripts and supporting proof artifacts, GitHub, 2026.
  2. OpenAI, openai/math: History, GitHub, 2026.
  3. OpenAI, Withdrawal notice: Algebraicity of Weil classes on split abelian eightfolds, openai/math, October 6, 2026.