#Lean

オープンエーアイは6日、未公開の最先端模型が約4000問から372系統・原稿722本の数学成果を出したと公式に公開した。8日には社内研究者がリーン形式化の追加と3本の撤回を告知し、準リーマン予想をフィールズ賞級と見る声と、符号誤りや原稿と形式化のずれを根拠に未検証だと見る声が同時に出ている。

OpenAIが次期主力候補Astraの内部版で数学・理論CSの未解決問題10件に新成果を出し、Lean形式証明付きで公開した流れが継続。研究パートナー化の転換点とする声と、査読・第三者検証待ち、さらにはLeanカーネルバグを突いた無効反証の報道を踏まえた慎重論が並ぶ。