要約（3行）
- OpenAI は GitHub の「openai/math」に、公開前の社内モデルが作った数学の論文（原稿）719本を置いている。372の「ファミリー」（関連する論文のまとまり）に分け、READMEによれば、モデルに出した問題は約4,000問、1つの結果につき平均3時間分の ChatGPT Pro の思考計算を使った。OpenAI の記事「Sharing AI progress in mathematics」は 10/6 付（記事は開けず、公式 RSS の要旨で確認）。
- 更新履歴の 10/7 の項によると、ある論文の符号の誤りで、安定化トレース相殺の議論が成り立たなくなり、同じ構成を使う2本も含む3本の原稿を取り下げた。別の14本を修正し、証明ソフト Lean での形式化を6件足した。
- 全体の約42%（300/719）の主な結果が形式化されている。READMEは「形式化されていない結果には誤りがありうる。すぐ直すよう努める」と書いている。
今後の使い方の流れ
- 「確認の段階」を見分ける。 READMEは、結果が検証の異なる段階にあり、すべてに Lean の形式化が付くわけではないと説明している。形式化があるものとないものを分けて読む。
- 取り下げ・修正の履歴を見る。 更新履歴に日付ごとに、取り下げ・修正・形式化の追加が書かれている。取り下げた論文には、理由と、保存された原稿へのリンクを載せたお知らせが付く。
- 引用や紹介の前に、最新の版か確かめる。 修正された論文は、古い版も版の説明から読めると書かれている。紹介するなら、どの版かを書く。
- 形式化の進み方を追う。 READMEは、Lean の形式化は入手でき次第、リポジトリを更新すると書いている。
この発表で何が変わりそうか（分析）
- AI の出した数学の成果は、「誰かの確認」より「機械が検査できる証明」で信頼を積む方向が見える。 形式化の割合を数字で示し、残りには誤りがありうると明記する書き方は、その方向の取り組みと読める【推測】。
- 公開のあとに、問題が見つかって直す流れが公開の仕組みに組み込まれている。 履歴の公開、版の保存、取り下げのお知らせ、修正の一覧がセットで置かれている。公開直後から間違いが見つかっていく前提で作られていると読める【推測】。
- 取り下げの理由は、1つの符号の誤りが、後続の論文に連鎖したこと。 1本の誤りが、同じ構成を使う2本を巻き込んだ。修正は、表現の整理から証明の補強まで幅がある。
- 人が関わった箇所も分かれている。 READMEは、ほとんどは同じ手順で作ったが、リーマンゼータ関数の零点がない領域の結果と、CM アーベル多様体のホッジ予想の証明は例外で、前者は読みやすさのため人が手を入れたと書いている。
- 評価は、これから外部の専門家の目で決まる。 今回の資料では、個々の主張の正しさを第三者が確かめた結果は確認できていない（第三者の議論は、Hacker News で上位に出ていたが、開いていない）。
- 中の人の言葉：READMEと履歴は会社名義で署名した個人の発言がなく、載せない。
出典
- OpenAI「openai/math」README（GitHub）github.com ↗ ／ 本文の取得元 raw.githubusercontent.com ↗
- OpenAI「openai/math」更新履歴（2026-10-07 の項）raw.githubusercontent.com ↗
- OpenAI「Sharing AI progress in mathematics」（2026-10-06、公式 RSS の要旨のみ）openai.com ↗
確認メモ（2026-10-09 に確認）：README と更新履歴の全文を開いて、数字（719本・372ファミリー・約4,000問・3時間・約42%・取り下げ3本・修正14本）と日付を確かめた。openai.com の記事ページは 403 で開けず、10/6 付の記事は公式 RSS の要旨だけを見た。個々の論文の内容と正しさ、第三者の評価は確かめていない。
