研究與評測
OpenAI 發布內部前沿模型數學新成果，於 GitHub 分享 Lean 證明與運算力估算
OpenAI News綜合 2 家報導一手來源
核實資料不足
來源為發布方或研究資料；不代表所有主張已獲獨立核實。
查證回合用盡，未形成有依據結論
OpenAI 發布了其內部前沿模型在數學未解問題上的新研究成果。官方已在 GitHub 上分享 Lean 證明形式化（Lean proof formalizations）以及相關研究細節。此外，公開的資料中還包含了以 ChatGPT Pro 使用量為基準所估算的運算力消耗細節。
讀原始報導社群討論
社群對 AI 宣稱解決 90 個前 500 大數學未解難題（如 Unique Games Conjecture、超越 O(nlog(n)) 的整數乘法）感到震驚，且平均每個結果僅耗費約 3 小時 ChatGPT Pro 思考算力。然而，許多人質疑如此龐大的論文量難以人工審核，且 Lean 證明可能存在定理表述錯誤的風險。此外，這也引發博士生研究遭搶先的焦慮，以及對 OpenAI 無視 AGMAI 呼籲、依賴社群免費驗證的道德批評。
來源
- Hacker Newsopenai.com
- Reddit r/singularityreddit.com
- Techmemetechmeme.com
- Techmemetechmeme.com
- The Verge AItheverge.com
本期分類