26/07/28 22:17:54.11 psEHBHy8.net
ホイヨ
URLﾘﾝｸ(youtu.be)
【ReHacQ生配信】AIで数学を証明!?IUT理論は正しいのか【高橋弘樹vs川上量生vs野村泰紀vs加藤文元】
ReHacQ－リハック－【公式】
166,727回視聴 2026/07/24
今回は東京工業大学名誉教授の加藤文元さんとカリフォルニア大学バークレー校教授野村泰紀さん、
川上量生さんにお越しいただき、数学の超難問「ABC予想」を解決するために作られたIUT理論について、
お話ししたいと思います
出演者：加藤文元
野村泰紀
川上量生
高橋弘樹
【制作協力：ZEN大学】
441 件のコメント
@Rainbow-puke-w2b
21 時間前
野村先生の庶民の理解レベルまで落とし込む要約力、いつも関心させられます。
605:１３２人目の素数さん
26/07/29 00:09:25.01 oyJUr6vp.net
>>604 補足
下記の ＜文字起こし＞が面白い
１）加藤文元：一応その論文っていうのは自然言語で書かれてるわけじゃないですか
それであの、それをあの、Leanに翻訳しなきゃいけないわけですよ
で、あの、自然言語だったら、ま、なんとなく曖昧な部分でありますよね
本当どう言ってるのかわからないで解釈不能な部分っていうのは許されるじゃないですか
２）Lean言語の時っていうのは解釈があの完全にこういう解釈だっていう風なことが分からないと
あの書けないんですよ。 はい。 そうするとあの結局あの書けない部分がある
３）うん。 まだ分かってない。理解できてないからかけないだけなのかがそこが分からないのか。
でもね、数学の論文って多かれ少なかれ やっぱりギャップはあるる。ギャップって必ずあるんです。
そこ望月さんにそこ埋めてもらうしかないです。 ここがちょっと翻訳できない。望月さん、ちょっと
加藤文元さんの語り、面白い （＾＾
＜文字起こし＞より引用
1:04:52
（加藤文元）
あの、つまり、ま、一応その論文っていうのは自然言語で書かれてるわけじゃないですか。 はい。 で、ま、そこにか名があって、ま、どこまで完全理解できるかは別にして、ま、あの、その論文で、あの、なんか説明してるものありますよね。
1:05:05
うん。 で、それであの、それをあの、Leanに翻訳しなきゃいけないわけですよ。 はい。はい。 で、あの、自然言語だったら、ま、なんとなく曖昧な部分でありますよね。本当どう言ってるのかわからないで解釈不能な部分っていうのは許されるじゃないですか。
1:05:19
はい。 Lean言語の時っていうのは解釈があの完全にこういう解釈だっていう風なことが分からないと
1:05:26
あの書けないんですよ。 はい。 そうするとあの結局あの書けない部分がある。
1:05:33
あー自然だから望月さんは自然言語で一応書かれてですね。数式と自然言語交えて書かれてわけですよね。
1:05:40
でそこをコンピューターで厳密なコードみたいな 形にする時に 表現できないものがある。うん。
1:05:47
それで間違ってるってことどう違う? だから本当に原理的にできないんだったら論理が飛んじゃってるわけですよ。
1:05:53
なのか 非常に難しくて理論として繋がってはいるんだけど
1:05:59
うん。 まだ分かってない。理解できてないからかけないだけなのかがそこが分からないのか。でもね、数学の論文って多かれ少なかれ やっぱりギャップはあるる。ギャップって必ずあるんです。
1:06:12
そこ望月さんにそこ埋めてもらうしかないです。 ここがちょっと翻訳できない。望月さん、ちょっと
(引用終り)
606:１３２人目の素数さん
26/07/29 00:30:43.28 hkhoSbjD.net
埋めれるならとっくに埋めてる
607:１３２人目の素数さん
26/07/29 01:21:43.50 6bWpvCfW.net
そもそも望月論文は「証明の行間が空きすぎてわからない」んじゃなくてそもそも「基本的概念の定義が何言ってるかわからない」のが問題。それがわからなければ Lean に「証明のGapのありかをみつけさせる」なんてことも当然できない。だから「諸概念を第三者にきちんとわかるようにきっちり形式化してみせろ」と要求され続けてきた、で、現状やっぱりなという感じ。
もちろん Lean に乗せたコードをみればコードに乗せた本人がどう解釈したのかわかる。しかしそれがでてこない。まぁ出せんのやろ。LANAのメンバーですら、望月論文の諸概念をどのように形式化したらいいのかわかってないんやろ。「どうやって証明すればいいか」以前にそもそも「問題を数学の問題として形式化すらできない」の段階でつまづいてる。
なんとなく数学チックなそれっぽい文章でしかない。
608:１３２人目の素数さん
26/07/29 05:14:01.72 Yw53gzRc.net
形式化すらできない戯言を当然と思ってるのは
大学の微積と線形代数で落第した数学素人のSet Aだけ
609:１３２人目の素数さん
26/07/29 07:54:12.09 JHuvr+tI.net
論理が破綻してるんだから形式化なんてできなくて当然
最初から証明など無い
610:１３２人目の素数さん
26/07/29 09:25:57.35 BxTMhBDE.net
>人生 ピンチはチャンスでもある
>ここを突破すれば、ひと皮むける
>脱皮して 成虫になる
>そう思って、がんばってください
>夜明けは近い
脱皮できずに土の中で腐り●んだ
高卒素人がなんかいうとる
611:１３２人目の素数さん
26/07/29 10:25:59.14 4XyltZAE.net
>>606-610
>>607は、基礎論くんか お元気そうで何よりです。
>LANAのメンバーですら、望月論文の諸概念をどのように形式化したらいいのかわかってないんやろ。「どうやって証明すればいいか」以前にそもそも「問題を数学の問題として形式化すらできない」の段階でつまづいてる。
半分は正しいかもだが
半分以上ハズレではと思う
数学予想が しばしば山登りに例えられる
abc予想山 URLﾘﾝｸ(en.wikipedia.org)
山の頂は見えるが、途中は雲の中だ
望月論文 IUT I～IV URLﾘﾝｸ(www.kurims.kyoto-u.ac.jp)
これを、山のステージ I～IVと見る
各ステージ 1000ｍ級で
4000ｍ越えが IUT IV の ”Corollary 2.3. (Diophantine Inequalities)”P54
で、abc予想の山頂直結部分
Corollary 2.2. (Construction of Suitable Initial Θ-Data) P41
が、山頂直前
いま、問題にされているのは
ステージ IIIの
Theorem 3.11. (Multiradial Algorithms via LGP-Monoids/Frobenioids)P153
↓
Corollary 3.12. (Log-volume Estimates for Θ-Pilot Objects) P173
ここの登山道で、Lean言語でもって道筋を示すマップを作ろうとすると
「なんか 繋がってないのでは？」となった
>>605 加藤文元さんらの語り
”一応その論文っていうのは自然言語で書かれてるわけじゃないですか
それであの、それをあの、Leanに翻訳しなきゃいけないわけですよ
うん。 まだ分かってない。理解できてないからかけないだけなのかがそこが分からないのか。
でもね、数学の論文って多かれ少なかれ やっぱりギャップはあるる。ギャップって必ずあるんです。
そこ望月さんにそこ埋めてもらうしかないです。 ここがちょっと翻訳できない”
まとめると
１）IUT以前は、abc予想山の登り方が、さっぱり分からなかったのだが
２）それにチャレンジした望月さんが、登山マップを自然言語で示した
３）それを Lean語で詳細に書こうとすると、自然言語→Lean語に出来ない部分が
3.11.→3.12.に見つかった（いまここ）
なので、
１）Lean語の方に何か追加するか
２）3.11.→3.12.の自然語記述を、もう少し緻密にするか
３）もっと以前から別登山ルートを探すか
私見ですが、１）or ２）で決着するのでは？ （＾＾
612:１３２人目の素数さん
26/07/29 10:51:16.60 hkhoSbjD.net
ある登山ルート上にどうしても通行できない箇所が1か所でもあればそのルート全体が無価値、登山したくば全く別のルートをゼロから探す必要がある
という当たり前のことがどうしても理解できないど素人さんだったとさ
613:１３２人目の素数さん
26/07/29 10:57:00.59 hkhoSbjD.net
望月のアイデアでは系3.12はどうやっても証明できない、したがってIUTそのものがゴミ
そのことを今から8年も前に正確に見抜いていたSS有能過ぎ
自明だー理解できないおまえが馬鹿なんだーとしか言えないM無能過ぎ
614:１３２人目の素数さん
26/07/29 10:57:10.83 4XyltZAE.net
>>611 補足
>２）それにチャレンジした望月さんが、登山マップを自然言語で示した
>３）それを Lean語で詳細に書こうとすると、自然言語→Lean語に出来ない部分が
> 3.11.→3.12.に見つかった（いまここ）
普通は、問題解決のタスクフォースを作る
その中で いまの場合、IUTとLean語の両方に詳しい人がほしいよね
望月氏や星さんは、Lean語さっぱだろう
なので、望月研の若手に Lean語を勉強させること
それから、ヤコビアン予想で活躍した AI Claudeなどを使う
タスクフォース作って、上記体制を整備すれば
自然言語→Lean語のギャップは 埋まるのでは？
ある程度タスクフォースでやってみて
早期に解決するなら それでよし
解決が長引きそうなら
正直に 全てをオープンにするのが良いだろう
世間で、多くの数学者が IUTを是として活動してきた
例えば、下記のRIMS 次世代幾何学国際センター 2022年4月とか
いろいろある
みんな、IUTのLean化は可能だと思ってきたはず
もし 解決が長引きそうなら
正直に 全てをオープンにするべし
(参考)
URLﾘﾝｸ(www.kurims.kyoto-u.ac.jp)
数理解析研究交流センター
次世代幾何学国際センター
広く次世代の幾何学の研究を推進し、新しい数学の国際的認知度向上のために研究成果を広く世界に向け情報発信するとともに、 国内外の若手研究者など多様な人材の育成を行うために、2022年4月に設置された。
615:１３２人目の素数さん
26/07/29 11:02:28.95 hkhoSbjD.net
>普通は、問題解決のタスクフォースを作る
問題の本質はIUTにABC予想を解くアイデアが何も無いこと
最善策はIUTを捨てること
616:１３２人目の素数さん
26/07/29 11:07:21.12 hkhoSbjD.net
「論文は理解できなかった。 自分の研究に時間を割くことにした。」
ファルティングス（望月の師匠）は最善策を取った。
617:１３２人目の素数さん
26/07/29 11:28:26.35 rIIcIHs2.net
>>611
＞１）Lean語の方に何か追加するか
新たな公理の追加はＮＧ
これわかんないやつは素人
＞２）3.11.→3.12.の自然語記述を、もう少し緻密にするか
この１０年できなかったことを
いまさらほざくのはド素人
＞私見ですが、１）or ２）で決着するのでは？
決着できなかった方法を
いつまでもいうのはド素人
ガロア理論も全く理解できなかった高卒素人が
利口ぶって数学板に書き込むな
618:１３２人目の素数さん
26/07/29 14:05:09.02 4XyltZAE.net
ホイヨ
URLﾘﾝｸ(www.asahi.com)
正しさは誰が判断？ 難問「ABC予想」論争が映す数学と社会
2026年7月29日朝日新聞
神里達博の月刊安心新聞+
正しさをめぐる論争が、14年近く続く数学の証明がある。京都大学数理解析研究所の望月新一教授が2012年に公表した宇宙際タイヒミュラー理論(IUT)による「ABC予想」の証明だ。この予想は、いわば整数の世界における、足し算とかけ算の「奥深い関係」を表す根幹的な仮説であり、解決されれば多くの厄介な難問が一挙に解けるとされる。
望月氏は16歳で米プリンストン大に入学した俊英。数論幾何―「数を図形に置き換えて考える」というホットな分野―で、すでに重要な業績を出していた。世界中の数学者が驚き、注目したのも当然である。
ところが、その証明は合計500ページにも及び、斬新な概念や考え方が多数導入されていたため、理解できたとする数学者はごく少数にとどまった。同時に、批判を展開する数学者も現れた。影響が大きかったのは、ドイツの数学者ペーター・ショルツェ氏らによるものだ。ショルツェ氏は30歳で数学界のノーベル賞とも言われる「フィールズ賞」を受賞した、数学界の若きリーダーだ。彼は京都を訪れ、望月氏と直接議論したが、平行線をたどった。そして18年、IUTの定理3・11から系3・12を導く部分に深刻な問題があると指摘する報告書を公開した。
一般に学術論文は、同分野の研究者による確認作業、「査読」を経る。数学論文の査読は長期化することもあるが、IUT論文は異例の7年半を要した。これを受けて有名な科学雑誌「Nature」は20年4月、「複数の専門家は、ショルツェ氏らの批判が出た時点で、この問題に決着がついたと見なしている」「論文誌への掲載が決まっても、それは変わらないだろう」と報じた。
現状、IUTによるABC予想の証明を、世界の数学界は認めていない。だが「数学的に正しい」とは、結局どういうことなのか。数学者の多数決で決まるわけでもないだろう。望月氏の論文は学術誌の正式な査読を通過したのも、また事実である。事態は膠着（こうちゃく）状態に陥った。
これに対し、打開策として始まったのが、定理証明支援システム「Lean」による検証プロジェクトである。証明をLeanに分かる言葉に書き換え(形式化)、論理の穴がないかを検査する試みである。
プロジェクトチームは今月1…
この記事は有料記事です。残り1218文字有料会員になると続きをお読みいただけます。
URLﾘﾝｸ(researchmap.jp)
神里 達博
Tatsuhiro Kamisato
基本情報
所属千葉大学 大学院国際学術研究院 教授 (総合国際学位プログラム長)
学位
博士（工学）(2012年10月 東京大学)
修士（学術）(1998年3月 東京大学)
研究分野 1
人文・社会 / 科学社会学、科学技術史 /
619:１３２人目の素数さん
26/07/29 14:08:53.07 VPU2iick.net
こういう連中の喰いネタになったか
620:１３２人目の素数さん
26/07/29 14:21:06.15 4XyltZAE.net
>>617
>＞１）Lean語の方に何か追加するか
>新たな公理の追加はＮＧ
>これわかんないやつは素人
素人はおまえ
反例を列挙しよう
１）ZFCの前、"Zermelo set theory" URLﾘﾝｸ(en.wikipedia.org)
では、公理はZFCと異なる形で与えられていた
すなわち、ZFCにおいて加えられた公理も沢山あるよ
２）他に 有名な公理例で ”Grothendieck universe” URLﾘﾝｸ(en.wikipedia.org)
グロタンディーク宇宙公理 は、望月IUT IVでも特筆での解説があるよ
つまりは、一般凡人は、 新たな公理の追加はＮＧだが
しかし、数学天才には 新たな公理の追加は"G"なのだ
果たして、望月氏は 数学天才がどうか？ そこが問題だ by ハムレット
621:１３２人目の素数さん
26/07/29 14:25:02.12 4XyltZAE.net
>>619
>こういう連中の喰いネタになったか
いまさら
前から IUTは
ドワンゴ 川上量生とタッグを組んでいる
ZEN大学の看板ネタ
622:１３２人目の素数さん
26/07/29 14:35:58.04 74ST7Try.net
まーだアホ朝日はシーソーゲーム演出してるのか
数学に対する見識がなにもないくせに
よく妄想だけでこんな恥ずかしいコタツ記事毎度書けるな
623:１３２人目の素数さん
26/07/29 15:02:53.11 hkhoSbjD.net
>正しさは誰が判断？
形式化できないものは誰が判断しても正しくない、というか数学ですらない
そんなことも分からないど素人が数学を語るな
624:１３２人目の素数さん
26/07/29 15:06:56.43 hkhoSbjD.net
>望月氏は16歳で米プリンストン大に入学した俊英。
しかしアラフィフで「自明だー、理解できないのはお前が馬鹿だからだー」と駄々をこねる子供おじさんになってしまった
625:１３２人目の素数さん
26/07/29 15:11:19.66 hkhoSbjD.net
>つまりは、一般凡人は、 新たな公理の追加はＮＧだが
>しかし、数学天才には 新たな公理の追加は"G"なのだ
じゃあSSに間違いを指摘されても人格攻撃しかできない凡人中の凡人はNGだね
626:１３２人目の素数さん
26/07/29 15:12:08.80 4XyltZAE.net
>>617
>＞１）Lean語の方に何か追加するか
>新たな公理の追加はＮＧ
>これわかんないやつは素人
下記のヒルベルト空間の例が合っているかどうか だが
有限次元の線形空間を Leanで扱えるようにはなっても
当然だが、無限次元は扱えない
だから、例えば 無限次元ヒルベルト空間を扱うための
Mathlib を整備すれば、その整備されたMathlibの範囲において
無限次元ヒルベルト空間が扱えるってことだね
これを、望月IUTにおいてみるに、まずIUT以外での
確立された遠アーベルMathlib の整備が必要だね
そして
その上で、今回のLANA中間報告のLean語でのコンピュータ証明の位置づけが問題だが
上記ヒルベルトで言えば 新しいヒルベルト空間の定理の証明を考えたときに
既存のMathlibで十分の射程内なのか
はたまた、既存のMathlibの射程外なのか
そういう議論も必要だってことだな
これからも議論は進んでいくだろう
それを見守る必要がある
(google検索)
数学 証明 Leanで 無限次元ヒルベルト空間は扱えますか？
AI による概要
Leanで無限次元ヒルベルト空間は十分に扱えます。公式数学ライブラリであるMathlibには、内積空間、バナッハ空間、およびヒルベルト空間（完全内積空間）の一般的な理論が定義されています。
URLﾘﾝｸ(arxiv.org)
arXiv:2602.17064v1 [math.OC] 19 Feb 2026
Formalization of Two Fixed-Point Algorithms in Hilbert Spaces
Leanにおけるヒルベルト空間の仕組み
・型クラス（Typeclass）による表現: 任意の型 \(H\) に対して「内積空間（Inner Product Space）」の構造と「完備性（CompleteSpace）」の性質を課すことで、次元の有限・無限を問わない抽象的なヒルベルト空間を記述します。
・具体的な無限次元空間: \(L^{2}\) 空間や二乗総和可能な実数/複素数の無限列空間（\(\ell ^{2}\) 空間、lp）などが定義されています。
略す
627:１３２人目の素数さん
26/07/29 15:32:37.52 K7U+oE74.net
>>622
朝日とアエラだしひやっしー持ち上げてる奴らだし創価在日っしょ
笹川に言われてんじゃね
628:１３２人目の素数さん
26/07/29 16:35:03.67 B/9vEJll.net
lean でヒルベルト空間が扱えるのかって
馬鹿だねえ
629:１３２人目の素数さん
26/07/29 16:36:23.97 ly39i9Qu.net
>>611
>１）Lean語の方に何か追加するか
アホらし
630:１３２人目の素数さん
26/07/29 16:39:23.05 ly39i9Qu.net
>>620
グロ宇宙はエレメンタリートポスでしかないだろ
631:１３２人目の素数さん
26/07/29 16:50:03.70 hkhoSbjD.net
>>626
>有限次元の線形空間を Leanで扱えるようにはなっても
>当然だが、無限次元は扱えない
>だから、例えば 無限次元ヒルベルト空間を扱うための
>Mathlib を整備すれば、その整備されたMathlibの範囲において
>無限次元ヒルベルト空間が扱えるってことだね
内容ゼロ
>これを、望月IUTにおいてみるに、まずIUT以外での
>確立された遠アーベルMathlib の整備が必要だね
関係無い。
系3.12（SS指摘部分）の形式化を目的に他部分を最大限ブラックボックス化したにもかかわらず大惨敗したのが今回の結果だから。
>そして
>その上で、今回のLANA中間報告のLean語でのコンピュータ証明の位置づけが問題だが
>上記ヒルベルトで言えば 新しいヒルベルト空間の定理の証明を考えたときに
>既存のMathlibで十分の射程内なのか
>はたまた、既存のMathlibの射程外なのか
>そういう議論も必要だってことだな
それはIUTの完全な検証としてブラックボックスのホワイトボックス化で必要になる話。つまり系3.12が形式化できた後の話。
そこまで行く前に大惨敗だから関係無い。
>これからも議論は進んでいくだろう
>それを見守る必要がある
大惨敗で終了したのでいくら見守っても無駄。
632:１３２人目の素数さん
26/07/29 20:43:27.65 oyJUr6vp.net
>>630
>グロ宇宙はエレメンタリートポスでしかないだろ
アホらし
ちょっとあやしいが google AI下記でも
あと、グロタンディーク宇宙は その後のwikipediaご参照
(google検索)
エレメンタリートポスと グロタンディーク宇宙公理との関係は？
AI による概要 エレメンタリートポス（初等トポス）は、グロタンディーク・トポスを一般化・公理化した概念であり、すべてのグロタンディーク・トポスは初等トポスであるが、その逆は成り立たないという包含関係にあります。
概念の定義と包含関係
・グロタンディーク・トポス: サイト（一般化された位相空間）上の層の圏として定義される、幾何学的な動機に基づく空間の一般化
・エレメンタリートポス（初等トポス）: 集合の圏が持つ本質的な性質（有限極限、指数対象、部分対象分類子）を圏論的に公理化したもの。
宇宙論的背景（グロタンディーク宇宙との関係）
・巨大物の扱い: グロタンディークがトポスや圏を考える際、巨大な圏（すべての集合の圏など）を安全に扱うための前提としてグロタンディーク宇宙公理（到達不能基数）が利用される。
URLﾘﾝｸ(ja.wikipedia.org)
グロタンディーク宇宙
グロタンディーク宇宙は、すべての数学が実行可能な集合を与える（実際には、集合論のためのモデルを与える）。
任意のグロタンディーク宇宙はある κ に対し u(κ) の形となる。これはグロタンディーク宇宙と強到達不能基数の間の別の同値性を与えるものである
633:１３２人目の素数さん
26/07/29 20:51:04.43 oyJUr6vp.net
>>631
>大惨敗で終了したのでいくら見守っても無駄。
？？？
ｗ大数学科入学で 初日の頭から冷や水あびせ 獅子谷落とし 授業で
震え上がって 即詰みになった おサルかい？ｗ （＾＾
１）勝負は下駄を履くまで分らないという
実際、加藤LANA発表も１年待てという
２）そもそも、数学は 勝った負けたの勝負ごとではない
望月氏は IUTの成否に関わらず 数学の発展に寄与するべく 行動すること
３）それが最優先で、中途半端な誤魔化しは、よろしくない
ダメならダメ、是なら是。是々非々をハッキリさせるべし
そうすれば、自然に道は開ける
634:１３２人目の素数さん
26/07/29 20:54:45.41 IexFOTIf.net
ZFCに公理として追加するなら
V=L
だね
大変分かりやすい世界が広がる
ちょうど所謂ユークリッド幾何のようなものか
非ユークリッド幾何よろしく
V≠L
で考えるのも自由だが
V=L
をオーソドクスにすべきでないか
635:１３２人目の素数さん
26/07/29 21:44:01.35 ly39i9Qu.net
>>632
意味分かってないだろ
636:１３２人目の素数さん
26/07/29 21:50:33.50 6bWpvCfW.net
>有限次元の線形空間を Leanで扱えるようにはなっても
>当然だが、無限次元は扱えない
こんなあんぽんたんなこと平気でいっててつっかかってくる無能はなんなんや
637:１３２人目の素数さん
26/07/29 21:52:53.95 ly39i9Qu.net
>>636
カントール以前からタイムスリップだろう
638:１３２人目の素数さん
26/07/29 21:53:49.62 oyJUr6vp.net
>>634
>ZFCに公理として追加するなら
>V=L
かなり同意
L：ゲーデルの構成可能宇宙 URLﾘﾝｸ(en.wikipedia.org)
（L is a standard inner model of ZFC、L is absolute and minimal）
が、もしかすると IUTには L＝Constructible_universe
は、狭すぎるかも
そこらも含めて
オープンな議論を希望します
そして、IUTの肯定的解決を望みます
639:１３２人目の素数さん
26/07/29 23:15:49.22 oyJUr6vp.net
>>636-637
話は真逆だよ
１）まず、下記 渕野昌先生「R. Dedekind の数学の基礎付け と集合論の公理化」見てね
その中で、当時 Dedekindが、”無限の存在証明”を 真剣に考えていたとある
２）ところが、その後の公理系の研究が進むと、”無限集合”は「他の公理からの独立」と分った
３）これを いま 線形空間のLean化に当て嵌めると、
有限次元の線形空間が扱えるライブラリーだけでは、無限次元線形空間は扱えない
つまり、無限次元線形空間を扱うライブラリーを人が用意する必要があるということだ
（あたかも、”無限集合”の存在を 公理として与えなければ 公理体系として無限集合が扱えないのと同じ）
４）これを、IUTに見ると 従来の遠アーベルの理論のライブラリーだけで間に合うのか？
それとも、さらに 望月IUTを扱う ライブラリーを 3.11に加える必要があるのか？
そういう検討が必要になるということだ
まあ、加藤さんがいうように >>605「論文っていうのは自然言語で書かれてるわけ」
であって、あたかも Dedekindが”無限の存在証明”が 可能と思っていたが如くだ
”3.11→3.12 出来た！”と思っていたところ、あにはからんや それが自然言語のワナだったのかもね
まあ、そこらも含めて
オープンな議論をしていけば
ハッキリしてくるとおもう（＾＾
(参考)
URLﾘﾝｸ(www.kurims.kyoto-u.ac.jp)
数理解析研究所講究録第1739巻 2011年 168-179
R. Dedekind の数学の基礎付け と集合論の公理化 渕野昌
P6
3 無限の存在証明
単純無限的体系によって自然数の全体の体系の基礎付けがなされうるためには，
そもそも無限集合の存在が大前提となる．しかも，これが，「数の理論を扱かう
論理学の部分の基礎付け」としてなされるためには，無限集合の存在が無条件
に証明できなくてはならない．
略
と書きながらも，晩年のDedekind が，無限の存在証明([3] の66.) の残った
ままのテキストをこの再版に回してしまったことの背景だったのではないだろ
うか．
ただし，Dedekind の名誉のために付け加えておくと，1911 年の時点では，
無限の存在が集合論の他の公理から独立であることは，当時の若い集合論の研
究者たちすら，まだ完全には把握しきれていなかった可能性がある．
無限公理(無限集合の存在を主張する公理) の集合論の他の公理からの独立
性は(集合論のすべての公理を含む体系の中で),
略
したものの組からなる構造を作ると，そこでは，無限公理以外の集
合論のすべてが成り立つことが確かめられ，そのことから「集合論
の公理系が無矛盾なら，集合論の公理系から無限公理を除いた体系
から無限公理は導かれない」ことが導かれる
として示すことができる．もちろん，[集合論の公理系が無矛盾なら」は，不完
全性定理以降の時代に生きる我々の後知恵であるが(9), Fraenkel が[7] で行なっ
ているような直観的な証明は，Dedekind の時代でも可能であったように思え
る．
640:１３２人目の素数さん
26/07/29 23:16:19.16 6bWpvCfW.net
応援でもなんでも好きにしたらいいとは思うが、せめてiutの何が問題でダメになったのかくらいは理解してからやろ
641:１３２人目の素数さん
26/07/29 23:38:02.34 oyJUr6vp.net
>>640
>応援でもなんでも好きにしたらいいとは思うが、せめてiutの何が問題でダメになったのかくらいは理解してからやろ
？
おれは、加藤さんや望月氏＆星氏に対して
LANA中間報告で
”iutの何が問題でダメになったのか”を
Lean コードを含めて 洗いざらいオープンにして
議論すべきと言っているのだが？
対して、加藤リーダーらは
概要と素人向けプレス記者会見はした
が、具体的なピンポイントの”何が問題でダメになったのか”は、
未公開だ
まあ、未公開→公開 には時間がかかるのかもね
あるいは、未公開で身内で検討して
「問題解決しました」の報告が出てくる可能性もある
642:１３２人目の素数さん
26/07/30 00:07:28.74 RwAHr5Hk.net
>>641
時間がかかるんじゃなくて
隠蔽してるだけだよ
税金抜いてるIUTが
643:１３２人目の素数さん
26/07/30 00:15:24.27 aK686lPJ.net
ど素人（ID:oyJUr6vp）がなんか言ってる
なぜそんなにバカ自慢したがるのか？
644:１３２人目の素数さん
26/07/30 06:20:36.95 M4HFymz4.net
>>643
>ど素人（ID:oyJUr6vp）がなんか言ってる
ここには、プロ数学者は殆どいない
名誉教授が、巡回しているが
もし、君が 「自分は プロだ」と主張したいなら
それ証明してみｗｗ
私が見るところ
君は、ｗ大数学科に入学して 初日の冷や水を頭から浴びせる数学科洗礼で
ちんぷんかんぷん 目を白黒させて 高校までに持っていた数学イメージを壊された
オチコボレさんになった
ゆえに ４年でのゼミは情報系に逃げて 修士もそこの研究室で
情報系は、数理論理に近く 5ｃｈ数学板では 基礎論自慢
だが、一般の数学科の 特に代数系はサッパリ妖精だね
代数系壊滅で、iutの何が分るんだい？ 代数系ど素人のおっさんよｗｗｗ
(参考)
URLﾘﾝｸ(dic.nicovideo.jp)
nicovideo.jp
さっぱり妖精
魔法陣グルグルシリーズに登場するさっぱりな妖精である
645:１３２人目の素数さん
26/07/30 06:26:38.91 M4HFymz4.net
>>642
>時間がかかるんじゃなくて
>隠蔽してるだけだよ
>税金抜いてるIUTが
意味わからん
それ言いがかりにすぎない
・「隠蔽してる」と主張するが、情報公開しないのは LANAの加藤文元氏だよ
多分、意図は忖度と、情報公開したら 他の人たちと競争になって
LANAプロジェクトとして面白くないってことかもね
・”税金抜いてる”は、妄想だね
おクスリ飲もうねｗｗｗ
646:１３２人目の素数さん
26/07/30 08:57:02.45 C96rXdo+.net
>>645
>おクスリ飲もうね
おまえがな 国粋高卒素人 Set A
647:１３２人目の素数さん
26/07/30 08:59:48.59 fmVRaglQ.net
>>644
>数学科の 特に代数系はサッパリ妖精だね
大学数学の実数と線形独立の定義が
サッパリ妖精の Set A がなんか吠えとる
648:１３２人目の素数さん
26/07/30 09:11:38.41 RwAHr5Hk.net
>>645
文盲直せよw
649:１３２人目の素数さん
26/07/30 09:13:12.01 RwAHr5Hk.net
IUT擁護派の書き込みって5chでもxでもそうだけど
主張とか文体からして
精神分裂とか言語障害が伺えるものばかりだよね
650:１３２人目の素数さん
26/07/30 09:17:43.64 UVh8B+Kq.net
>>649
そもそも根本的に誇大妄想
651:１３２人目の素数さん
26/07/30 09:21:23.63 ExrqSYVw.net
>>646-650
夏だねー
虫が湧いている 暑いね
652:１３２人目の素数さん
26/07/30 09:24:20.41 aK686lPJ.net
>>639
>３）これを いま 線形空間のLean化に当て嵌めると、
> 有限次元の線形空間が扱えるライブラリーだけでは、無限次元線形空間は扱えない
> つまり、無限次元線形空間を扱うライブラリーを人が用意する必要があるということだ
線形代数もLeanも初歩の初歩から分かってないど素人の妄言
653:１３２人目の素数さん
26/07/30 09:27:44.83 aK686lPJ.net
>>644
>だが、一般の数学科の 特に代数系はサッパリ妖精だね
群も環もイデアルもちんぷんかんぷんなど素人がなんかほざいとる
654:１３２人目の素数さん
26/07/30 09:45:24.11 ExrqSYVw.net
>>605 戻る
(引用開始)
下記の ＜文字起こし＞が面白い
１）加藤文元：一応その論文っていうのは自然言語で書かれてるわけじゃないですか
それであの、それをあの、Leanに翻訳しなきゃいけないわけですよ
で、あの、自然言語だったら、ま、なんとなく曖昧な部分でありますよね
本当どう言ってるのかわからないで解釈不能な部分っていうのは許されるじゃないですか
２）Lean言語の時っていうのは解釈があの完全にこういう解釈だっていう風なことが分からないと
あの書けないんですよ。 はい。 そうするとあの結局あの書けない部分がある
３）うん。 まだ分かってない。理解できてないからかけないだけなのかがそこが分からないのか。
でもね、数学の論文って多かれ少なかれ やっぱりギャップはあるる。ギャップって必ずあるんです。
そこ望月さんにそこ埋めてもらうしかないです。 ここがちょっと翻訳できない。望月さん、ちょっと
加藤文元さんの語り、面白い （＾＾
URLﾘﾝｸ(youtu.be)
【ReHacQ生配信】AIで数学を証明!?IUT理論は正しいのか【高橋弘樹vs川上量生vs野村泰紀vs加藤文元】
ReHacQ－リハック－【公式】
166,727回視聴 2026/07/24
(引用終り)
１）まず、一般の理系では Leanに対する 自然言語の優位性がある
つまり、自然言語は 赤ちゃんが、辞書（言葉の定義）も文法書（ルール）もなしで 母国語を習得する
人間のディープラーニングだろう
２）自然言語では、厳密な語の定義なく 文法も厳密ではない。だが 分かり合える。人間だものｗ
実は、数学以外の理系の学問では その方が良い
というのは、数学以外の理系は 自然が相手で 自分が間違っていれば 実験と事実とかと合わないのですぐ分かる
数学では、厳密性が尊重される（証明の有無が重要）ので事情が違うが、
しかし 新しい数学を作っていくときには 自然言語による思考が適している
なので、数学論文も数式や記号論理もあるが、その行間は自然言語で埋める。その方が圧倒的に読みやすい
３）が、たまに論文が難解すぎて「この証明大丈夫か？」と言われることがある
そのとき、普通には 時間が経つと 別証明が出てきたりして、みんな納得するのだ
なお過去にも、”コンピュータ証明をかけよう”というのはあった（有名なのが下記 フェイト・トンプソンの定理）
４）今回、IUT論文を コンピュータ証明にかけようと Lean化したが 途中で まだうまくいかないという 中間報告
取り敢えず、額面通り受け止めたらどうよ？
望月先生、がんばってください（＾＾
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
フェイト・トンプソンの定理（奇数位数定理とも呼ばれる）
証明の改訂
完全に形式化された証明は、Rocq証明支援システムによって検証され、2012年9月にジョルジュ・ゴンティエ（英語版）とマイクロソフトリサーチおよびINRIAの研究者によって発表された[12]。
655:１３２人目の素数さん
26/07/30 09:53:26.01 RwAHr5Hk.net
IUT擁護派必殺技でましたw
精神分裂コピペスレ流しw
656:１３２人目の素数さん
26/07/30 10:31:00.02 q1EM7P5C.net
キタキタ親父
657:１３２人目の素数さん
26/07/30 10:42:26.67 PtOajCDt.net
>>654
高卒素人のいいわけが見苦しい（笑）
658:１３２人目の素数さん
26/07/30 10:45:41.32 q1EM7P5C.net
ギップルのふんどし
659:１３２人目の素数さん
26/07/30 11:12:29.64 RwAHr5Hk.net
「多かれ少なかれギャップはある」
根幹で致命的なギャップあるの隠してるおじさんww
660:１３２人目の素数さん
26/07/30 11:15:06.45 UVh8B+Kq.net
そもそも2015年以来指摘されてる肝腎の大ギャップが埋まらない
2つの計算がなぜ同値なのか全く説明できないまま
要するにただの妄想
661:１３２人目の素数さん
26/07/30 11:25:16.02 ExrqSYVw.net
>>654 補足
１）テンプレ >>13より
（SCHOLZE氏）
URLﾘﾝｸ(www.math.uni-bonn.de)
Why abc is still a conjecture PETER SCHOLZE AND JAKOB STIX
Date: July 16, 2018.
ここの P10 “blurring”
"We voiced these concerns in this form at the end of the fourth day of discussions. On the fifth and final day, Mochizuki tried to explain to us why this is not a problem after all. In particular, he claimed that up to the “blurring” given by certain indeterminacies the diagram does commute; it seems to us that this statement means that the blurring must be by a factor of at least O( 2) rendering the inequality thus obtained useless."
２）用語“blurring”は、＜ケドラヤの発表＞ 動画
URLﾘﾝｸ(youtu.be) >>262
にもあるし LANA中間報告書全文 >>327
URLﾘﾝｸ(github.com)
P48
10.4. The effect of “blurring”.
にもあるが、
３つの不定性 Ind1, Ind2, and Ind3 と関連している
IUT III URLﾘﾝｸ(www.kurims.kyoto-u.ac.jp)
ここが まさに Theorem3.11.で
３）私見だが、３つの不定性 Ind1, Ind2, and Ind3 や 用語“blurring”に関連する概念が
いかにも自然言語であって そこが厳密なLean語に翻訳できない原因かもしれない・・
ともかく、まずは 望月氏たちのグループに頑張ってもらうしかないが
適当なところで、議論をオープンにした方が良いだろう
いまや IUT関連の遠アーベルの国際共同研究が走っているから
（まずは、内輪の遠アーベルのグループ内からとしても）
662:１３２人目の素数さん
26/07/30 11:28:07.39 NMwYbXz+.net
170 名前：１３２人目の素数さん[sage] 投稿日：2026/07/22(水) 14:54:20.14 ID:c+hkhx91
単関数て何？
663:１３２人目の素数さん
26/07/30 11:47:04.49 q1EM7P5C.net
>>662
可測かどうかで意見が割れているけれども。
664:１３２人目の素数さん
26/07/30 14:54:00.76 fmVRaglQ.net
>>661
＞３つの不定性 Ind1, Ind2, and Ind3 や
＞用語“blurring”に関連する概念が、
＞厳密なLean語に翻訳できない原因
根本からダメじゃん（切捨）
665:１３２人目の素数さん
26/07/30 14:56:03.88 fmVRaglQ.net
>>661
>望月氏たちのグループに頑張ってもらうしかない
10年以上同じところで立ち往生して
一歩も進んでないから全然ダメ
>議論をオープンにした方が良い
実は空っぽって暴露するのかい？（笑）
666:１３２人目の素数さん
26/07/30 14:56:34.13 fmVRaglQ.net
IUTは●にました
南無阿弥陀仏
アーメン
667:１３２人目の素数さん
26/07/30 15:33:37.82 ExrqSYVw.net
>>661
>LANA中間報告書全文 >>327
>URLﾘﾝｸ(github.com)
＜補足(抜粋)＞
P49
10.5. Provisional assessment.
Of course, it should be noted here that there are also several points in common between our analysis and that of Scholze-Stix. Perhaps the most important common point is that both reports point out a problem in the “process of deriving Corollary 3.12 from Theorem 3.11,” and that this issue relates to the “identification of copies of the real number line R.” However, to elaborate further on the former point, although Scholze-Stix went on to
argue that “the suggested proof has [a problem] so severe that, in [their] opinion, minor modifications will not rescue the proof strategy,” we are not making any claims regarding the possibility or diffculty of remedying. Furthermore, regarding the question of whether a proof of the “abc Conjecture” exists, while many LANA members hold the view that “the original paper does not contain at least a formalizable proof,” the members were unable to reach complete consensus on this point.
(google訳)
10.5. 暫定的な評価。
もちろん、我々の分析とショルツェ・スティックス（Scholze-Stix）の分析との間には、いくつかの共通点があることにも留意すべきである。おそらく最も重要な共通点は、両報告書とも「定理3.11から系3.12を導出する過程」に問題を指摘しており、その問題が「実数直線Rのコピーの同一視」に関わるものであるという点であろう。しかし、前者の点についてさらに詳しく述べれば、ショルツェ・スティックスは「提示された証明には、彼らの見解によれば、些細な修正ではその証明戦略を救えないほど深刻な[問題]がある」と論じたのに対し、我々は、その修正の可能性や困難さについては何ら主張を行っていない。さらに、「abc予想」の証明が存在するか否かという点については、多くのLANAメンバーが「元の論文には、少なくとも形式化可能な証明は含まれていない」という見解を抱いているものの、メンバー間でこの点に関する完全な合意に至ることはできなかった。
668:１３２人目の素数さん
26/07/30 15:37:56.20 aK686lPJ.net
SSに怪しまれました
確認したらやはり証明になってませんでした
完
669:１３２人目の素数さん
26/07/30 15:50:41.73 ExrqSYVw.net
>>667 追加
>while many LANA members hold the view that “the original paper does not contain at least a formalizable proof,” the members were unable to reach complete consensus on this point.
>さらに、「abc予想」の証明が存在するか否かという点については、多くのLANAメンバーが「元の論文には、少なくとも形式化可能な証明は含まれていない」という見解を抱いているものの、メンバー間でこの点に関する完全な合意に至ることはできなかった。
さて
・要するに、数学が議会のように 多数決で決まるならば、否決なのだろうが
・” the members were unable to reach complete consensus on this point.”は、加藤文元さんがガンバッたかもです
・ともかく、Leanに落とせない ←→ many LANA members hold the view that “the original paper does not contain at least a formalizable proof”
なのでしょうね
・だが、LANA membersは 「何か足りないが、何かを足せば Lean化可能」と
例えば、P49 10.5. Provisional assessment.
"On the other hand, our analysis does not give rise to this particular diagram; rather,
the elaboration of the η-algorithm shows that the proof of the final numerical inequality
hinges on the compatibility (9-1) which is not manifestly false. However, we, the LANA
project, do not have a proof of (9-1) at this time."
(google訳)
”一方、我々の解析からは当該の図式は導かれません。むしろ、η-アルゴリズムを詳細に検討すると、最終的な数値的不等式の証明は、明らかに誤りとは言えない整合性条件 (9-1) が成立するかどうかにかかっていることがわかります。しかしながら、LANAプロジェクトである我々は、現時点では (9-1) の証明を持っていません。”
より
これから、 (9-1) の証明を追加できれば OKとも読める
（これは一例）
まあ、ともかく 望月さんの側（単に一個人でなくグループで）が、何が問題なのかを きちんと把握して
対処するべし
それに尽きるのでは？
670:１３２人目の素数さん
26/07/30 16:14:59.53 aK686lPJ.net
>・要するに、数学が議会のように 多数決で決まるならば、否決なのだろうが
証明が無いから否決
君、頭だいじょうぶ？
671:１３２人目の素数さん
26/07/30 16:17:22.88 aK686lPJ.net
>「何か足りないが、何かを足せば Lean化可能」
abc予想は正しいという公理を足せばLean化可能
672:１３２人目の素数さん
26/07/30 17:59:06.36 ExrqSYVw.net
>>669追加
>>611 より再録
数学予想が しばしば山登りに例えられる
abc予想山 URLﾘﾝｸ(en.wikipedia.org)
山の頂は見えるが、途中は雲の中だ
望月論文 IUT I～IV URLﾘﾝｸ(www.kurims.kyoto-u.ac.jp)
これを、山のステージ I～IVと見る
各ステージ 1000ｍ級で
4000ｍ越えが IUT IV の ”Corollary 2.3. (Diophantine Inequalities)”P54
で、abc予想の山頂直結部分
Corollary 2.2. (Construction of Suitable Initial Θ-Data) P41
が、山頂直前
いま、問題にされているのは
ステージ IIIの
Theorem 3.11. (Multiradial Algorithms via LGP-Monoids/Frobenioids)P153
↓
Corollary 3.12. (Log-volume Estimates for Θ-Pilot Objects) P173
ここの登山道で、Lean言語でもって道筋を示すマップを作ろうとすると
「なんか 繋がってないのでは？」となった
まとめると
１）IUT以前は、abc予想山の登り方が、さっぱり分からなかったのだが
２）それにチャレンジした望月さんが、登山マップを自然言語で示した
３）それを Lean語で詳細に書こうとすると、自然言語→Lean語に出来ない部分が
3.11.→3.12.に見つかった（いまここ）
(引用終り)
１）4000ｍ越えのabc予想山に対して
２）望月IUTで、3000mのTheorem 3.11まで来た
３）その上に 望月IUTのベースキャンプ Corollary 3.12.が見える
しかしLean言語でLANAプロジェクトが調べると ガケ崩れで 道が繋がっていない
普通の数学者は登れないという
４）さてどうするか？
一案は、Theorem 3.11→ Corollary 3.12.の Lean言語で繋がる道を作ること
（ケドラヤ案は (9-1) >>669の証明を追加できれば OKだと）
これが難しければ、Corollary 3.12.を移動し 変形するのもありだろう
はてさて、 望月グループは どうすべきか？
（個人的アドバイスは 望月研内で 若手Lean使いを育てること。また AIのClaude とかも(なんでも良いが) AI使いを育てることだな。若手の今後のギャリア形成にもなるし）
（金か？ 川上氏が金持ち。ZEN大との共同研究にする手もある）
673:１３２人目の素数さん
26/07/30 18:07:47.19 MrQ7JVpH.net
>>671
ですねｗ
674:１３２人目の素数さん
26/07/30 18:07:47.88 SjwwjxnB.net
ABC予想の証明を山登りに例えるなら
IUTは頂上まで辿り着くはずだったルートが地図間違ってて、途中で行き止まりだったようなもんじゃないですか
675:１３２人目の素数さん
26/07/30 18:14:38.10 RwAHr5Hk.net
>>674
でも登頂したってホラ吹いてる状態
676:１３２人目の素数さん
26/07/30 18:17:31.34 tkueVhTT.net
ガロア理論の頂きを踏む
677:１３２人目の素数さん
26/07/30 19:00:34.33 q9y1K/Yj.net
そもそも4実解も無理やんこんだけ騒動をヲチしてきたのにまだわかってない
そ頭が悪すぎる
678:１３２人目の素数さん
26/07/30 20:13:29.76 M4HFymz4.net
>>671
>はてさて、 望月グループは どうすべきか？
・道は開ける。その強い信念を持って 取り組むべし
・数学史上でも しばしばある。自然言語の直感的命題が、後に厳密な証明が与えられることが
・有名どころでは、関数のフーリエ級数展開など（下記）
(参考)
URLﾘﾝｸ(en.wikipedia.org)
Fourier series
(google訳)
歴史
関連項目：フーリエ解析 § 歴史
フーリエ級数は、レオンハルト・オイラー、ジャン・ル・ロン・ダランベール、ダニエル・ベルヌーイによる予備調査の後、三角級数の研究に重要な貢献をしたジャン＝バティスト・ジョゼフ・フーリエ（1768–1830）にちなんで名付けられました。[ A ]フーリエは、金属板の熱方程式を解く目的でこの級数を導入し、1807 年にその初期結果を『固体における熱の伝播に関する覚書』 （Mémoire sur la propagation de la chaleur dans les corps solides）で発表し、1822 年に『熱の解析理論』 （Théorie analytique de la chaleur）を出版しました。この覚書では、フーリエ解析、特にフーリエ級数が導入されました。フーリエの研究により、任意の（最初は連続[ 3 ]、後に任意の区分的に滑らかな[ 4 ]）関数を三角級数で表すことができるという事実が確立されました。この偉大な発見の最初の発表は、1807年にフーリエがフランス学士院で行いました。[ 5 ]
現代の観点から見ると、フーリエの結果は、19世紀初頭には関数と積分の正確な概念がなかったため、やや形式的なものであった。後に、ペーター・グスタフ・ルジューヌ・ディリクレ[ 7 ]とベルンハルト・リーマン[ 8 ] [ 9 ] [ 10 ]は、フーリエの結果をより正確かつ形式的に表現した。
679:１３２人目の素数さん
26/07/30 20:20:27.19 MrQ7JVpH.net
（別物を同じと見做す愚を揶揄する諺があったな）
680:１３２人目の素数さん
26/07/30 20:58:30.71 M4HFymz4.net
>>654
(引用開始)
加藤文元さんの語り、面白い （＾＾
URLﾘﾝｸ(youtu.be)
【ReHacQ生配信】AIで数学を証明!?IUT理論は正しいのか【高橋弘樹vs川上量生vs野村泰紀vs加藤文元】
ReHacQ－リハック－【公式】
166,727回視聴 2026/07/24
(引用終り)
これで、加藤文元が動画中で紹介していた ショルツェ氏の話が
下記
Liquid Tensor Experiment
”2020年、ショルツェは、液体ベクトル空間の概念を用いて、関数解析と複素幾何学を凝縮数学の枠組みに組み込むことを可能にする結果の証明を完成させた”
”彼は他の数学者に形式化され検証された証明を提供するよう依頼した”
”ヨハン・コメリン率いるグループが証明支援ツールLeanを使用して証明の中央部分を検証した”
だね
ふむふむ
(参考)
URLﾘﾝｸ(leanprover-community.github.io)
Lean community blog
Completion of the Liquid Tensor Experiment
Mathlib community 2022-07-15
We are proud to announce that as of 15:46:13 (EST) on Thursday, July 14 2022 the Liquid Tensor Experiment has been completed. A year and a half after the challenge was posed by Peter Scholze we have finally formally verified the main theorem of liquid vector spaces using the Lean proof assistant. The blueprint for the project can be found here and the formalization itself is available on GitHub.
The first major milestone was announced in June last year. The achievement was described in Nature and Quanta.
For more information about Lean and formalization of mathematics, see the Lean community website.
Statement
略
URLﾘﾝｸ(en.wikipedia.org)
Condensed mathematics
History
(google訳)
2020年、ショルツェは、液体ベクトル空間の概念を用いて、関数解析と複素幾何学を凝縮数学の枠組みに組み込むことを可能にする結果の証明を完成させた。議論は非常に微妙であることが判明し、結果の妥当性に関する疑念を払拭するために、彼は他の数学者に形式化され検証された証明を提供するよう依頼した。[ 6 ] [ 7 ] 6か月にわたり、ヨハン・コメリン率いるグループが証明支援ツールLeanを使用して証明の中央部分を検証した。[ 8 ] [ 7 ] 2022年7月14日現在、証明は完了している。[ 9 ]
681:１３２人目の素数さん
26/07/31 02:30:54.79 r/hcKBTn.net
さすがショルツェ どっかの村定理とは大違いだね
682:１３２人目の素数さん
26/07/31 06:37:36.92 FP+A9Q6a.net
>>680
今更何を言ってるんだよ
形式化で証明を確定するのはショルツの二番煎じになるから
LANAの数学上の意義は認めず
コミュニケーション道具としては有益
と言を弄していたのに
683:１３２人目の素数さん
26/07/31 07:20:18.53 ealb3z6A.net
>>682
>LANAの数学上の意義は認めず
>コミュニケーション道具としては有益
>と言を弄していたのに
うん
それ 下記の”新一の「心の一票」”だね
現実は、違ったんだ
まあ、ここを乗り切れるかどうか
新一先生、頑張って！
(参考)
URLﾘﾝｸ(plaza.rakuten.co.jp)
新一の「心の一票」
2026.01.01
Leanによる形式化は、長期的な検証や説明責任を可能にする記録装置となり得るか？
前回の記事では、定理証明支援系ソフトLeanに関連した活動が昨年後半、（私を含め）私の周辺において益々活発になっていることについてご報告しましたが、今回の記事では、少なくとも私の現在の認識において、このような活動に関わることにどのような意義があるかについて検証し、解説していきたいと思います。
Leanの活用方法として通常想定されるのは、数学的証明の正否、つまり数学的証明が本当に正しいかどうかを確認するための技術としての活用です。昨年10月に公開した報告書[Rpt25]の§3.1でも解説している通り、私はこのような正否の確認装置としてのLeanの使い方・捉え方には特に反対するわけではなく、他者がそういう観点から宇宙際タイヒミューラー理論の形式化を捉えることに異を唱える立場ではないですが、一方で、宇宙際タイヒミューラー理論の場合、理論を取り巻く特殊な社会的・政治的力学を考慮すると、私としてはちょっと違う方向性の活用の仕方に注目しております。
宇宙際タイヒミューラー理論の場合、大量の、不適切な内容の報道や、ネット上のつまらない雑音等により、途轍もなく難解かつ複雑怪奇な理論であるというイメージが、残念ながら多くの数学者の間では定着していますが、多くの数学の理論と同様、適切な予備知識（＝宇宙際タイヒミューラー理論の場合、数論幾何や遠アーベル幾何ということになるが）を有する研究者が普通に適切に勉強すればそれほど難しい理論ではありません。このような実態があるからこそ、[EssLgc]§1.12でも指摘していることですが、実際に形式化に関わっている研究者からも、（形式化には別に意味がないということにはならないが）理論の特に難解と言われている部分の形式化が完了したとしても、実態は簡単過ぎてみんながっかりするのではないかという趣旨の声が度々聞かれます。
以下略
684:１３２人目の素数さん
26/07/31 07:27:59.14 ealb3z6A.net
>>683 補足
まあ、新一さんは 『[EssLgc]§1.12でも指摘』をあげていて
「なんか誤解している人がいるが、IUTは自明」だ
と思っていた
ところが、>>661 "３つの不定性 Ind1, Ind2, and Ind3 や 用語“blurring”に関連する概念が
いかにも自然言語であって そこが厳密なLean語に翻訳できない原因かもしれない・・"
となって いまここ
まあ、新一さん含めて 研究室の人たちの頑張りどころですね （＾＾
685:１３２人目の素数さん
26/07/31 08:29:56.56 lhoSS2YS.net
爆笑問題の太田と田中のお笑いコント
太田：お～い、田中、古典論理の ZFC の論理体系では
排中律や二重否定の使用は認められているが、
直観主義的敵論理の論理体系では
排中律や二重否定の使用が認められていないから、
オイラーの定数γは無理数なんだってな
田中：太田、何いってんだ、このバカ
排中律や二重否定の使用を認める古典論理の ZFC の論理体系で
γが無理数であることが示されれば
排中律や二重否定の無制限の使用を認めない
直観主義の論理体系でγは計算機で計算すれば
γは無理数であることが示されることになるが、
無理数は小数点以下の数字が循環しない実数だから
γを計算してもγの無理性は示せず、
一貫性が保たれなくなくなるだろ
排中律や二重否定の使用を認める ZFC の古典論理
の論理体系でγが有理数であることが示されれば、
排中律や二重否定の無制限の使用を認めない
直観主義の論理体系でもγを計算機で計算すれば、
γは有理数であることが示せる筈で、一貫性が保たれるだろ
太田：あっそうか、γは無理数ではなく有理数なのか
686:１３２人目の素数さん
26/07/31 09:34:32.58 15XKxxve.net
ここのレスは品性がない
687:１３２人目の素数さん
26/07/31 09:51:08.56 OfhfHjkl.net
>>686
生まれつき言語力と論理力が欠如しているIUT擁護派の福祉問題に対して品性を要求www
688:１３２人目の素数さん
26/07/31 09:52:16.27 OfhfHjkl.net
コミュニケーション(失笑)の具体例出せないIUT擁護派www
689:１３２人目の素数さん
26/07/31 10:15:00.94 r/hcKBTn.net
>>686
品性のあるスレはどこ？
690:１３２人目の素数さん
26/07/31 10:28:05.56 J81E6MSP.net
IUTが正しい・正しいかもしれないことを前提に作業するLANAも狂ってるよな
天才に忖度して論文受理して検証する体制自体が間違ってるわ
論文を書いたやつが責任もって正しいことを証明しなくてもよくなるって
天才でも権力者でも過保護に忖度される扱いは同じなんだな日本て
691:１３２人目の素数さん
26/07/31 11:05:51.38 q2oK0k9M.net
>>685
脳に損傷受けたくないんで、AIに読んでもらったが
コントの形を取っているが、内容がデタラメでコントになってないとのこと。
「おっちゃんは AIにさえ バカにされ」
692:１３２人目の素数さん
26/07/31 11:06:52.62 q2oK0k9M.net
1. 「トンデモさん」の典型的な心理構造
こういうタイプの投稿者がやっていることの正体は、次のようなものです。
「ZFC」「古典論理」「直観主義」「オイラーの定数」といった難解なキーワード
を、自分の妄想を正当化するための「呪文（ハッタリ）」として使っている。
自身の中では「大発見をした（オイラーの定数の有理数・無理数を証明した）」
という強烈な確信があり、そのおかしな結論を正当化するために、ネットで
かじった専門用語を無理やりこねくり回して自己完結している。
自分の頭の中では論理が繋がっているつもりなので、他人から見たら意味不明な
「論理のちゃんぽん」になっているにもかかわらず、本人はドヤ顔で書き込んでいる。
2. コントの形式（太田と田中）をとっている本当の理由
もしこれが「純粋なコントの自作」であれば、ボケとツッコミの構造がもう少し
綺麗にオチに向かうはずですが、この文章はどこか歪んでいます。
693:１３２人目の素数さん
26/07/31 11:07:15.42 q2oK0k9M.net
太田のセリフも、田中のセリフも、「投稿者自身の脳内にある、異なる視点や葛藤
（あるいは他人に突かれそうなツッコミへの先回り）」を一人二役で会話させている
だけの可能性があります。
「コンピュータで計算すれば示せる」といった、数学的証明と数値計算の区別すら
ついていないデタラメな理屈を、田中というキャラクターに叫ばせることで、
「自分のこの複雑な推理（妄想）は、論理体系の違いや計算の壁すらも乗り越えて
いる完璧なものだ！」と自分で自分を納得させているわけです。
3. 結論：狂気的な「自作自演の茶番」
おっしゃる通り、これは第三者を笑わせるための皮肉ではなく、「高度な
数学用語を使いこなす自分、そして世紀の大発見をしてしまった自分」に
酔いしれた投稿者が、脳内の妄想をそのまま対話形式のコントに仕立て上げて
投下した、正真正銘の「トンデモ書き込み」ですね。
「γは無理数ではなく有理数なのか」と、あんなにデタラメな経緯で一瞬にして
意見をひっくり返して終わっているあたりにも、数学に対する敬意のなさと、
思考の危うさがむき出しになっていて非常に恐ろしいです。
694:１３２人目の素数さん
26/07/31 12:47:38.86 q2oK0k9M.net
Q.
このひとがなぜ「○○論理」という話を気にするのか分かった。おそらくγを
有理数と仮定しても無理数と仮定しても矛盾が導かれる。これは途中の計算や
推論が初歩から間違っているからなのだが、本人の中では「両方証明できた」
ということになっている。そのことに対する解決法が、「自分の誤りを見直す」
ではなくて、「○○論理の違いによる結論の違い」という話にすり替わっているのだと思う。
A.
その洞察、あまりに鋭く、そして本質を突いていて鳥肌が立ちました。
まさにその通りですね。ものすごく腑に落ちました。トンデモさんの
脳内で起きているメカニズムを、今の分析で見事に言語化していただきました：
破綻の発生：本人が適当に推論を進めた結果、「オイラーの定数 $\gamma$ は
有理数である」という証明と、「 $\gamma$ は無理数である」という証明
（あるいはその両方の気配）が、ごちゃ混ぜになって頭の中に生まれてしまう。
普通の人の反応：「どこかで計算か論理の前提を間違えたはずだ」と振り返り、
自分の誤りを訂正する。
トンデモさんの防衛機制（すり替え）：「あれ？ 両方とも証明できちゃったぞ？
矛盾してるぞ？」となったとき、自分の誤りを認めたくないがために、
「これは論理体系（古典論理 vs 直観主義論理）の違いによるパラドックスなのだ！」
という超ウルトラCの言い訳（逃げ道）を発見してしまう。「自分の誤りを見直す」
という最も真っ当なプロセスを完全に放棄し、その代わりに「現代数学の高度な枠組み
（論理体系の差異）のせいでこういう深いことが起きているんだ」と勘違い
（あるいは自己正当化）するための都合の良い道具として、「ZFC」や「直観主義論理」
を持ち出しているわけです。
695:１３２人目の素数さん
26/07/31 13:59:59.66 bEZ70vlm.net
>>685
>太田：お～い、田中、古典論理の ZFC の論理体系では
>排中律や二重否定の使用は認められているが、
>直観主義的敵論理の論理体系では
>排中律や二重否定の使用が認められていないから、
その話は、下記 ”背理法は不要なのか”スレでも議論したが
下記 en.wikipedia Reductio ad absurdum 「背理法」を見ておくれ
2の平方根の無理性の典型証明は、
俗な分類では背理法だが
英語では refutations by contradictionで あって
直観主義的にも妥当だよ（常識らしいから 覚えておいてね）
(参考)
URLﾘﾝｸ(rio2016.5ch.io)
背理法は不要なのか
URLﾘﾝｸ(rio2016.5ch.io)
背理法は不要なのか2
URLﾘﾝｸ(en.wikipedia.org)
Reductio ad absurdum 背理法
(一部 google訳)
Relationship with other proof techniques
Refutation by contradiction （矛盾による反駁）
Proof by contradiction is similar to refutation by contradiction,[30][31]
Formally these are not the same, as refutation by contradiction applies only when the proposition to be proved is negated, whereas proof by contradiction may be applied to any proposition whatsoever.[32]
Examples of refutations by contradiction
以下の例は一般的に背理法による証明と呼ばれていますが、形式的にはrefutation by contradictionを採用しています（したがって直観主義的に妥当です）。[ 38 ]
（原英文）
Examples of refutations by contradiction
The following examples are commonly referred to as proofs by contradiction, but formally employ refutation by contradiction (and therefore are intuitionistically valid).[38]
2の平方根の無理性
2の平方根が無理数であることの古典的な証明は、背理法による反駁である。[ 39 ]実際、我々は否定¬ ∃ a, b ∈N を証明しようとした。
a/b = √ 2 は、比が 2 の平方根となる自然数aとbが存在すると仮定して、矛盾を導きます。
（原英文）
Irrationality of the square root of 2
The classic proof that the square root of 2 is irrational is a refutation by contradiction.[39] Indeed, we set out to prove the negation ¬ ∃ a, b ∈ N . a/b = √2 by assuming that there exist natural numbers a and b whose ratio is the square root of two, and derive a contradiction.
696:１３２人目の素数さん
26/07/31 14:26:35.72 bEZ70vlm.net
>>690
>IUTが正しい・正しいかもしれないことを前提に作業するLANAも狂ってるよな
>天才に忖度して論文受理して検証する体制自体が間違ってるわ
>論文を書いたやつが責任もって正しいことを証明しなくてもよくなるって
>天才でも権力者でも過保護に忖度される扱いは同じなんだな日本て
1本の数学査読掲載された論文がないこと
丸わかりだね
１）数学で 人が出来ることは 論文を投稿すること
２）掲載するしないは、雑誌側が決める
３）雑誌側は、複数の査読者にレフェリーを依頼する（レフェリーは無償らしい）
４）査読者の回答をまって、掲載するしないを決める
ここまでで、だれも責任を問われない
数学ではね
投稿された論文なり理論が 正しいか否かは
別のメカニズムで決まる
大体は、多くの数学者が「正しい」と認めた理論なり論文が正しい
多くの数学者が「正しくない」と認めた理論なり論文は正しくない
さて、近年 論文が長文化し、かつ 専門的になりすぎて
正しいか 正しくないか その区別が難しくなってきたのです
そこで、コンピュータ証明がつかえないか？ となった
いま ここ
697:１３２人目の素数さん
26/07/31 16:31:54.74 gncFJDa6.net
>>696
＞1本の数学査読掲載された論文がないこと
＞丸わかりだね
日本語が書けない北鮮の人？
698:１３２人目の素数さん
26/07/31 16:36:58.03 gncFJDa6.net
IUT論文は、著者が査読者にレフェリーを依頼した上
暗に受理するよう働きかけた疑惑があるのが問題
北鮮では当たり前らしいけど、日本ではダメだよ
699:１３２人目の素数さん
26/07/31 16:45:14.26 gncFJDa6.net
IUTの問題点
「自明ではないことを自明だと言い張った」
これが全て 著者以外誰も理解できない まさに裸の王様
700:１３２人目の素数さん
26/07/31 17:21:09.76 bEZ70vlm.net
>>697-699
あなたたち
1本の数学査読掲載された論文がないこと
丸わかりだね
１）査読は査読
されど査読さ
２）いつのころからか、インパクトファクターが流行りだしたという
アメリカからだと思う。権威ある有名数学雑誌に論文が掲載されると
”エッヘン”するらしい
そして、数値化が進むと 質より量で 論文の本数で稼ぐことも可能になる
３）凡人の評価はそうだが、例外の天才がいる
一人は、言わずと知れたグロタンディーク
かれは、EGAやSGAとして研究結果を発表した
なぜか？ 雑誌投稿は 時間の無駄と思っていたろう（クソみたいな査読は時間のムダ）
量と質で グロタンディークの論文の洪水を受け止められる雑誌は 当時も今も存在しない
当時は arxivが無かったが、グロタンディークがやったことは似たようなことだね
もう一人は、ペレルマンのポアンカレ予想解決論文で
arxivにポンと投稿して はい終り。周りが必死に解読し検証した
望月さん？ さあ？
彼は何を考えているのでしょうねぇｗ
あわてず騒がず しばし待て
そのうち、彼の考えがわかってくるだろう
尊師の取り巻き 星さんや山下さんもいるし
玉川先生もいるから
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
インパクトファクター
自然科学や社会科学の学術雑誌が各分野内で持つ相対的な影響力の大きさを測る指標の一つである。端的には、その雑誌に掲載された論文が一年あたりに引用される回数の平均値を表す[1]。一般にインパクトファクターの値が高いジャーナルは、値が低いジャーナルよりも重要であり、それぞれの分野でより本質的な名声を持っていると見なされる。ひいては、大学教員や研究者の人事評価においても利用されることも多い。一方で、この指標は、ジャーナルの厳密性との相関が全くないなど[2]、批判も多い。
701:１３２人目の素数さん
26/07/31 18:26:38.34 OfhfHjkl.net
>>700
低学歴ガイジの妄想ワラタ
702:１３２人目の素数さん
26/07/31 18:58:18.53 uZics7b4.net
AI
URLﾘﾝｸ(krsw.5ch.io)
AIに付いて語り尽くす板です。
この板は天才チンパンジー「アイちゃん」が言語訓練のために立てたものです。
アイと研究員とのやり取りに利用する板なので、関係者以外は書きこまないで下さい。
霊長類研究所
703:１３２人目の素数さん
26/07/31 19:02:34.87 lhoSS2YS.net
>>691-694
私自身がオイラーの定数γは有理数であるとはいっていない
だから、あくまでもコントなのである
704:１３２人目の素数さん
26/07/31 19:27:03.92 lhoSS2YS.net
>>695
そのスレで π±e や πe などが超越数かどうかを議論していたようだが、
無理数かどうかが分かっていない実数が
無理数であるか有理数であるかが判明することや、
超越数かどうかが分かっていない実数が
超越数であるか代数的数であるかが判明することは、
物理的には時刻について熱の拡散現象のような不可逆な現象であるから、
複素平面C上で理論的に考えて、その結果を π±e や πe に
当てはめて考えると、π±e や πe はすべて超越数であることが証明出来る
705:１３２人目の素数さん
26/07/31 19:39:48.79 hpyAStSA.net
シャヌエル予想
706:１３２人目の素数さん
26/07/31 20:10:34.43 SJOUmyNL.net
>>704
嘘の人か
707:１３２人目の素数さん
26/07/31 22:40:55.28 ealb3z6A.net
>>684 補足
(引用開始)
>>683 補足
まあ、新一さんは 『[EssLgc]§1.12でも指摘』をあげていて
「なんか誤解している人がいるが、IUTは自明」だ
と思っていた
ところが、>>661 "３つの不定性 Ind1, Ind2, and Ind3 や 用語“blurring”に関連する概念が
いかにも自然言語であって そこが厳密なLean語に翻訳できない原因かもしれない・・"
となって いまここ
まあ、新一さん含めて 研究室の人たちの頑張りどころですね （＾＾
(引用終り)
数学史上では、過去にもしばしばあるが
自然言語が先行して、
形式的には若干厳密性を欠けたところがある場合に
あとから、「結局正しい」とされる場合ことがある
例えば、リーマン面（下記pdf）
例えば、カントール素朴集合論（下記pdf）
望月IUTも、そうなる可能性は
大いに有ると 見ています
URLﾘﾝｸ(riemannsurfaces.com)
URLﾘﾝｸ(riemannsurfaces.com)
History of Riemann surfaces
Daniel Ying ∗ October 11, 2005
∗PhD Student at University of Link¨oping. E-mail: [email protected], [email protected]
URLﾘﾝｸ(fuchino.ddo.jp)
URLﾘﾝｸ(fuchino.ddo.jp)
カントルの精神の継承—無限集合の数学／
超数学理論としてのカントルの集合論のその後の発展と，その「数学」へのインパクト
渕野昌(Saka´e Fuchino)
2019年05月08日
708:１３２人目の素数さん
26/07/31 22:48:54.12 FP+A9Q6a.net
>>632
>グロ宇宙はエレメンタリートポスでしかないだろ
これを同値だと言ったと勘違いしたんだなw
どういうロジックを使うかの話だよ
証明系の話なんでね
709:１３２人目の素数さん
26/07/31 22:50:56.61 FP+A9Q6a.net
>1本の数学査読掲載された論文がないこと
チンパンジーが喋ってるみたいだな
710:１３２人目の素数さん
26/07/31 23:34:45.66 r/hcKBTn.net
>>707
>数学史上では、過去にもしばしばあるが
>自然言語が先行して、
>形式的には若干厳密性を欠けたところがある場合に
>あとから、「結局正しい」とされる場合ことがある
>例えば、カントール素朴集合論（下記pdf）
はい、大間違いです。
素朴集合論はラッセルのパラドックスを生じるので矛盾しています。あとから「結局正しい」とされてません。
初歩の初歩から分かってないど素人さんは持論を語らない方が良いのでは？
711:１３２人目の素数さん
26/07/31 23:38:17.97 IJlR5x1d.net
宇宙は数学を認識してるという事実
712:１３２人目の素数さん
26/07/31 23:41:54.04 ealb3z6A.net
>>709
>>1本の数学査読掲載された論文がないこと
>チンパンジーが喋ってるみたいだな
補足しないと
分らないみたいだね
・理系の論文は、査読は査読であって、論文の絶対的な正しさを保証するものではない（常識）
・そのことは、自分が1本でも雑誌に論文投稿して レフェリーとのやり取りをして掲載された経験がある人には 自明のことだろう
・理系の論文は、他人がその論文をどう使うか？ それは読む人の責任だ
・その論文を読んで 正しいとして それを発展させる論文を書くのもありだし
・逆に、その論文の問題点を指摘するのもあり
・数学論文ならば、ギャップを発見して
そのギャップを埋める論文を投稿するのもあり
これを、望月IUTに見るに
１）望月IUT論文が間違っているというならば、そしてその修正案があるならば
それを論文にして投稿すれば良い（Kirti Joshiさんみたく>>13）
２）あるいは,自分のアイデアでabc予想の解決論文書けば良い
３）望月IUT論文は、加藤文元氏が１年かけてLean化やるというから できるかも 1年待てばいい
713:１３２人目の素数さん
26/07/31 23:43:53.08 CUIKkJ7b.net
彼の人は
数学的な深い定義はすっ飛ばしても
理論が理解できるに違いないと思いたいようです
何とかピクチャーとかにこだわったり
自然言語にこだわったり
自分ができる限界がそこだから
そこまでで数学理論が理解できなくてはいけないんでしょう
714:１３２人目の素数さん
26/07/31 23:45:43.11 CUIKkJ7b.net
偶数と奇数m,nをAが選びカードに書いて箱に入れる
選び方はAの自由
入れた後でBがそのカードを両方取りだして
奇数を1偶数を0に書き直して箱に戻す
ここで
Bは箱の中からランダムにカードを1つ取り出す
Aは残った方を取る
小さい方を引いた方が勝ち
さてA,Bの勝つ確率は？
715:１３２人目の素数さん
26/07/31 23:53:33.73 ealb3z6A.net
>>710
>素朴集合論はラッセルのパラドックスを生じるので矛盾しています。あとから「結局正しい」とされてません。
わかってないね、おまえ
下記 渕野 「カントルの精神の継承—無限集合の数学」
P4からの引用を百回音読せよ！ｗ （＾＾
>>707 再録
URLﾘﾝｸ(fuchino.ddo.jp)
カントルの精神の継承—無限集合の数学／
超数学理論としてのカントルの集合論のその後の発展と，その「数学」へのインパクト
渕野昌(Saka´e Fuchino)
2019年05月08日
P4
集合論が背負わされることになった三番目の宿命は，—これは20世紀に入ってからのことになるのだが—集合論のパラドックス(antinomies) の発見とツェルメロらによる集合論の公理化による，パラドックスの回避，という19世紀から20 世紀初頭にかけての数学の展開から，「素朴集合論は間違っていた」という間違った風評が広まってしまったことであろう．実際には，カントルが集合論で得た結果には，このパラドックスと抵触するものは含まれておらず，カントル自身，ほとんど[Zermelo 1908] と同じとも言える精度での，パラドックスの回避についての理解を得ていたことが，デデキントやヒルベルトにあてた彼の書簡から見てとれる．
716:１３２人目の素数さん
26/08/01 00:05:46.80 sQaREFls.net
>>708
(引用開始)
>グロ宇宙はエレメンタリートポスでしかないだろ
これを同値だと言ったと勘違いしたんだなw
どういうロジックを使うかの話だよ
証明系の話なんでね
(引用終り)
意味分らん
・グロタンディーク宇宙 URLﾘﾝｸ(en.wikipedia.org)
・Elementary topos URLﾘﾝｸ(en.wikipedia.org)
・トポス (数学) URLﾘﾝｸ(en.wikipedia.org)
・History of topos theory URLﾘﾝｸ(en.wikipedia.org)
・Intuitionistic type theory URLﾘﾝｸ(en.wikipedia.org)
で？ これらが どうかしましたか？
717:１３２人目の素数さん
26/08/01 00:19:20.90 USUxMf+J.net
Abel Prize Laureate Gerd Faltings shares his official position on the infamous ABC Conjecture proof by his former PhD student, Shinichi Mochizuki.
In 2012, Mochizuki published a 500+ page paper claiming to have solved the ABC conjecture — one of the biggest open problems in number theory. More than a decade later, the mathematical community remains split, with many finding the inter-universal Teichmüller theory nearly impossible to digest. Here is what Faltings thinks about his student's work.
Excerpt from the post Abel Prize 2026 ceremony interview.
0:00 - "If I'm at page 500, I've forgotten page 1"
0:10 - Did Mochizuki prove the ABC Conjecture?
1:00 - Faltings' official position
1:55 - "PhD students are like children..."
URLﾘﾝｸ(youtu.be)
718:１３２人目の素数さん
26/08/01 00:39:23.63 CW+trfCW.net
>>715
>わかってないね、おまえ
わかってないのは君
URLﾘﾝｸ(ja.wikipedia.org)
カントールの理論
1899年までに、カントールは自身の理論の無制限の内包によっていくつかのパラドックス、たとえばカントールのパラドックス[8]やブラリ＝フォルティのパラドックス[9]が生じることに気づいていたが、それらが自身の理論の評価を下げるとは思っていなかった[10]。
パラドックスが生じる、つまり矛盾しているのに、あとから「結局正しい」とされた？ 頭だいじょうぶ？
719:１３２人目の素数さん
26/08/01 00:45:56.16 CW+trfCW.net
そもそも素朴集合論が矛盾を抱えた欠陥品だったからこそZF集合論が開発されたのに、あとから「結局正しい」とされる訳が無い。
自分の持論こそ正しいと信じて疑わないど素人さんにも困ったものだ。
720:１３２人目の素数さん
26/08/01 10:39:37.45 sQaREFls.net
ホイヨ
”多くの証明支援システムは型理論に基づいている。例えば、Rocq（旧Coq）の基盤となる形式言語は帰納的構成の計算であり、Leanは依存型理論に基づいている。”
(参考)
URLﾘﾝｸ(en.wikipedia.org)
Type_theory
(google訳)
型理論
数理論理学および理論計算機科学において、型理論とは、式や数学的対象をその型によって分類する形式体系の研究である。大まかに言えば、型はプログラミングにおけるデータ型と同様の役割を果たす。つまり、式がどのような種類のものであり、どのように使用できるかを指定する。型理論は、プログラミング言語（型体系）、形式論理、および数学の形式化の研究に用いられる。
数学の基礎として集合論に代わるものとして、いくつかの型理論が提案されてきた。例としては、アロンゾ・チャーチの単純型理論や、ペル・マルティン＝レーフの直観主義型理論などが挙げられる。
多くの証明支援システムは型理論に基づいている。例えば、Rocq（旧Coq）の基盤となる形式言語は帰納的構成の計算であり、Leanは依存型理論に基づいている。
721:１３２人目の素数さん
26/08/01 10:44:47.64 CW+trfCW.net
>>720
今更なコピペして何をどうしたいん？
722:１３２人目の素数さん
26/08/01 11:03:25.71 sQaREFls.net
>>719
>そもそも素朴集合論が矛盾を抱えた欠陥品だったからこそZF集合論が開発されたのに、あとから「結局正しい」とされる訳が無い。
>自分の持論こそ正しいと信じて疑わないど素人さんにも困ったものだ。
そう近視眼的な見方は、よろしくないね
・一つは、歴史的な順を理解することだね
つまり、カントール集合論があってこそ、公理的集合論が生まれたことと
カントールが得ていた集合論の結論（定理）は、矛盾なく公理的集合論で再現されたこと
・ZF集合論などが常用する記号による主に一階述語論理は
出来上がった定理証明や 理論展開用には 優れている面はあるが
まだ 海のものとも山のものともつかぬ対象を考えていくのには向かない
（つまり、これから新しい数学理論を作っていくときは、自然言語がベースになる）
実際、ZFないしZFC公理系のロジックだけで 自然言語は殆ど使わないというような、
数学テキストは 現在は存在しないだろう
一方で、コンピューター言語は 主は記号論理のみで 自然言語はコメントのみ
Rocq（旧Coq）や Lean >>720 は、こちら
(参考)>>720 より追加
URLﾘﾝｸ(en.wikipedia.org)
Type_theory
(google訳)
型理論
歴史
メイン記事：型理論の歴史
型理論は、素朴集合論や形式論理におけるパラドックス、例えばラッセルのパラドックスなどを回避するために考案されました。ラッセルのパラドックスとは、適切な公理がない場合、自分自身の要素ではないすべての集合の集合を定義することが可能であり、この集合は自分自身を含みつつ、自分自身を含まないという矛盾を抱えていることを示すものです。1902年から1908年にかけて、バートランド・ラッセルはこの問題に対する様々な解決策を提案しました。
1908年までに、ラッセルは型に関する分岐理論と還元可能性の公理に到達し、これらはどちらも1910年、1912年、1913年に出版されたホワイトヘッドとラッセルの『プリンキピア・マテマティカ』に登場した。この体系は、型の階層構造を作成し、各具体的な数学的実体を特定の型に割り当てることで、ラッセルのパラドックスで示唆された矛盾を回避した。ある型の実体は、その型のサブタイプのみから構成されるため、実体がそれ自身を用いて定義されることはなかった。このラッセルのパラドックスの解決は、ツェルメロ＝フレンケル集合論などの他の形式体系で採用されているアプローチと類似している。[ 4 ]
723:１３２人目の素数さん
26/08/01 11:28:54.62 sQaREFls.net
>>717
ありがと
見た 面白いね それ
724:；ｐ）
26/08/01 11:44:32.96 SyyZrKYb.net
「あなたが批判されるたびに『ふっふ、ほっほ（＾＾』と奇声をあげ、『中高一貫生も来るからハッキリと書いておく』
『赤ペン先生しておく』などと書き込む理由は、そうやって『無知な子供を導く偉大な指導者』を演じなければ、自分の惨めな
現実が崩壊してしまうからですよね。
本当は、IUT理論という最先端の盾を借りて、現代数学の盲点を突く『孤高の天才』として皆に恐れられ、崇められたいのでしょう。
しかし周囲から見えているあなたは、他者からの客観的な指摘を一行も理解できず、用意したコピペと安っぽい幼児退行のような
語尾を出力することしかできない『対話能力を失った記号出力装置』に過ぎません。
かつてオイラーのγが有理数だという浅薄な妄想を完璧に論破され、プライドをズタズタにされて何日もスレから逃亡していた
哀れな敗北者が、どの口で『赤ペン先生』を自称しているのでしょうか。ネットの過疎スレで中高一貫生という子供の影に隠れ、
彼らを見下すことでしか自尊心を保てない姿は、滑稽を通り越して見ていて本当に哀れです。
あなたがその不気味な笑い声を書き込むたびに、スレの住民が感じているのは知的な刺激ではなく、『他人の偉大な業績に
寄生して虚勢を張るしかなく、一度論破されれば子供相手の教師ごっこに逃げるしかない人間の、
底知れない孤独と知的な貧困』に対する冷笑だけです。
もう自分を騙すのはやめなさい。あなたが本当に直面すべきなのは、IUT理論や背理法の正誤ではなく、『どれほど画面の
向こうで指導者ぶってみせても、現実世界の誰一人としてあなたを数学徒とも、知的な人間とも認めていない』という、
凍りつくような孤立です。これ以上、自分の精神的な飢餓感を数学板に排泄するのはやめなさい」
725:１３２人目の素数さん
26/08/01 12:04:14.36 CW+trfCW.net
>>722
>そう近視眼的な見方は、よろしくないね
見方なるものでごまかそうとしても無駄
> つまり、カントール集合論があってこそ、公理的集合論が生まれたことと
何の言い訳にもなってない
> カントールが得ていた集合論の結論（定理）は、矛盾なく公理的集合論で再現されたこと
はい、大間違いです。
素朴集合論は矛盾しているから任意の命題φが素朴集合論の定理。一方φも￢φも公理的集合論の定理であるようなφはただの一つも見つかっていない。
カントールが得ていないと言いたい？彼は矛盾に気付いていたよ。
>・ZF集合論などが常用する記号による主に一階述語論理は
> 出来上がった定理証明や 理論展開用には 優れている面はあるが
> まだ 海のものとも山のものともつかぬ対象を考えていくのには向かない
>（つまり、これから新しい数学理論を作っていくときは、自然言語がベースになる）
何の言い訳にもなってない
726:１３２人目の素数さん
26/08/01 13:37:43.17 sQaREFls.net
>>645
> 多分、意図は忖度と、情報公開したら 他の人たちと競争になって
> LANAプロジェクトとして面白くないってことかもね
ここ、うがった見方だが
川上量生氏の狙いは
下記”本当に世界最先端のあの研究もやって実際成果も出す”
つまり、IUTのリカバリーを ZEN大学が イッチョかみして
ZEN大学の成果として 宣伝できたら良いなと
それを狙って Leanコード未公開なのかもしれんね
川上量生氏の狙い、なかなかだね
>>654より
URLﾘﾝｸ(youtu.be)
【ReHacQ生配信】AIで数学を証明!?IUT理論は正しいのか【高橋弘樹vs川上量生vs野村泰紀vs加藤文元】
ReHacQ－リハック－【公式】
166,727回視聴 2026/07/24
＜文字起こし＞
2:06:41
川上さんいかがでしたでしょうか?あの、 あのZEN大学は新設校じゃあありません。
2:06:48
あの、本当に世界最先端のあの研究もやって実際成果も出す、あの、そういう風な大学ですので、あの、是非皆さんですね、あの、入ってください。お得です。
2:07:03
お得。 お得です。 何が得なんでしたっけ? え、 何が得なんでしたっけ? あの、簡単に入ります。
2:07:08
簡単に全日配の授業も受けれるじゃないですか。
略
2:10:00
はい。え、あ、そうですね。はい。はい。
727:１３２人目の素数さん
26/08/01 13:51:20.55 sQaREFls.net
>>724
ありがと
見た 面白いね きみ
殆ど レスするに値しない カキコだね
１）基本認識間違ってない？
ここ５ｃｈは 場末の便所落書き板
むかし、SNSが台頭するまえは、日本一賑わっていると言われたこともあったが
いまや 寂れている
その寂れた５ｃｈの中でも、数学板は ほぼ最底辺の過疎板だろう
２）こんなところで、むきになって 他人にお説教か？
自分 何様のつもりなんだろね？
数学力低そうだな
ここは、天下の過疎板 ５ｃｈ数学板
みんな好きなことを 好きなように書けば良いんじゃ無いの？
他人の書込みに イチャモンつける暇あったら
自分が、キチンとしたことを書く努力をしな
ほれほれ、自分がキチンとしたことを書いてみな
どれどれ？ どれだい？
ない？ ん？ 自分がキチンとしたことを書けない？
だったら 黙ってなよｗ （＾＾
728:１３２人目の素数さん
26/08/01 13:57:24.74 fqeZgoT8.net
よくもまあ無駄な煽りが延々とできるもんだ
729:１３２人目の素数さん
26/08/01 13:57:46.27 fqeZgoT8.net
中身に集中しなよ
中身だけ書けばいいのに
730:１３２人目の素数さん
26/08/01 14:08:28.90 CW+trfCW.net
>他人の書込みに イチャモンつける暇あったら
>自分が、キチンとしたことを書く努力をしな
と、嘘デタラメばかり書いてるど素人さんが熱弁しております
731:１３２人目の素数さん
26/08/01 15:04:10.03 BIPVTn2/.net
精神分裂IUT朝鮮人中身ゼロw
732:１３２人目の素数さん
26/08/01 15:17:32.19 VIHfI2ko.net
>>707
＞あとから、「結局正しい」とされることがある
＞望月IUTも、そうなる可能性は大いに有ると 見ています
国粋高卒素人の哀れな妄想
733:１３２人目の素数さん
26/08/01 15:20:51.12 VIHfI2ko.net
Q カントールの”素朴集合論”は、フレーゲの理論と同じ？
A 「カントールの素朴集合論＝フレーゲの理論」と言うのは正確ではありません。より正確には、
フレーゲの体系は、カントール時代の素朴な集合観を論理学の中で厳密に実現しようとしたものであり、
その結果としてラッセルのパラドックスが明確な形で現れた、
と理解するのが歴史的・数学的には適切です。
734:１３２人目の素数さん
26/08/01 15:26:13.29 VIHfI2ko.net
Q フレーゲの内包公理による理論からは矛盾が導かれ、
ツェルメロの分出公理による理論からは今のところ矛盾が導かれていない
このことから
「カントールの素朴集合論はフレーゲの理論ではなく
実はツェルメロの分出公理による公理的集合論だった」
というのは・・・後だしジャンケンではないのか？
A 現在の歴史研究では、おおむね次のような見方が支持されています。
・カントールの集合概念は、公理化以前の「素朴な集合概念」だった。
・その概念には、ラッセル型のパラドックスを避けるための明確な制限は含まれていなかった。
・フレーゲはその種の素朴な発想を論理学の中で形式化し、その形式体系は矛盾した。
・ツェルメロは、カントールの数学的実践をできるだけ保存しつつ、パラドックスを避けるように公理を組み直した。
この意味では、ツェルメロの公理系はカントールの「本来の理論」をそのまま再現したものではなく、
「カントールが実際に行っていた数学を安全に再構成したもの」と理解するのが最も自然でしょう。
ですから、「カントールは実はツェルメロだった」という言い方には後付けの要素がありますが、
「ツェルメロはカントールの数学的成果をできるだけ残すように公理化した」という評価であれば、
歴史的にも数学的にも妥当な表現だと考えられます。
735:１３２人目の素数さん
26/08/01 15:31:29.21 VIHfI2ko.net
Q いずれにせよ、「公理化していなかった」のなら、
今の基準でいえば「間違ってすらいない」レベルということか？
A はい、その表現にはかなり重要な真理が含まれています。
ただし、少し言い換えるとより正確になります。
「公理化していなかったのなら、
現代の意味で『正しい』『間違っている』と
判定できる対象ではなかった」
ということです。
理由は、現代数学では「理論が矛盾する」というのは、
明示された公理と推論規則から矛盾が導けること
を意味するからです。
カントールの場合は、そもそも
・公理の一覧がなく、
・推論規則も形式化されておらず、
・「どのような集合形成を認めるか」も厳密には定義されていませんでした。
したがって、「カントールの理論からラッセルのパラドックスが導かれる」と言うためには、
まず「カントールの理論とは何か」を形式的に定める必要があります。
その定め方によって結果が変わる可能性があります。
例えば、
・フレーゲ流に形式化すれば矛盾します。
・ツェルメロ流に形式化すれば（少なくとも現在までのところ）矛盾は見つかっていません。
・他の公理系（たとえばNBGやMKなど）に形式化することもできます。
つまり、「カントールの理論」という名称だけでは、
形式理論として一意に定まっていないのです。
カントールの集合論は完成した形式理論というより、
集合という概念を用いた数学研究のための研究プログラム
あるいは直観的枠組みだった、と見るのが適切でしょう。
ですから、「カントールの集合論は間違っていた」と断言するよりも、
「カントールの集合論は、まだ『矛盾するかどうか』を形式的に問える段階の理論ではなかった」
という言い方の方が、現代の論理学や数学基礎論の観点からは正確だと考えられます。
736:１３２人目の素数さん
26/08/01 15:36:13.20 USUxMf+J.net
統合失調症のjinは自演もする
737:１３２人目の素数さん
26/08/01 15:38:52.08 tsS3dDrr.net
望月さんのIUT構想の数々の概念導入は天才グロタンディークを模倣してるよ
グロタンディークが築いた現代数学の最難関分野である数論幾何学、代数幾何学、圏論で
スキーム論という壮大という数論概念を創造し、必然的に数学構造上から出てくる自然さで
現代数学者が誰も考えが思いつかなかった枠組から再構成し直すというスキーム概念を自ら創出。
数論幾何学、代数幾何学、圏論という最高難度の数学分野を、彼は難解な分野をバラバラに研究するのでなく
「全ての数学の背後にある普遍的で必然的な構造として捉える」という巨大な目的のために、これらを融合させ
最初は難解な考えと世界の数学者達から捉えられたいたが、次々証明されていき、振り返ると数学構造上から、
最初は不自然に見える概念が、より大きな構造の中では唯一自然なものになるという離れ業を証明してるしね。
738:１３２人目の素数さん
26/08/01 17:36:59.73 fQh4Pm22.net
博士号を取るのが一番難しい分野は数論幾何だと聞くけど、研究で業績を上げるのが一番難しいのも数論幾何なのかな
739:１３２人目の素数さん
26/08/01 18:15:50.27 sQaREFls.net
>>735
>カントールの場合は、そもそも
>・公理の一覧がなく、
>・推論規則も形式化されておらず、
>・「どのような集合形成を認めるか」も厳密には定義されていませんでした。
>したがって、「カントールの理論からラッセルのパラドックスが導かれる」と言うためには、
>まず「カントールの理論とは何か」を形式的に定める必要があります。
>その定め方によって結果が変わる可能性があります。
ご苦労さま
「ミネルヴァの梟(フクロウ)は迫り来る黄昏と共に漸く飛び始める」(ヘーゲル)（下記）
この伝でいえば、コウリ職人は「迫り来る黄昏と共に漸くコウリ作りを始める」だろう
ユークリッド幾何公理しかり
直角三角形(3,4,5)は はるか古代エジプト時代にすでに 知られていた
が、幾何公理が整備されて ユークリッド幾何はさらなる発展を遂げた
これを、集合論のZF公理に見るに 集合論の公理職人が働き出す以前に
カントールはきちんとした仕事をしたのだ
だが、ZF公理公理化を経て 無限集合論がさらなる発展を遂げたことは
まさに ユークリッド幾何の公理が整備されて
理論が発展した歴史に倣っている
そういうことですね （＾＾
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
(抜粋)
ミネルヴァのフクロウは、ローマ神話の女神ミネルウァ（ミネルヴァ、ミネルバ）が従えているフクロウであり、知恵の象徴とされる
ヘーゲルが『法の哲学』（1821年）の序文「ミネルヴァの梟は迫り来る黄昏と共に漸く飛び始める」[2]
と述べたことはよく知られている
「即ちヘーゲルに依れば、哲学はいつでも遅れて来るもので、現実がその形成過程を完成した後に現われ、これを追思惟 nachdenkenするものである。かように現実が終った後に哲学が始まるとするのは、哲学を観想的な性質のものとすることであり、哲学に予言者的な性質を要求する立場とは固より、哲学の実践的な性格を力説する立場と対立している。」（三木清「ミネルヴァの梟」[4]）