10 月 6 日，OpenAI 將由一款未發布的內部模型生成的 719 篇數學論文上傳至 GitHub。此次發布正值其顧問機構於一週前呼籲 AI 實驗室停止在專有模型上測試高等數學問題之後。這一週的時間差凸顯了當前 AI 驅動數學研究中的張力：實驗室利用公開問題衡量模型進展，而數學界部分人士則要求在 AI 生成的結果流傳之前，先進行揭露與傳統的同儕審查。

超過 600 份問卷回覆塑造了 IAS 小組 9 月 29 日的指導方針

位於紐澤西州普林斯頓高等研究院的數學與人工智慧顧問小組，於 9 月 29 日根據超過 600 份問卷回覆發布了其建議。該小組在其指導文件中寫道：「我們想在一開始就明確表示：我們不認可這種做法，並要求他們停止在專有模型上測試高等數學問題。」

同一份文件警告，私下持有的內部模型可能造成一個兩級體系，少數實驗室將遠遠領先其他所有研究者。

根據其儲存庫，OpenAI 作為模型開發的一部分，在公開研究問題上測試其模型，並在現有數學基準測試趨於飽和——即模型在現有測試中得分達到或接近頂端之時——之後擴大了這些測試。該公司表示，曾與顧問小組進行溝通，並參考其建議進行此次發布。在 10 月 6 日發布的聲明中，該小組表示，其顧問角色並不構成「對 OpenAI 取得這些結果之過程的認可」，並將合規與否的判斷交由更廣泛的數學界裁定。

納維-斯托克斯的 Lean 程式碼所證明的命題弱於書面論文

OpenAI 將這 719 篇論文整理為 372 個數學家族，每個家族都圍繞一個主要結果及其相關證明構建。該專有模型被給予約 4,000 道問題，每個結果平均需要約三小時的 ChatGPT Pro 思考運算。

該顧問小組要求 AI 實驗室為每項結果公布模型名稱、所使用的提示詞、摘要化的思維鏈、所需時間以及運算成本。OpenAI 公布了 10 份推理摘要，其頂線結果中約 42% 附有 Lean 形式化。此次發布與該逐項結果清單的吻合程度，正是該小組留給數學界解決的問題之一。

Lean 是一種可讓電腦檢查證明的程式語言。程式碼通過編譯，並不代表程式碼與書面論證完全相同；它只確立該形式化命題為真。研究人員將這種將書面論證轉換為機器可檢查程式碼的方式稱為自動形式化。

Alexander Bastounis、Fabian Circelli 與 Anders C. Hansen 在 10 月 6 日發表的一篇論文中審視了這一落差。他們發現，OpenAI 的納維-斯托克斯書面論文所宣稱的內容強於其 Lean 程式碼所證明的範圍，其中一項估計改變了輸入導數的階數。作者也在 OpenAI 的歐拉證明中發現了類似的錯誤轉換，並寫道，OpenAI 的書面證明與其他自動形式化的 Lean 證明「不應在未經與其他證明相同的同儕審查程序與審視的情況下，被表面地信任」。

OpenAI 於 9 月 8 日宣布了納維-斯托克斯結果。這組方程式是克雷數學研究所千禧年大獎難題之一，每道難題獎金為 100 萬美元。紐約大學數學家 Tristan Buckmaster 隨後質疑該公司對這項工作中人類介入程度極低的描述，如 Cryptopolitan 所報導。該公司已承諾為與重大 AI 成果相關的研討會、會議及特別計畫提供資金。10 月 6 日，數學家陶哲軒撰文指出，使用 AI 系統解題的人往往在解決問題後便對該領域失去興趣，並補充說，許多人無法就相關成果回答問題或發表演講；他的貼文並未點名 OpenAI。

該公司曾表示，其顧問對研究節奏沒有發言權，Cryptopolitan 於 9 月報導。隨著合規判斷現在落入數學界手中，值得關注的指標是：同儕審查將支持還是質疑這些從書面到 Lean 的轉換，以及未來的發布是否會逐項列出該小組要求每項結果應揭露的資訊——模型名稱、提示詞、摘要化思維鏈、時間與運算成本。