數學家呼籲同行停止與 OpenAI 合作

OpenAI 公布了 372 項成果，出自一個尚未釋出的內部模型，並稱這些成果解決或推進了數學與理論電腦科學中長年未解的問題，Scientific American 報導。其中包括四維 Kakeya 猜想，不少證明已用 Lean 驗證，Lean 是一種能檢查證明邏輯的語言。OpenAI 發言人表示，幾乎所有成果都來自對單一 AI 代理人下的一道提示詞。

爭議在於資訊揭露。OpenAI 先前發表 Navier-Stokes 成果後，成立了一個數學家顧問小組，該小組建議公開每項成果背後的模型、完整提示詞與運算時間。OpenAI 只提供平均運算時間，沒有提示詞，並表示這些建議對它沒有約束力。MIT 的 Andrew Sutherland 對該雜誌說，在外界能夠重現之前，這類一次生成的說法都無法驗證；多倫多大學的 Daniel Litt 則說，這次釋出對數學有益。

對評估實驗室研究說法的人來說，任何人都能重跑 Lean 檢查來驗證一份證明，但模型是怎麼產出這份證明的，沒有模型和提示詞就無從驗證。