ハクソク

世界を動かす技術を、日本語で。

OpenAIが3つの数学的成果を撤回

2026年10月8日原文(twitter.com)

概要

OpenAIのGitHubリポジトリにて、Leanによる新たな形式化が追加 6件の新規形式化、19件の修正、3件の撤回が実施 全体の約42%の主要成果が形式化済み 今後も新たな形式化やエラー修正を継続予定 詳細はhistory.mdで確認可能

OpenAI数理GitHubリポジトリの最新アップデート

  • OpenAIの GitHub mathリポジトリ で、 Lean形式化 の大幅更新
  • 6件の新規Lean形式化 追加
  • 19件の既存内容 に対する修正
  • 3件の内容撤回 （withdrawals）
  • リポジトリ全体で 約42%の主要成果 が形式化済み
  • 今後も 新たな形式化 や エラー修正（errata） を随時追加予定
  • 詳細な変更履歴は history.md （GitHubリンク）で公開
  • Dan Roberts（@danintheory）による公式アナウンス
  • 数学的成果の 信頼性向上 と 透明性確保 を目指す取り組み
    • Leanによる形式化で 証明の厳密性 を担保
    • エラーや修正点も 随時反映 する運用方針

今後の展望

  • 形式化率のさらなる向上 を目指す計画
  • コミュニティからのフィードバック も歓迎
  • 数学分野における 形式化証明の普及促進
  • 継続的な 品質向上と情報発信

Hackerたちの意見

じゃあ、3つの撤回された証明はLeanで検証されてないやつだったの？もしそうなら、なんでLeanで検証された証明と自然言語の証明を混ぜたのかな？アーロンソンのブログを読みながらずっと疑問に思ってたんだ。 「少なくとも、これは証明だって確信してる！他の372の画期的な結果のいくつかにはLeanの証明書があるけど（全部じゃないけど）。でも、どうやら人間はこれらの証明をほとんど理解してないみたい。」 明らかにすべきことは、検証済みのものと、いいアイデアがあるかもしれないけど間違いもあるかもしれないものを2つの部分に分けて公開することだと思う。後者は人間が検証するのにかなり手間がかかるだろうね。