標籤: lean

OpenAI 10 月 6 日在 GitHub 公開內部前沿模型產出的 722 篇數學稿件，分成 372 個結果家族，其中包括 ζ 函數在 Re s > 7/8 沒有零點的準黎曼假設證明。整理產出流程、主要宣稱、Lean 形式化實際涵蓋的範圍，以及數學界對驗證與揭露方式的批評。