一龍馬/AI 情報站讀懂消息背後的脈絡
星期六
搜尋

團隊強調這不代表兩版證明都錯,而是自動形式化為了讓程式能編譯通過,可能悄悄改寫邏輯

中文摘要

劍橋大學團隊指控 OpenAI 的 Navier-Stokes 證明出現自然語言版與 Lean 程式版不一致,Lean 版把 Lemma 8.6 的界線寫成 m+5,比原文的 m+4 更寬鬆。團隊強調這不代表兩版證明都錯,而是自動形式化為了讓程式能編譯通過,可能悄悄改寫邏輯。OpenAI 向 New Scientist 表示已知落差,並稱不代表任一證明無效,將持續修正。

一龍馬判讀

對數學家而言,風險是把 Lean 可編譯等同於論文已通過同儕審查;若長證明被靜默改寫,查核成本會落在人力逐段比對上。

原文節錄

Hacker News

that they don’t match.

取得全文 · 不代表內容已獨立查證

查看原文 閱讀社群討論
完整收錄文字與來源

OpenAI mistranslated mathematics into code for its Navier-Stokes proof

收錄日期
2026-10-10
來源
官方 RSS+Hacker News Algolia API
抓取時間
2026/10/10 06:00(台北)