「Lean検証済み」と書かれた証明でも、Leanが検査するのは機械向けの言語で書かれた文章です。人間が読む元の証明と意味がずれていれば、お墨付きは当てになりません。Science誌が報じた研究者たちの懸念を入口に、OpenAIのナビエ・ストークス証明で見つかった「Lean版が元の主張より弱い」という食い違いを紹介します。機械による検証と人間の理解の違いを考えます。
〇AI is shaking up math. But can its proofs be trusted?（2026年10月28日）
https://www.science.org/content/article/ai-shaking-math-can-its-proofs-be-trusted
〇Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs（2026年10月）
https://arxiv.org/pdf/2610.08144
〇AIが3本の道を1点に束ねた——87年来の「ヤコビアン予想」に反例、決勝戦の夜に（2026年7月22日）
https://note.com/math_translator/n/nd994ba292d1d
#数学 #数学の翻訳家 #数学翻訳家 #AI #人工知能 #形式化数学 #Lean #定理証明 #証明 #OpenAI #ナビエストークス #数学者 #査読 #未解決問題 #研究 #科学ニュース #テクノロジー #Anthropic #ClaudeFable5 #数学の美しさ #AI数学 #信頼性 #検証 #ケプラー予想 #数学の世界
感想
まだ感想はありません。最初の1件を書きましょう！