>>605 戻る
(引用開始)
下記の ＜文字起こし＞が面白い
１）加藤文元：一応その論文っていうのは自然言語で書かれてるわけじゃないですか
　それであの、それをあの、Leanに翻訳しなきゃいけないわけですよ
　で、あの、自然言語だったら、ま、なんとなく曖昧な部分でありますよね
　本当どう言ってるのかわからないで解釈不能な部分っていうのは許されるじゃないですか
２）Lean言語の時っていうのは解釈があの完全にこういう解釈だっていう風なことが分からないと
　あの書けないんですよ。 はい。 そうするとあの結局あの書けない部分がある
３）うん。 まだ分かってない。理解できてないからかけないだけなのかがそこが分からないのか。
　でもね、数学の論文って多かれ少なかれ やっぱりギャップはあるる。ギャップって必ずあるんです。
　そこ望月さんにそこ埋めてもらうしかないです。 ここがちょっと翻訳できない。望月さん、ちょっと
加藤文元さんの語り、面白い （＾＾
https://youtu.be/b6JlM_nrM3M?t=1
【ReHacQ生配信】AIで数学を証明!?IUT理論は正しいのか【高橋弘樹vs川上量生vs野村泰紀vs加藤文元】
ReHacQ−リハック−【公式】
166,727回視聴 2026/07/24
(引用終り)

１）まず、一般の理系では Leanに対する 自然言語の優位性がある
　つまり、自然言語は 赤ちゃんが、辞書（言葉の定義）も文法書（ルール）もなしで 母国語を習得する
　人間のディープラーニングだろう
２）自然言語では、厳密な語の定義なく 文法も厳密ではない。だが 分かり合える。人間だものｗ
　実は、数学以外の理系の学問では その方が良い
　というのは、数学以外の理系は 自然が相手で 自分が間違っていれば 実験と事実とかと合わないのですぐ分かる
　数学では、厳密性が尊重される（証明の有無が重要）ので事情が違うが、
　しかし 新しい数学を作っていくときには 自然言語による思考が適している
　なので、数学論文も数式や記号論理もあるが、その行間は自然言語で埋める。その方が圧倒的に読みやすい
３）が、たまに論文が難解すぎて「この証明大丈夫か？」と言われることがある
　そのとき、普通には 時間が経つと 別証明が出てきたりして、みんな納得するのだ
　なお過去にも、”コンピュータ証明をかけよう”というのはあった（有名なのが下記 フェイト・トンプソンの定理）
４）今回、IUT論文を コンピュータ証明にかけようと Lean化したが 途中で まだうまくいかないという 中間報告

取り敢えず、額面通り受け止めたらどうよ？
望月先生、がんばってください（＾＾

(参考)
https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A7%E3%82%A4%E3%83%88%E3%83%BB%E3%83%88%E3%83%B3%E3%83%97%E3%82%BD%E3%83%B3%E3%81%AE%E5%AE%9A%E7%90%86
フェイト・トンプソンの定理（奇数位数定理とも呼ばれる）
証明の改訂
完全に形式化された証明は、Rocq証明支援システムによって検証され、2012年9月にジョルジュ・ゴンティエ（英語版）とマイクロソフトリサーチおよびINRIAの研究者によって発表された[12]。