IT・AI
2026年10月8日
OpenAIのAI数学証明、英語訳とLean証明が食い違うと海外で議論
「IT・AI」の記事
OpenAIがAIを使ってNavier-Stokes方程式に関する命題を「解決した」と発表した件で、その証明には形式検証用の言語Leanで書かれた版と、人間向けの自然言語版の二つがある。arXivに投稿された論文「Navier-Stokes Lost in Translation」は、この二つが実は同じ主張を証明していないと指摘し、Hacker Newsで議論になった。スレでは、Lean証明自体の正しさは誰も疑っていないという前提のもと、それでも問題が「解決した」と言えるのか、査読を経ずに報道されることの危うさ、そして人間が読む自然言語の証明がそもそも何のためにあるのかという論点で意見が分かれた。
Navier–Stokes、翻訳で迷子になる
出典: arxiv.org / 元記事はこちら
3
海外の名無しさん
2026-10-07 16:31
AI生成の証明を報じるときは、他の研究と同じようにコミュニティがレビューして検証するまで、少なくとも『証明したと主張している』という書き方にすべきだと思う。AI企業は査読の対象外、という考え方は害がある。
19
海外の名無しさん
2026-10-07 16:49
>>3 俺の理解では、Lean側の証明が正しいこと自体や、それが実際に主張している命題を証明していること自体に異論は無い。それで『解決した』と言うには十分。自然言語の証明は『あればいいね』程度のもの。
4
海外の名無しさん
2026-10-07 16:25
俺の理解が正しければ、これは自然言語の証明とLeanの証明が同じことを言っているかを疑問視してるだけで、Lean側の証明自体の正しさは疑ってないってこと?
22
海外の名無しさん
2026-10-07 16:32
>>4 Lean側が正しいかどうかは検証しやすいけど、それが『本当に証明したいこと』を証明しているかどうかはもっと難しい問題。コードがコンパイルできたからってバグが無いとは限らないだろ。
23
海外の名無しさん
2026-10-07 16:53
>>4 その通り。自然言語の証明は間違ってるけどLeanの証明は正しい。人間も同じミスをする。仕様書を書いて、それをコードに翻訳して、コードが動かなくて、最終的にコードは直すけど元の仕様書を直し忘れる、みたいな。
24
海外の名無しさん
2026-10-07 16:42
>>4 自然言語側の証明に誤りが見つかったわけじゃなくて、単に『違う』ってだけじゃないの?
5
海外の名無しさん
2026-10-07 16:22
Navier-Stokes方程式が何なのかをざっくり知りたい人向けに(リンク参照)。
28
海外の名無しさん
2026-10-07 16:31
>>5 これすごく良い。数学全部これくらい色分けして説明してほしい!!
7
海外の名無しさん
2026-10-07 16:57
Leanで書かれたあらゆる証明に対して検証器を書けると提案する人が多い気がする。これって不完全性定理と矛盾しないのはなぜか、簡単に教えてくれる人いる?
31
海外の名無しさん
2026-10-07 17:01
>>7 不完全性定理が言っているのは、ある公理系の中で真とも偽とも証明できない命題が存在するということ。Leanで証明が書けるなら、その命題はそもそも不完全性の範囲外にあるということ。
32
海外の名無しさん
2026-10-07 17:00
>>7 『役に立つ証明』に限ればそう。証明している系そのものについてのメタな主張をすれば、どんどん複雑で面白くもない定理を作れてしまう。ある段階になると、系は自分自身についての問いには答えられなくなる。
8
海外の名無しさん
2026-10-07 16:46
非圧縮流体の中のピストンみたいなもんだよ、要するにコップの中の嵐。
12
海外の名無しさん
2026-10-07 16:39
数学者じゃないんだけど、なんで最初からLeanだけ使わないの? 自然言語をわざわざ使う理由は?
36
海外の名無しさん
2026-10-07 16:45
>>12 Leanは読むのがすごく大変で、詳細のレベルが高すぎるから。読めるレンマでも、あまりに細部まで書かれていて、人間の作業記憶の限界のせいで本当の理解が難しくなる。
37
海外の名無しさん
2026-10-07 16:46
>>12 じゃあなんでいつも機械語で書かないの? プログラミング言語を使う理由は?
39
海外の名無しさん
2026-10-07 16:43
>>12 人間がコードを書くのと同じ理由。コンパイラが機械語に翻訳するためだけじゃなく、他の人間がそれを理解したり、そこから学んだり、修正したりできるようにするため…
18
海外の名無しさん
2026-10-07 17:01
>>2 『Navier-Stokesの元の「自然言語」のアイデアを正しく形式化していない』って、『正しく形式化していない』の意味で書いたつもり?
20
海外の名無しさん
2026-10-07 16:36
>>3 『AI企業は査読の対象外、という考え方は害がある』 そんな考え、どこかで見かけたことある? これってそもそも、OpenAIの主張が検証されてるっていう投稿のコメント欄だよね?
49
海外の名無しさん
2026-10-07 16:49
>>20 OpenAIは、自分たちの結果を査読付き論文に投稿する(あるいは投稿すると言う)ことをしていない、という態度でその考えを示している。
64
海外の名無しさん
2026-10-07 16:55
>>49 あれはオープンソースの精神で公開されてるんだと思う。狭い意味での『査読』は主に学術界での名声を割り振るためのもので、GitHubのリポジトリを誰かが『査読』することを妨げるものは何もない。
65
海外の名無しさん
2026-10-07 16:53
>>49 どこかの論文誌に出していないのと、『査読の対象外』と言っているのは全然違う話。今まさにOpenAIの主張をレビューしてる人たちがいるじゃないか。
25
海外の名無しさん
2026-10-07 17:07
>>4 そうなんだけど、自然言語の証明と形式証明が『対応している』かどうかの判断自体が主観的なんだよな。
27
海外の名無しさん
2026-10-07 16:32
>>4 その通り。AIが自然言語版の証明を正しく書くことへの実質的な圧力は無いし、それを自動的に判定する方法も無い。
38
海外の名無しさん
2026-10-07 16:56
>>12 Figure 1の例を見ればわかるはず…自然言語版の方が人間にはずっと読みやすい。
40
海外の名無しさん
2026-10-07 16:44
>>12 何が証明されているのかを人間が理解する必要があるから。
41
海外の名無しさん
2026-10-07 16:47
>>12 Leanは書くだけのプログラミング言語だよ(書いた後、誰も読めない)。
43
海外の名無しさん
2026-10-07 16:30
>>13 『downvoteの多さが反対意見の多さを示してる』『論破したぜ!』 問題を見誤ってると思うよ。
44
海外の名無しさん
2026-10-07 16:47
>>14 Lean側の証明の正しさに異論を言ってる人はいない。問題は自然言語への変換の出来が悪かったってこと。
45
海外の名無しさん
2026-10-07 16:37
>>14 その通り。自然言語とLeanの間をAIに翻訳させたことは無いけど、英語からGolang、Python、TypeScript、SQLへの翻訳はやらせたことがあって、その『解釈』はなかなか…創造的だったよ。
47
海外の名無しさん
2026-10-07 17:01
>>19 元記事の主張は、Leanでの形式化がその問題の自然言語での記述と対応していない、つまり証明された命題が『解決した』と言うために証明すべきだった命題ではない、というもの。
60
海外の名無しさん
2026-10-07 17:07
>>47 それは元記事の主張じゃない。他のコメント、特にDeepMindのFormal Conjecturesでの表現についての話を見て。
50
海外の名無しさん
2026-10-07 16:51
>>20 LLMが生成したLeanの式がコンパイルできたというだけで、様々な数学的事項が『証明された』と報じる、息を切らしたような報道をたくさん見てきた。人間が書いた証明だったら、査読者が誤りをチェックするまでそうは発表しないはずなのに。
68
海外の名無しさん
2026-10-07 16:57
>>50 その通り。フェルマーの最終定理の証明の検証には15か月以上かかった。プレスリリースと、急いでほぼAIが書いた原稿だけを根拠に、大問題が解決したとメディアが報じているのはばかげている。OpenAIなんかはそういう軽率な報道に乗っかって喜んでいる。
69
海外の名無しさん
2026-10-07 16:56
>>50 まさにそれ。この件の報道は『OpenAIが問題Xを解決した』であって、『OpenAIが問題Xを解決したと主張している』ではない。
55
海外の名無しさん
2026-10-07 16:42
>>22 構文の話と意味論の話(syntax vs semantics)だね。
56
海外の名無しさん
2026-10-07 17:04
>>23 自然言語の証明が間違っているって、どうやってわかるの?
57
海外の名無しさん
2026-10-07 16:47
>>28 できるよ。コードがあるだけじゃなく、対話的なエディタもある。
59
海外の名無しさん
2026-10-07 16:48
>>39 それだけじゃなく、コードのコメントや独立したドキュメントもある。
70
海外の名無しさん
2026-10-07 16:58
>>53 『自然言語の証明はLeanのコードから、ずさんに作られた』 本当に? LLMがLeanの中で推論してるとでも言うの? これ(とOpenAIなどの他の証明)は逆の順序で作られてるはずだけど。『エージェントたちは9月5日土曜、最初のエージェントが起動してから約88時間後に解に到達した。Leanでの形式化と検証にはGPT-6 Astraでさらに17時間かかった』(OpenAIの発表記事より)
73
海外の名無しさん
2026-10-07 17:01
>>70 そうそう、LLMがLeanで直接推論してると思ってる人がいるのに驚いた…学習データは全部自然言語なのに。
この話題の背景と論点
Leanは定理証明支援系と呼ばれるソフトウェアで、証明の各ステップを機械的に検証できる一方、人間がそのまま読んで意味を追うのは難しい。そのため研究者は通常、Lean証明と並行して自然言語の説明を書き、両者が同じ主張を証明していることを示す。今回話題になった論文は、AIが生成したNavier-Stokesに関する証明で、この自然言語版とLean版の対応に食い違いがあると指摘した。スレで割れたのは、Lean証明自体の正しさは誰も疑っていない中で、それでも「解決した」と呼べるかという一点。査読を経ずにプレスリリースベースで「解決」と報じるメディアの姿勢への批判も多く、フェルマーの最終定理の査読に15か月以上かかった過去の例が引かれていた。不完全性定理との関係を尋ねる質問も出たが、これは「証明できない命題が存在する」という定理であり、実際に証明が書けた命題はそもそもその範囲外にあるという整理がされている。
※本記事は海外掲示板 Hacker News のスレッド「Navier–Stokes Lost in Translation 」から抜粋し、編集部で日本語に意訳したものです。訳文の責任は当サイトにあります。
続けて読む（IT・AI）
この記事のリアクション
😆 おもしろい 0 😮 びっくり 0 😢 かなしい 0 👍 わかる 0 😠 ひどい 0
まだコメントはありません。