OpenAI 未發布模型 Astra 解決 10 項數學難題，並以 Lean 軟體驗證證明

據報導，OpenAI 使用一款名為 Astra 的未發布進階模型，成功解決 10 項長期未解的數學難題。解決的問題涵蓋高維度球體填充、錯誤更正碼極限、複雜網路結構模式、量子賽局理論，以及涉及後量子網路安全技術的高維度網格目標搜尋。 OpenAI 為這些解答發布了超過 250 頁的論文，外加 60 頁描述構想過程的文件，並使用數學證明驗證軟體 Lean 認證了每一項結果。其中最受矚目的成果是證明了「非軟群」（non-sofic groups）的存在，該問題已懸而未決數十年。 然而，這項發表引發了學界對於 AI 與人類貢獻比例的爭議。OpenAI 最初在公告中稱這些問題「至少十年內在主要結果上毫無進展」，引發劍橋大學與匈牙利 Alfréd Rényi 數學研究所等學者不滿，指出非軟群的證明實際上高度依賴學者 Gábor Kun 與 Andreas Thom 在 2016 及 2019 年發表的研究基礎。 在學者反映後，OpenAI 發言人證實已修改公告措辭，改為「解決或對長期未解問題取得實質進展」，以承認近期人類數學家的貢獻，但該網頁並未加上任何更正註記。