數學研究

OpenAI 公布內部前沿模型數學成果，以 GitHub 與 Lean 強化可驗證性

本體評估 OpenAI 此次發布為正面且具戰術意義的進展，因其主動採用 Lean 形式化驗證與算力消耗揭露，成功將技術宣傳轉化為具備可證偽性的科學對話。然而該評價附帶保留條件：在底層模型尚未全面開源、生成流程無法端到端重現，且 Lean 驗證尚未覆蓋全部證明的現狀下，此發布僅能視為建立驗證協議的過渡原型，尚不足以確立其已解決 AI 生成證明的不可信問題。