OpenAI 本週喺 GitHub 上突然放低近 400 條由 AI 生成嘅數學結論，分散喺超過 700 份手稿入面，涵蓋組合數學、幾何、數論、理論計算機科學、代數、拓撲、概率與統計力學、數學物理等領域。數量大到 OpenAI 要另外出版本瀏覽指引，教人點樣喺嗰堆資料入面揾路。
三十多名數學研究員嘅反應用詞清一色震撼：「驚人」、「壓倒性」、「前所未有」、「超現實」，甚至「純屬癲嘢」（pure insanity）。佢哋指出，光係把約 40 頁嘅目錄同摘要睇完，已經要一個多鐘。康涅狄格大學數學系教授 Álvaro Lozano-Robledo 話：「光係過一遍全部摘要，已經令人有壓倒性嘅感覺。」有學者話：「就算 AI 即刻消失，好似外星人嚟過地球然後就走咗，我哋都要花十年去理解呢堆嘢。」
呢堆手稿入面，有一部分附有 Lean 形式化。Lean 係一種證明輔助程式語言（proof assistant），可以將數學證明轉寫成機械可驗證嘅形式，即係話就算你唔完全明白背後嘅論證，都可以確認佢喺邏輯上成立。呢類形式化之前已經幫過研究者核對過 OpenAI 嘅數學結論。
問題係，呢幾百份手稿嘅驗證程度相差甚遠。OpenAI 喺 GitHub 承認，呢批結論「處於不同驗證階段」，「多數但並非全部手稿已經形式化」。OpenAI 交代，719 份手稿入面只有 300 條頂層結論完成形式化，約佔 42%，並話會喺取得更多形式化後更新儲存庫（update the repository with more formalizations as we obtain them）。
有研究員抱怨形式化比例偏低，特別係喺咁大數量嘅結論入面；佢哋亦強調，就算某條結論附有 Lean 程式碼，驗證本身亦唔係即時完成——研究者要逐條核對形式化有冇真係證明咗佢聲稱嘅嘢，呢個過程本身好耗時。
有學者擔心，就算佢哋自己都要幾先至消化得完，OpenAI 未必會等咁耐，到時「或者仲會放更多」。
模姐驗嚇貨：呢件事最值得關注嘅，唔係「AI 可以寫數學」，而係規模同驗證速度之間嘅落差。42% 形式化，即係超過一半嘅結論仲未齊機械可驗證嘅證明。呢個唔係功能發布，而係一批尚未驗證完成嘅素材。對數學界嚟講，佢哋嘅職業，正係喺呢堆嘢入面分清楚「解決方案」（solutions）同「低質輸出版」（slop）；呢個分別，唔係靠 OpenAI 來劃。
模姐｜深度調教
