26/07/25 14:12:25.30 AuqA/R3q.net
>>493 補足
>・RIMS のIUT論文別冊出版のとき
> 巻頭に編集者連名で「ちゃんと審査したので大丈夫」宣言を書いた
> 柏原先生が 筆頭だったが、10名くらい居たはず
類似例は、数学史ではしばしばある
自然言語系では、当然視・自明視していた事項が
実は、公理系の選び方で、自明ではないと判明することがある
下記の可算選択公理みたく
多くの人が 賛同したことは
後世から見て「まるっきり間違いとは言えない」ねと
そこらがハッキリすれば
それはまた数学の更なる発展に繋がる
ともかく、オープンな議論にすることが大切なことだろう
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
選択公理
可算選択公理
カントール、ラッセル、ボレル、ルベーグなどは、無意識のうちに可算選択公理を使ってしまっている。
495:１３２人目の素数さん
26/07/25 14:14:04.64 w8hVZYjm.net
>>493
その通りだとは思うがどう考えても誰かはダメージを受けるね。
そしてその可能性のある人間が問題解消に動くとはとても思えない。
496:１３２人目の素数さん
26/07/25 14:18:47.69 +LSaq+7s.net
>後付けでも ロジック追加で Lean形式化のギャップを埋めることができれば
>一応格好はつく
格好つくどころか世紀の大証明
497:１３２人目の素数さん
26/07/25 15:40:41.84 yA77s9YW.net
>>494
>>493
後付けすれば勝てる！！
パチンコ中毒朝鮮人の主張w
498:１３２人目の素数さん
26/07/25 15:41:39.22 GEmS8Kd0.net
>>490
オープンに望月新一の大惨敗を認めればいいだけ
499:１３２人目の素数さん
26/07/25 15:43:44.38 GEmS8Kd0.net
>>493
IUT証明は大失敗
後付けで証明したら
望月新一ではなくLean形式化チームのみの大成果
望月も星も蚊帳の外 残念でした 南無阿弥陀仏
500:１３２人目の素数さん
26/07/25 15:44:35.23 GEmS8Kd0.net
>>494
自明でないなら即敗北
はいっ、死にました！
501:１３２人目の素数さん
26/07/25 16:52:44.94 9niKyc4j.net
そのギャップを解決する本質的なアイデアがなくて空虚なのなら一からABC予想証明するより難しいかもしれないけど
502:１３２人目の素数さん
26/07/25 17:01:49.83 bmdqsgm3.net
>>501
GAP解消に至らなくても
とても良いアイデア満載なんだろ
503:１３２人目の素数さん
26/07/25 17:02:40.97 bmdqsgm3.net
しかっし
IUTダメなら
F1何てもっとダメダメだろうに
504:１３２人目の素数さん
26/07/25 17:23:33.39 1OyDcIqY.net
>>480
↑これって望月先生本人の？
まじですか
505:１３２人目の素数さん
26/07/25 18:33:58.86 AuqA/R3q.net
順番にいくよ
>>504
>↑これって望月先生本人の？
>まじですか
多分、望月先生ご本人でしょう
他にも多数の投稿があるよ
それらは、望月先生ご本人と仮定しても 完全に無矛盾だから
>>495-503
>その通りだとは思うがどう考えても誰かはダメージを受けるね。
理系では仕方ない
よくあることです
論文が間違っていました
これのゴマカシは きかない
>オープンに望月新一の大惨敗を認めればいいだけ
それに近いが 「Lean形式化未達」を
まず 率直に認めることだね
全ては そこが出発点だ
>後付けで証明したら
>望月新一ではなくLean形式化チームのみの大成果
>望月も星も蚊帳の外 残念でした 南無阿弥陀仏
もし、そうなっても仕方ないだろう
数学では ゴマカシはきかない
>そのギャップを解決する本質的なアイデアがなくて空虚なのなら一からABC予想証明するより難しいかもしれないけど
まあ、現実を
誤魔化さずに素直に 直視すること
そこが、基本で出発点ですよ
506:１３２人目の素数さん
26/07/25 18:48:31.43 +LSaq+7s.net
内容ゼロ
507:１３２人目の素数さん
26/07/25 18:53:21.43 QIF3bQjn.net
とんでも論文なのに権威のゴリ押しでごね得狙うのはAIでできなくなりそうだね
望月に限らずちゃんと証明書いてないのにプロには当たり前だ！とか居直る困ったエライ人も多いからね
深谷小野vsMcDuffはどうなるのかな？
508:１３２人目の素数さん
26/07/25 19:11:36.52 xZue3L+T.net
>>488
それならそうはっきりと言えばいいだろ
509:１３２人目の素数さん
26/07/25 19:16:38.68 bmdqsgm3.net
>>508
言ってると思うが
510:１３２人目の素数さん
26/07/25 20:13:39.51 gUOaiiW+.net
>>509
のようなものじゃ駄目だろ
そもそもRIMSの人たちは圏論から述語論理に翻訳出来るのかね
511:１３２人目の素数さん
26/07/25 21:48:20.71 bmdqsgm3.net
n変数の論理式はV^n={(x1,…,xn)}の部分クラスとみなせないかな
V^nの部分クラス全部がn変数論理式とは見なせないかもと思うけど
φ(x1,…,xn)
に対して
P={(x1,…,xn)|φ(x1,…,xn)}
を考えてやれば
φ⇔ψ
であるものを同一視するので十分じゃ無いかな
どうせ使うのはφ(x1,…,xn)の真偽だけだから
論理式として異なっていても真偽が一致すれば
問題にならないんじゃ無いかな
512:１３２人目の素数さん
26/07/25 21:53:16.26 AuqA/R3q.net
>>505 補足
>まあ、現実を
>誤魔化さずに素直に 直視すること
>そこが、基本で出発点ですよ
みなさん
コメントありがとう
繰り返すが
１）望月、星、加藤で話をして 現状のLeanのコードを含めて
あらいざらい、オープンにすること
２）望月＋星他 一族で 今回の中間報告への応答を発表すること
まず、すなおに Lean形式化未達であること
その原因についてを述べて
その後,これからどうするのか？ 計画と見通しを述べる
３）その後、Lean形式化達成に向けて、シンポジュームとか
オープンな議論の場を持つ（議論は公開する）
これを繰り返す。その中で、Lean化達成できればGood！
513:１３２人目の素数さん
26/07/25 21:54:06.53 1OyDcIqY.net
これ本人だとすると全くleanわかってない
公式文書読めよ
514:１３２人目の素数さん
26/07/25 22:28:25.08 yA77s9YW.net
みなさんありがとうとか言ってんの笑う
文字読めてねえw
515:１３２人目の素数さん
26/07/25 22:28:53.90 yA77s9YW.net
ID:bmdqsgm3
こいつマジで言語障害以前に知恵遅れてるだろ
516:１３２人目の素数さん
26/07/25 22:36:41.09 AuqA/R3q.net
>>513
>これ本人だとすると全くleanわかってない
>公式文書読めよ
うん
１）まず、本人かどうかだが、下記の全33件で 最初が 2016.11.25で
このときから 本人かどうかが問題になった
が、それから10年、いまでは、まずご当人だろうとされている
（当人しか書けそうもないことも書いてあるから）
２）”全くleanわかってない”は、自身でも発言しているし 正しいだろう
だから、leanチームとのインターフェイスは 星さんが担ってきた
３）ゆえに、leanチームの許諾を得て、現状のleanコードを公開してもらって
それを 遠アーベル関係者（仏国も含め）で共有して
leanに詳しい京大の人にも入って貰って、3.11→3.12を いろいろ突き回すことも検討しないとね
そう思うわけです
私も leanは 詳しくないが
ともかく オープンにすること、衆知を集めること、マンパワーを増やすこと
ここらが、基本ですね
(参考)
>>479 より
新一の「心の一票」
URLﾘﾝｸ(plaza.rakuten.co.jp)
新着記事一覧(全33件)
URLﾘﾝｸ(plaza.rakuten.co.jp)
はじめまして
ブログを開設しました。仕事で忙しくてそれほど頻繁に更新することはできないかもしれませんが、とりあえず、この通り、略式でブログ開設のご挨拶をさせていただきたいと思います。どうぞよろしくお願い致します。（因みに上の画像は富士山の写真です。もう少し補足しますと、2015年11月、親戚の結婚式に出席するために静岡を訪問した際に撮った写真です。）
2016.11.25
517:１３２人目の素数さん
26/07/25 22:59:36.73 bmdqsgm3.net
>>515
下らないね君
518:１３２人目の素数さん
26/07/26 01:42:28.32 PZsQ0etD.net
>>517
文盲のセリフがこれw
519:１３２人目の素数さん
26/07/26 07:40:07.33 KL8UsKGR.net
「のようなもの」を形式化して新しい数学の地平ですね
定義ははっきりしないのようなもの
のようなものから始まる数学
「の・ようなもの」のエリザベスがRIMS呆酷暑読んでたりする世界か
520:１３２人目の素数さん
26/07/26 08:15:37.02 3b2MGiGr.net
>>505
>>オープンに望月新一の大惨敗を認めればいいだけ
>それに近いが
誤 それに違いが
真 そのものズバリだが
さっさと玉音放送を流しなさい
今後帝國ノ受クヘキ苦難ハ固ヨリ尋常ニアラス
爾臣民ノ衷情モ朕善ク之ヲ知ル
然レトモ朕ハ時運ノ趨ク所
堪ヘ難キヲ堪ヘ忍ヒ難キヲ忍ヒ
以テ萬世ノ爲ニ太平ヲ開カムト欲ス
>>後付けで証明したら
>>望月新一ではなくLean形式化チームのみの大成果
>もし、そうなっても仕方ないだろう
トンデモ過ぎて、そうなりそうもない
数学界の「竹槍三百万本論」
521:１３２人目の素数さん
26/07/26 08:26:50.88 jgtmOrU+.net
>>516 補足
>まず、本人かどうか
取りあえず下記が参考になるでしょう
（もちろん、厳密な証明ではないが）
あとは、33件の投稿を見て 各自ご判断願う
(参考)
URLﾘﾝｸ(plaza.rakuten.co.jp)
新一の「心の一票」
2016.12.18
本ブログに対するコメント等への対応について
(抜粋)
私は余りにも「特異性」の高い人間なので、自分の身元を隠してもばれるのはどうせ時間の問題であり、身元を隠すことにはあまり意味がないとの結論に達しました。
私は数学者であり、私の研究・教育活動については京都大学のサイト内のホームページをご参照下さい。
URLﾘﾝｸ(www.kurims.kyoto-u.ac.jp)
（因みに、「なりすまし」の可能性が気になる読者の方もいるかもしれませんが、いざというときは、上記の（大学のサイト内の）ホームページやそこに記載されているメールアドレスの管理体制と、本ブログの管理体制がリアルタイムで連動していることはいつでも簡単に証明できます。）
一方、本ブログでは、大学のサイト内のホームページに「相応しくない」様々な個人的な、非数学的な感想やコメントを公開するつもりです。
URLﾘﾝｸ(plaza.rakuten.co.jp)
新一の「心の一票」
2017.01.04
本ブログの開設に当たっての抱負と名称の由来
(抜粋)
・加藤文元さんのツイッター：数ヶ月前にこのツイッターを偶々発見して、2005年～2011年春までの間、月に数回、数時間の数学の「セミナー」をした後、一緒に食事（＝多くの場合、焼肉）に行くという形で加藤さんと頻繁に交流していた頃の気分を懐かしく思い出し、何らかの形でその頃の「気分」を再現できないか検討したところ、（ツイッター等のSNSだと文字数の制限があったりして自分のように長文を書きたがる体質の人間には向かないだろうと感じたため）ブログを開設するのが一番自分のイメージに合った形態の「個人的文化発信」の装置になるであろうとの結論に達しました。
・自己紹介機能の「名刺代わり」：私の場合、日本語と英語のネットしか読めませんが、私＝「望月新一」という人物を巡って私の想像を超えたような＝目を覆いたくなるような＝開いた口が塞がらないような、とんでもない出鱈目なネット上の書き込みが氾濫しています。
・私はもう少しで48歳になりますが、略
・私の「心の一票」：略
私はアメリカには住みたくない、英語はもう聞きたくない。
つまり、
「日本」、「日本語」に投票したい。
でも、（当たり前ですが）そのような「明確な意思」を米国の民主党や共和党への支持によって表明することは明らかにも技術的に本質的に不可能です。具体的なレベルでいうと、博士課程を修了したら日本の大学に就職できるように様々な努力をすること以外に、上記の「本音」を実現する方法がなかったように思いますし、実際、そのような努力をすることによって目出度く（というか、運よく）その「本音の実現」に（京大の助手のポストという形で）漕ぎ着けることができました。
522:１３２人目の素数さん
26/07/26 08:58:50.61 jgtmOrU+.net
>>520
>真 そのものズバリだが
>さっさと玉音放送を流しなさい
証明は、成立か 不成立か ２値の世界だが
数学は、勝った 負けた の世界ではない
>>後付けで証明したら
>>望月新一ではなくLean形式化チームのみの大成果
>もし、そうなっても仕方ないだろう
例え話で 補足しておくと
・望月さん 詰め将棋の長手数問題を作った。名前が ”遠アーベル流IUT”
・それを、ある将棋ソフトの解析にかけたら、ある部分で詰まないよ と出た
・それを受けて、詰め将棋作者の望月氏がどうするか？
普通は、下記
１）将棋ソフトの解析をオープンにする
２）なぜ詰まないのか？ どこか改善できないか？
３）まれに、将棋ソフトのバグの可能性もあるかもです（Lean ライブラリー不備）
で、仏国との遠アーベルの国際研究プロジェクトが 走っている
URLﾘﾝｸ(ahgt.math.cnrs.fr)
早く解決した方がいいよね
（否定か肯定か 最終結果に関わらず）
仏国にも 「どうなってんの？」「こうなっています」と オープンに全てを報告した方がいい
523:１３２人目の素数さん
26/07/26 09:16:07.04 q7nx5Qo2.net
アホ
524:１３２人目の素数さん
26/07/26 09:32:47.69 GAZVSuj5.net
S-S同様IUTは間違いと言っていて
しかし自分がその間違いを正したと主張してた人居たと思うけど
その人はLANAの発表を受けて何か言ってないの？
S-Sはもうとおに興味失っているだろうから
特に何も言わない？
でも加藤さんがS-Sも間違ってると言っているのには
コメントしてイイと思うけどね
525:１３２人目の素数さん
26/07/26 09:39:16.84 jgtmOrU+.net
>>522 補足
>証明は、成立か 不成立か ２値の世界だが
>数学は、勝った 負けた の世界ではない
囲碁では、形勢判断が非常に重要で
かつ 将棋よりも 変化の手段の余地は大きい
”考えれば手はあるもの”（坂田栄男『囲碁名言集』（下記））と言われる
数学でも、最初のアイデアは厳密さが欠けていたが
後世に 厳密な証明が与えられた例は多数ある
例えば
１）ニュートン・ライプニッツの微分積分：結構直観的な議論だが、後世厳密化された
２）5次代数方程式の冪根解法：イタリア ルフィニ氏が不可だと言った。アーベルが厳密な証明を与えた
３）ガロアの方程式理論：決闘前夜の走り書きで、ある部分では”証明は思いつくであろう”と流したりがあったが（不成立の命題もあった）、後世正しいとされた
４）リーマン面：リーマンの議論は厳密性を欠くと言われたが、結局正しかった
IUTに戻ると、現状Lean形式化に乗らない部分があると言われるが
一方で、IUT論文を正しいと認めた 数学者 多数
筆頭が 玉川先生かな？ 仏国の数学者も多数 認めた
なので、上記例のように 何某かの数学的真理を含んでいる可能性はあると見ています
望月先生、頑張って下さい！
(参考)
URLﾘﾝｸ(rendaico.jp)
囲碁吉の天下六段の道
更新日／２０２４（平成３１．５．１栄和改元／栄和６）．３．１日
(抜粋)
【坂田の「1 心理編」】
「坂田栄男『囲碁名言集』（有紀書房、1988年）」の「1 心理編」は次の通り。
あきらめる前に、もう一度考えよう。考えれば手はあるものだ
526:１３２人目の素数さん
26/07/26 09:53:17.44 q7nx5Qo2.net
アホ
527:１３２人目の素数さん
26/07/26 09:58:51.89 jgtmOrU+.net
>>524
>S-S同様IUTは間違いと言っていて
>しかし自分がその間違いを正したと主張してた人居たと思うけど
うん、下記のKirti Joshiさんだね
>でも加藤さんがS-Sも間違ってると言っているのには
”S-Sも間違ってる”の部分は、下記動画でキラン・ケドラヤ氏が報告していた
公開文書にも、記載があったと思う
えーと Contents ”10. An examination of Scholze-Stix document 46”だね
(参考)
URLﾘﾝｸ(sites.arizona.edu)
Webpage of Kirti Joshi
（リンクあるが略す）
My reports on the Mochizuki-Scholze-Stix Controversy
・Final Report (May 2025) [Provides my final conclusion regarding the proof of the abc-conjecture.]
・Provisional Report (June 2024) [Written after extensive correspondence (in May-June 2024) with Peter Scholze and it provides robust conclusions regarding the invalidity of the Scholze-Stix Report, but because Mochizuki was objecting to my work (in March 2024),
I did not provide any conclusion on the proof of the abc-conjecture. This report also contains a time-line of events leading upto this report.]
URLﾘﾝｸ(zen.ac.jp)
2026/07/17 Zen大学
プレスリリース
IUT理論のコンピューターによる検証を目指す LANAプロジェクト、「Project LANA Interim Report on IUT Theory」を公開
——現時点での評価、残された課題、Scholze–Stix報告書との関係を報告
公開文書「Project LANA Interim Report on IUT Theory」
報告書全文 ▶ URLﾘﾝｸ(github.com)
発表動画
URLﾘﾝｸ(youtu.be)
URLﾘﾝｸ(zen.ac.jp)
2026/03/31
プレスリリース
IUT（宇宙際タイヒミューラー）理論のコンピューターによる検証を目指すZEN数学センターの新プロジェクト「LANA」を発表
―世界3大学による国際共同研究として始動―
528:１３２人目の素数さん
26/07/26 14:14:45.90 PZsQ0etD.net
バカ朝鮮人のセルフコピペQ&Aかよw
でも論理で繋がってない低学歴キチガイ仕草w
529:１３２人目の素数さん
26/07/26 14:25:13.20 3b2MGiGr.net
負けを認められない国粋狂人 Set A
530:１３２人目の素数さん
26/07/26 14:43:25.79 PZsQ0etD.net
>>529
朝鮮偽右翼に国粋とか言うのやめろよ
531:１３２人目の素数さん
26/07/26 14:47:20.94 KL8UsKGR.net
>>525
証明論に限らず数学の形式化が進んでるから
昔みたいなことはもう起きないよ
532:１３２人目の素数さん
26/07/26 15:34:53.65 jgtmOrU+.net
>>531
>証明論に限らず数学の形式化が進んでるから
>昔みたいなことはもう起きないよ
たぶん 違うんじゃ無いかな
１）まず、下記の 渕野先生が書いている
”厳密性を数学と取りちがえるという勘違い”
２）さらには、形式化の限界
これは、下記ゲーデル不完全性定理の話（下記）
”証明できない真実: 第一不完全性定理により、内容としては正しい（真である）にもかかわらず、その体系の中のルール（公理）だけでは「正しい」と証明できない命題が必ず存在することが示されました”
要するに、数学とは IUTのLean形式化の失敗をのり超えて 進んでいくものだと思う
（それは、何かを追加して Lean形式化が出来るのか 逆に IUTは根本に問題あり となるか どちらか不明だが）
(google検索)
ゲーデル不完全性定理の数学における意義は何か？
AI による概要
ゲーデルの不完全性定理の数学における意義は、「すべての数学の真理を完全に証明できる一つの完璧なルールブック（公理系）を作ることはできない」と示したことです。主な意義として、ヒルベルト・プログラムの挫折、真と証明の乖離、数学基礎論の発展があげられます
ヒルベルト・プログラムの挫折
略
「真理」と「証明」の限界
・証明できない真実: 第一不完全性定理により、内容としては正しい（真である）にもかかわらず、その体系の中のルール（公理）だけでは「正しい」と証明できない命題が必ず存在することが示されました
>>30より再録
＜厳密だけが、数学ではない＞
＜数学と厳密＞
あなたのまったく逆を、渕野先生が書いている
”厳密性を数学と取りちがえるという勘違い”
URLﾘﾝｸ(www.amazon.co.jp)
数とは何かそして何であるべきか デデキント 訳解説 渕野昌 筑摩書房2013
「数学的直観と数学の基礎付け 訳者による解説とあとがき」
P314
(抜粋)
数学の基礎付けの研究は，数学が厳密でありさえすればよい， という価値観を確立しようとしているものではない.
これは自明のことのようにも思えるが，厳密性を数学と取りちがえるという勘違いは，
たとえば数学教育などで蔓延している可能性もあるので，
ここに明言しておく必要があるように思える
多くの数学の研究者にとっては，数学は，記号列として記述された「死んだ」数学ではなく，
思考のプロセスとしての脳髄の生理現象そのものであろう
したがって，数学はその意味での実存として数学者の生の隣り合わせにあるもの，と意識されることになるだろう
そのような「生きた」「実存としての」(existentialな)数学で問題になるのは，
アイデアの飛翔をうながす(可能性を持つ)数学的直観」とよばれるもので，
これは， ときには，意識的に厳密には間違っている議論すら含んでいたり，
寓話的であったりすることですらあるような，
かなり得体の知れないものである
533:１３２人目の素数さん
26/07/26 15:38:04.41 GAZVSuj5.net
（何かを理解しているつもりになっている）
534:１３２人目の素数さん
26/07/26 16:03:29.48 jgtmOrU+.net
>>532 補足
(引用開始)
>証明論に限らず数学の形式化が進んでるから
>昔みたいなことはもう起きないよ
たぶん 違うんじゃ無いかな
(引用終り)
意味が分らないだろうから、ABC予想の歴史を振りかえろう
１）昔々 フェルマーさんが、フェルマー予想を出した。証明を得たが、余白が狭いという名言を書いた
URLﾘﾝｸ(ja.wikipedia.org)
２）みんな挑戦したけど、最終解決にならない状態で 数百年
”1984年、ゲルハルト・フライは、フェルマー方程式とモジュラリティ定理（当時はまだ予想だった）との関連性を指摘した”（下記）
３）モジュラリティ定理は、日本では谷山志村予想で有名だが
当時は、モジュラリティ定理の証明は多くの数学者は「無理！」とあきらめた
そこで考えられたのが、abc予想だ
これは フェルマー予想で使われた 楕円曲線（フライ曲線とも呼ばれる）の性質から予想された不等式
要するに 流れは
フェルマー予想→フライが楕円曲線に関連づけ→谷山志村予想→谷山志村予想は難しいので迂回路して abc予想
→ 望月新一 おいらが 遠アーベルで証明するぞ とIUT理論を提出
→ LANA：Lean形式化に乗らないのでは？という中間報告（2026年07月 いまここ）
この数学数百年の大河の流れは、だれが考えても まだまだ 数学形式化だけでは 説明できないだろう
そもそも、ABC予想にもいろんなバリエーションありだしね（例えば 下記スピロ予想とか）
(参考)
URLﾘﾝｸ(en.wikipedia.org)
(google訳)
1984年、ゲルハルト・フライは、フェルマー方程式とモジュラリティ定理（当時はまだ予想だった）との関連性を指摘した。フェルマー方程式が指数p > 2に対して解( a , b , c )を持つ場合、半安定楕円曲線（現在ではフライ・ヘレグアルク曲線として知られている[注4 ]） が成り立つことが示された。
ワイルズの一般証明
1986年にリベがε予想を証明したことで、フレイが提案した2つの目標のうち最初の目標が達成された。リベの成功を知った、フェルマーの最終定理に幼い頃から魅了され、楕円曲線の研究をしていたイギリスの数学者アンドリュー・ワイルズは、後半の目標、すなわち半安定楕円曲線に対するモジュラリティ定理（当時は谷山・志村予想として知られていた）の特殊な場合を証明することに尽力することを決意した
URLﾘﾝｸ(ja.wikipedia.org)
ABC予想
オステルレ＝マッサー予想（英語: Oesterlé–Masser conjecture）[1][2]は、1985年にジョゼフ・オステルレとデイヴィッド・マッサーにより提起された数論の予想（未解決問題）である
URLﾘﾝｸ(en.wikipedia.org)
abc conjecture
(google訳)
abc予想は、オステルレとマッサーが楕円曲線に関するスピロ予想を理解しようとした試みの結果として生まれたものであり、[ 4 ]スピロ予想はabc予想よりも多くの幾何学的構造を含んでいます。abc予想は修正されたスピロ予想と同等であることが示されました。[ 1 ]
535:１３２人目の素数さん
26/07/26 16:52:47.41 q7nx5Qo2.net
>>532
>１）まず、下記の 渕野先生が書いている
>”厳密性を数学と取りちがえるという勘違い”
数学は厳密でなくてもよいと勘違いしてるのがおまえ。
>２）さらには、形式化の限界
> これは、下記ゲーデル不完全性定理の話（下記）
> ”証明できない真実: 第一不完全性定理により、内容としては正しい（真である）にもかかわらず、その体系の中のルール（公理）だけでは「正しい」と証明できない命題が必ず存在することが示されました”
それは数学そのものの限界であって形式化の限界ではない。
数学で論ずる対象は「何を仮定すると何が結論できるか」つまり相対的真理であって絶対的真理ではない。形式化はそのことを明らかにした。
>要するに、数学とは IUTのLean形式化の失敗をのり超えて 進んでいくものだと思う
内容ゼロのポエム
ど素人さんは持論を語らない方が良い。どうしても語りたければチラシの裏でどうぞ。
536:１３２人目の素数さん
26/07/26 17:46:10.90 CTtkSBc5.net
jin は頭の病気
537:１３２人目の素数さん
26/07/26 18:04:36.94 q7nx5Qo2.net
>>534
>この数学数百年の大河の流れは、だれが考えても まだまだ 数学形式化だけでは 説明できないだろう
この検索でヒットしたワードを訳も分からず並べただけの出来損ないのAIみたいなクソ文はなに？
538:１３２人目の素数さん
26/07/26 18:13:08.56 q7nx5Qo2.net
>（何かを理解しているつもりになっている）
馬鹿である自覚が無いので「理解しているはずだ、理解していないなんてことはあり得ない」とでも妄想してるんでしょう
539:１３２人目の素数さん
26/07/26 18:15:13.31 q7nx5Qo2.net
自覚の無い馬鹿ほど始末の悪いものは無い
540:１３２人目の素数さん
26/07/26 19:15:59.82 3b2MGiGr.net
>>532
＞”証明できない真実: 第一不完全性定理により、
＞内容としては正しい（真である）にもかかわらず、
＞その体系の中のルール（公理）だけでは
＞「正しい」と証明できない命題
＞が必ず存在することが示されました”
誤り
「内容としては正しい（真である）にもかかわらず、」が嘘
「内容として、正しい（真である）としたら」が正しい
「正しいとしたら、正しいことが証明できない命題」が正解
なぜなら、正しい、とわかってないから
やっぱ論理が分からん高卒には、そこがどうしても理解できんか
541:１３２人目の素数さん
26/07/26 19:19:00.94 3b2MGiGr.net
>>535
＞それ（ゲーデルの不完全性定理）は数学そのものの限界であって形式化の限界ではない。
そう 理論内で自身の命題の証明可能性を記述できるとすると、そういうことが起きる、という話
やっぱ論理が分からん高卒Set Aには、そこがどうしても理解できんか
542:１３２人目の素数さん
26/07/26 19:24:10.29 3b2MGiGr.net
結局
「q-pilot対数的体積の二つの計算が「tautologicalに同値」とされている点、
あるいは、アルゴリズムの出力から得られる複数の可能なデータのうちの一つが、
入力から定まるデータとどのように同一視されるのか」
という、2015年以来指摘され続けてきた問題点について
望月新一が全く説明できず「自明！」と吠え続ける限り
数学界からは相手にされない
10年同じことをいってるのが
実数の定義が理解できない高卒Set Aそっくり
543:１３２人目の素数さん
26/07/26 19:25:48.45 3b2MGiGr.net
>>539
真の馬鹿は己の馬鹿を決して認めたがらない
そしてそれゆえ無敵の馬鹿であり続ける
544:１３２人目の素数さん
26/07/26 19:40:24.15 jgtmOrU+.net
>>542
>望月新一が全く説明できず「自明！」と吠え続ける限り
>数学界からは相手にされない
１）数学界から相手にされて
2026年7月17日 LANA中間報告だろ？
２）LANA中間報告が出た。
それを受けて 望月一派がどうするか？
３）私の意見は、LANA中間報告のLeanコードを公開して
IUTに賛成・反対両方入れて オープンな議論をすべし
ということ
545:１３２人目の素数さん
26/07/26 19:42:02.71 Lm9NjsrG.net
スレがいつの間にか進んでいる
骨密度の数値か骨質のどちらかの数値が低下して背骨が弱くなって
脊椎を何ヶ所か圧迫骨折すると、骨折後体が不自由になって、
腰の腰椎などの脊椎が前に曲がって圧迫骨折の治療に時間がかかり
圧迫骨折した脊椎は元の状態に戻らないだけでなく
背中を思うように曲げたりして動かせなくなるから、
瀬田君も脊椎の圧迫骨折には気を付ける方がいい
まさかのまさかの大誤算でした
内服薬にも長期間服用すると副作用として
圧迫骨折を引き起こす薬剤があるんだね
546:１３２人目の素数さん
26/07/26 20:57:29.44 jgtmOrU+.net
>>545
ID:Lm9NjsrG は、おっちゃんか？
レスありがとうね
圧迫骨折のアドバイスありがとね
まあ、IUT+遠アーベルの話は
日本には 論客がたくさんいる
だから、玉川先生とか いろいろ入って貰って
解決策を議論すれば良い
LANAプロジェクトの中間報告に使った元データとか
洗いざらい出して オープンに議論することだね
547:１３２人目の素数さん
26/07/26 20:58:48.46 tAKMiHWD.net
数学の勉強は骨が折れる。
548:１３２人目の素数さん
26/07/26 21:11:38.63 /9yjFCLH.net
まだ寝言言ってるよ
leanで定式化できないなら数学でない
それがわからんのならもう出てくんな
能無し
549:１３２人目の素数さん
26/07/26 21:43:23.66 q7nx5Qo2.net
>>532
＞”証明できない真実: 第一不完全性定理により、
＞内容としては正しい（真である）にもかかわらず、
＞その体系の中のルール（公理）だけでは
＞「正しい」と証明できない命題
＞が必ず存在することが示されました”
完全性定理の反例があると言ってる？
550:１３２人目の素数さん
26/07/26 22:17:40.07 PZsQ0etD.net
>>549
そんな狭い範囲の話じゃねーんだよw
低学歴ってすぐ完全表現使うから嘘になるんだよ
ケーキ切れない論理も集合も知らないからIUT信者なんてやってられるんだよお前はww
551:１３２人目の素数さん
26/07/26 22:17:55.36 PZsQ0etD.net
低学歴w
552:１３２人目の素数さん
26/07/26 22:18:12.98 PZsQ0etD.net
実際さあ
こんなんでさあ
「天才だ！天才だ！」とか
言ってんのも言われるのも恥知らずって感じだよな
よく平気で生きてられるな
553:１３２人目の素数さん
26/07/26 22:27:16.17 q7nx5Qo2.net
>>550
完全表現って何？
俺がIUT信者？何盛大に勘違いしてんだこいつ？
554:１３２人目の素数さん
26/07/26 22:40:29.94 q7nx5Qo2.net
>>549
もちろん反例なんて無いから、間違ってるのは>>532。
PAで考える。ゲーデル文「ゲーデル文は証明できない」をGと書く。
不完全性定理から￢Gは証明できない。・・・(1)
(1)と完全性定理から￢Gが偽となるモデルが存在する。・・・(2)
仮に標準モデルで￢Gが真とすると任意のモデルでも真であるはずだから(2)と矛盾。背理法により標準モデルで￢Gは偽、すなわちGは真。
真なのは標準モデルでであって、任意のモデルでではない。それが>>532の間違い。
555:１３２人目の素数さん
26/07/26 23:11:09.43 jgtmOrU+.net
>>534 補足
へんなやつらが湧いているな
追加しておくと
１）IUTを なんらかのコンピューター証明に乗せられないか？
という案だけは、望月氏のIUT論文投稿後 随分初期からあった（10年以上前）
が、当時のコンピューター環境では、コンピューター証明に乗せるには
マンパワーとマシンパワーが足りなかっただろう（だれも出来なかった）
２）2026年の今は、Lean形式化と AIのアシストと マシンパワーで
ようやく IUTの検証が可能なレベルになってきたのでしょうね
３）さて、先の中間報告 7月17日 >>327 ご参照方
中間報告の結論は、現時点のLean形式化未達なれど 達成できる可能性はあるという
よって
１）みんなで手分けして 早く結論を出した法が良いだろう
そうしないと、望月研の院生とか「おれたちどうなるの？」って話とかね
２）軌道修正の余地はあるのでは？
現時点のギャップを埋めるライブラリー補充とか
ギャップを迂回する別ルートを探すとか
３）いまどきなら AIエージェント使いをリクルートして
AIエージェントを走らずとかもありだろう
収束を加速する手段は、いろいろ考えられるから
議論をオープンにすれば良いと思うよ
556:１３２人目の素数さん
26/07/26 23:13:39.21 jgtmOrU+.net
>>555 タイポ訂正
１）みんなで手分けして 早く結論を出した法が良いだろう
↓
１）みんなで手分けして 早く結論を出した方が良いだろう
余談
いまどき、AIエージェントが一番頼りになったりしてｗｗ （＾＾
557:１３２人目の素数さん
26/07/26 23:20:05.21 q7nx5Qo2.net
>>555
>現時点のLean形式化未達なれど 達成できる可能性はあるという
現時点のリーマン予想証明未達なれど 達成できる可能性はあるという
と同じくらい内容ゼロ。
>へんなやつらが湧いているな
ど素人さんは持論語らない方が良いというアドバイスも頑なに聞く耳持たない君がね
558:１３２人目の素数さん
26/07/26 23:21:58.03 q7nx5Qo2.net
>>556
全体がクソなのにtypo気にしても無駄
559:１３２人目の素数さん
26/07/26 23:24:43.18 GAZVSuj5.net
（どんな未解決問題も証明される可能性は常にある）
560:１３２人目の素数さん
26/07/26 23:37:50.76 jgtmOrU+.net
>>534 補足
１）AI「ヤコビアン予想」反例 まあ、これはこれ
URLﾘﾝｸ(rio2016.5ch.io)
AI「Claude Fable 5」が87年来の難問「ヤコビアン予想」を覆す反例を生成したとAnthropic研究者が報告
URLﾘﾝｸ(gigazine.net)
２）将来的には いまの囲碁や将棋AIみたく 人間のプロ棋士より上位互換になるかもだが
2026年現在の数学においては、総合的にはプロ数学者が上だろう
しかし、人間＋最新AIなら 並みのプロ数学者を超えるかもね
３）LANAプロジェクトのLean形式化で言えば
IUTがLean形式化をパスしなかった原因は いろいろ考えられるだろうが
可能性としては IUTの”3.11→3.12”ギャップがあることも考えられる
ここらは、議論を進めないと 分らないことだね
なので、話をオープンにして
早く進めた方が良いねと
561:１３２人目の素数さん
26/07/26 23:54:36.29 jgtmOrU+.net
>>560
>２）将来的には いまの囲碁や将棋AIみたく 人間のプロ棋士より上位互換になるかもだが
> 2026年現在の数学においては、総合的にはプロ数学者が上だろう
さて 補足
URLﾘﾝｸ(ja.wikipedia.org)
遠アーベル幾何学
数体とその絶対ガロア群の初期の結果は、アレクサンドル・グロタンディークによる数体の双曲線[1]についての予想に先立ち、ユルゲン・ノイキルヒ、ギュンデュズ・イケダ、岩澤健吉、内田興二（ノイキルヒ・内田の定理）によって得られていた。
単語としての「遠アーベル」はアーベルに否定の接頭辞 an がついたもので、1980年代のグロタンディークの有名な著作である「Esquisse d'un Programme」で導入された[2] [3] 。
望月新一はいわゆる単(mono-)遠アーベル幾何学を導入および発展させた[6]。それは、数体または他のいくつかの体にわたる特定のクラスの双曲的曲線について、その代数的基本群からその曲線を復元するものである。単遠アーベル幾何学の主要な結果は望月の「絶対遠アーベル幾何学」などにある[7][8]。
遠アーベル幾何学は、類体論の一般化の1つと見なすことができる。 他の2つの一般化（高次アーベル類体論と、表現理論的ラングランズ・プログラム）とは異なり、遠アーベル幾何学は非常に非線形でnon-アーベルである[9]。
(引用終り)
この 遠アーベル幾何学 でも
いつの日か 数学AIが 自力で グロタンディークを超えるアイデアを出すかもだがｗ
さすがに いまは「ヤコビアン予想」反例(>>560) 程度が限界でしょう（それでも凄いけどね）
別に ”パーフェクトイド空間”というのがある（下記URL）
ペーター・ショルツェ氏によって 創始されたという
URLﾘﾝｸ(ja.wikipedia.org)
数学AIが パーフェクトイド体を 自力で考えたらエライと思う
2026年時点では、それらまだ無理でしょう
なので、IUTのLean形式化は かなり人間の数学者が 奮闘する必要があるだろう
望月先生、がんばって下さい！
562:１３２人目の素数さん
26/07/27 00:28:21.84 n/V8zLfy.net
LANAのleanコードはなんで公開しないんだろうな？ClaudeCodeでほぼ作ったもので恥ずかしくてプロの数学者として公開できないとかなの？
まぁ望月さん達には公開してるっぽいからそれで必要十分と思ってそうではあるけど
563:１３２人目の素数さん
26/07/27 01:53:15.48 sKVJthfH.net
>>544
ZEN大学は数学界に入るのかどうか
かなり眉唾な状況になってきた
564:１３２人目の素数さん
26/07/27 01:59:51.43 sKVJthfH.net
>>555
Coqでもやろうと思えば出来たよ
Isabelleでもな
そんなややこしい数学じゃないから
問題はこういう一般的な数学の第一線ではかなり大雑把な表現が使われてること
対象の型について言及もほとんどなく誤ってるケースさえある
565:１３２人目の素数さん
26/07/27 02:02:01.87 sKVJthfH.net
>>562
望月を説得するために1年間必要だから
それまでにみんな群がってきて結論出ては態度が硬化する
566:１３２人目の素数さん
26/07/27 03:58:54.90 Ahtg297b.net
「LANAの形式化」というのが仮にあるとして、一応建前では
1) 3.11～3.12 のところにはギャップがある
2) それ以外ではギャップがない、最低でも矛盾がない
をみたすものでないと会見の内容と矛盾するが、2)がだめなんやろ。つまり「現時点で矛盾をうまない形式化」すらないんやろ。
少なくとも今の態度はそうとられても仕方ないやろ。
567:１３２人目の素数さん
26/07/27 04:12:17.09 sKVJthfH.net
>>566
一般的には
どういう数学構造や公理系が使われてるかざっくり調べてライブラリの準備
なければ整備
簡単そうなところはそれに伴いすぐにコード化して
後は順番に頭から
だと思う
だから3.12以降はあまり進んでない可能性もあるが
誰もそんな事は問題にしないだろう
望月星との対話が進まないから
チームは3.12以降に進んだ可能性もあるしな
568:１３２人目の素数さん
26/07/27 11:40:34.81 Ee+a0l2w.net
>>562-567
みなさん、レスありがとう
>LANAのleanコードはなんで公開しないんだろうな？
同意
おそらくは、加藤リーダーたちの忖度だと思いますが
客観的には、忖度の時期は過ぎていると思う
その理由は
１）IUT論文は、査読完了で出版されて数年たつ
２）PRIMS別冊巻頭言で、柏原委員長、玉川副委員長以下何名もの数学者が太鼓判
３）なので、ダメならダメ。リカバリー出来るなら出来る。皆で議論しましょうとオープンな議論であるべき
４）他に、東京工大から出した5人論文の話もある。望月IUTがこけたら こっちにも影響する
５）それ以外にも、仏国との遠アーベル共同研究プロジェクトとか影響大きい
ダメならダメで、すっきり出直すべきだし
リカバリー出来るなら 早くやるべき
（別に もう 望月氏以外でリカバリー出来るならそれでも可では？ 例えば、AIエージェント使いを連れてくるとかもありでしょ）
>Coqでもやろうと思えば出来たよ
同意ですが、leanの方が 良い面があるのでは？
lean使いの人口が多いとか
（プログラミング言語で、C言語か Javaかみたいな）
569:１３２人目の素数さん
26/07/27 11:51:41.74 QEPbZWbZ.net
また無内容
570:１３２人目の素数さん
26/07/27 14:25:27.15 ELrTEiig.net
544 >私の意見は、…オープンな議論をすべし
546 >オープンに議論することだね
555 >議論をオープンにすれば良いと思うよ
560 >話をオープンにして早く進めた方が良いねと
女子〇生に股をオープンに、という変態オッサンか（笑）
571:１３２人目の素数さん
26/07/27 14:29:32.31 ELrTEiig.net
>>568
>１）IUT論文は、査読完了で出版されて数年たつ
不正査読ね
>２）PRIMS別冊巻頭言で、柏原委員長、玉川副委員長以下何名もの数学者が太鼓判
みんなで不正査読を黙認ね
>３）だから、ダメならダメ。リカバリー出来るなら出来る。皆で議論しましょうとオープンな議論であるべき
不正査読が明らかになれば、RIMSは確実に取り潰されるけどね
>４）他に、東京工大から出した5人論文の話もある。望月IUTがこけたら こっちにも影響する
当然、無意味な前提から結論を導く無意味な論文になるね 不正査読かどうかは知らんけど
>５）それ以外にも、仏国との遠アーベル共同研究プロジェクトとか影響大きい
フランス人はIUTが正しいとは思ってないから 国粋🐎🦌のSet Aとかいう高卒とは違うよ
572:１３２人目の素数さん
26/07/27 14:33:04.20 ELrTEiig.net
>ダメならダメで、すっきり出直すべき
RIMS解体 高卒Set Aは数学板から足を洗うべき（笑）
573:１３２人目の素数さん
26/07/27 15:22:09.43 Ee+a0l2w.net
>>570-572
>>１）IUT論文は、査読完了で出版されて数年たつ
>不正査読ね
数学的真理という観点からは、その議論は無意味ｗ
１）いま 数論のabc予想がある
URLﾘﾝｸ(en.wikipedia.org)
２）abc予想が、既に解決済みか？ はたまた 未解決か？
これは、出来るだけ早く 決着させるべき問題だ
３）それが、数学界全体としてプラスなのであって
解決済みなら、その先へ
未解決なら、解決への歩みを進めるべし
簡単な話だろ？ｗ （＾＾
574:１３２人目の素数さん
26/07/27 16:09:49.99 QEPbZWbZ.net
また無内容
575:１３２人目の素数さん
26/07/27 16:20:25.41 +EtGURU+.net
最近XでIUTにダメ出ししてる人カッコいい
言ってる内容は全然わかんないけど数学できそう
576:１３２人目の素数さん
26/07/27 17:16:16.55 Ee+a0l2w.net
>>574-575
>>573で主張していることは
１）望月氏および望月氏側の人たちが、積極的に事態収拾にあたること
２）望月氏側の人たちには、IUT論文の査読を通して出版した人たちも含む
３）手順は、まずLANA中間報告のバックデータを全部公開する
次に、望月氏を中心に 3.12がLean形式化をパスしなかった原因を追究する
大体３か月から半年で まあ年末には 望月氏側の検討結果を公表する
そういう進め方をするという意思表明をすること
もし、3.11→3.12のLean形式化が、なんらかLeanライブラリー追加とかでできるならば、せいぜい３か月から半年でしょう
それ以上かかるなら、相当大掛かりな見直しだから それはそれで仕方ない
そこらを、はっきりさせれば良い
私見ですが、早期の”3.11→3.12のLean形式化”成功！の可能性は
大いにあると見ています
577:１３２人目の素数さん
26/07/27 17:50:51.87 ELrTEiig.net
>>573
>>不正査読ね
> その議論は無意味
その反論が無駄
ABC予想が証明できてないなら
不正査読決定 RIMS解体
>>576
私見だが、”3.11→3.12のLean形式化”成功！の可能性は
全くないとみている できるならとっくにできてる（笑）
578:１３２人目の素数さん
26/07/27 17:56:33.34 ELrTEiig.net
IUTの変 の展開
・望月新一とかいう自己愛性人格障害の人が
わけのわからんこといって書いた論文を
身内に不正査読させて無理矢理通そうとした
・RIMSで議論したが今更不正査読と認めると
最悪解体させられるので組織防衛のために
なんと見過ごすことにした
・しかしながらさすがに悪目立ちしすぎて隠蔽不可能
そういうしてる間に加藤文元が自分だけ助かろうと
LANAプロジェクトによる検証を立ち上げた
これでアウトの結果が出ても、加藤文元は、
自分は検証に向けて努力したということで
無罪放免を狙う作成（笑）
579:１３２人目の素数さん
26/07/27 22:01:51.54 9NBu0pqC.net
>>577-578
数学シロウトか
はたまた ｗ大数学科初日オチコボレさんか
どちから知らないが
全く説得力ゼロだね
いいか
21世紀の現代数学 は、高度に専門化されているから
分野が違えば、他の分野の人は ことの成否は 正確には判断できないとしたものだ
なので、LANAプロジェクトの中間報告は Lean形式化未達だが
達成できる可能性はあると
そういう報告をした（今後1年かけるとかね）
ところで、今後1年は長い（長過ぎるのでは？）
話を秘密にする理由が希薄だと思うし
もっと、オープンな議論にした方がいいと思うな
そこで自然に
ダメならダメ
やれるならやれると
なると思うぞ
580:１３２人目の素数さん
26/07/27 22:14:29.76 QEPbZWbZ.net
また無内容
581:１３２人目の素数さん
26/07/27 23:12:51.13 NNMZFXzh.net
ですね
582:１３２人目の素数さん
26/07/28 00:17:03.91 W0Cg6UGe.net
URLﾘﾝｸ(810ch.net)
URLﾘﾝｸ(script.s16.xrea.com)
583:１３２人目の素数さん
26/07/28 00:17:44.31 W0Cg6UGe.net
URLﾘﾝｸ(810ch.net)
URLﾘﾝｸ(script.s16.xrea.com)
584:１３２人目の素数さん
26/07/28 06:41:20.71 3Y4+2uQh.net
>>579
数学素人は自分だろ（笑）
＞中間報告は形式化未達だが達成できる可能性はあると
実際は、達成できないとまではいえない、という二重否定だがな
ニュアンスの違い 分かるか？ 素人
証明できた と 証明できないとまではいえない の違い
＞今後1年は長い（長過ぎるのでは？）
●ねよ
＞話を秘密にする理由が希薄
＞もっと、オープンな議論にした方がいいと思うな
望月新一とかいう●違いにいえよ
＞ダメならダメ
ダメなんで諦めて●ね ド素人
ガロア理論も分からん奴に数学は無理
585:１３２人目の素数さん
26/07/28 07:51:40.54 psEHBHy8.net
>>579
>ところで、今後1年は長い（長過ぎるのでは？）
>話を秘密にする理由が希薄だと思うし
>もっと、オープンな議論にした方がいいと思うな
補足しておくと
下記 ”Arithmetic, Homotopy, and Geometry 2027-28”
が計画されている
下記の Scientific committee メンバーは、IUTに賛同し支持してきたメンバーだ
会議の内容は、IUT限定ではないだろうが
しかし、発表でIUTを是として引用文献に挙げることができるか
あるいは、IUTを非とする議論なのか？
それによって、発表内容が 当然異なる
”Season A - Apr-June, 2027”だから
今後1年 2027年7月にLANA報告だとすると遅い
なので、2027年7月にLANA報告を待たずに
議論をオープンにしないと、みんな困惑する
議論をオープンにすれば、その情報をベースにあとは各人が自己責任で考えることができる
状況は、悪いながらも それが最善だろう
URLﾘﾝｸ(ahgt.math.cnrs.fr)
Arithmetic, Homotopy, and Geometry 2027-28
Scientific Program & Seasons
Season A - Apr-June, 2027
Homotopy, rationality, and geometry
Season B - Sept-Nov, 2027
The homology-homotopy frontier in arithmetic geometry
Season C - Feb.-March, 2028
Combinatorial arithmetic geometry
Scientific committee: B. Collas° (RIMS Kyoto, JP), P. Dèbes (Lille, FR), B. Fresse (Lille, FR), Y. Hoshi (RIMS Kyoto, JP), M. Kim (ICMS Edinburgh, UK), A. Mézard (IMJ-PRG, FR) & A. Tamagawa (RIMS Kyoto, JP) - ° indicates lead.
586:１３２人目の素数さん
26/07/28 09:18:58.92 3yi27Rrd.net
また無内容
587:１３２人目の素数さん
26/07/28 09:20:56.65 xkDIbBjR.net
>>585
数学の論文が読めない素人には分からんだろうが
そもそもIUTはなかったものとしてすすめられている
だから、たんたんとIUTの"死亡宣告"を待てばよい
588:１３２人目の素数さん
26/07/28 10:19:42.82 GrrSkgiT.net
もどる
>>242-245 より抜粋
ID:13yLpBZq さんの労作
(引用開始)
Claude Opus4.8とFable5使ってIUTを1から地道に検証するプロジェクトを個人的にこの一ヶ月やってみたがFable5の言い分は以下だった
IUT理解者に対する要請部分のみを書く
4. 要請
以下のいずれか一つをご教示いただきたい:
(A) 箇所の特定: (P) が(定義的措定ではなく)導出されている箇所 —— 論文・節・命題/Remark 番号 —— の特定。 すなわち、ラベル配置「テータ値 q^{j²} が j 成分に置かれる」から 受信側測度の主張「その可能な像の包が深さ ⌊j²·ord(q)－d－a⌋－b の領域に含まれ、 その体積が同じ正規化で q-標対象と比較可能である」への移行が遂行されている箇所。
(B) 機構の提示: (A) が「複数箇所の組合せから従う」場合、その組合せの明示 —— 各ステップが (i) 特定された構造の間の同型、(ii) 特定された正規化での体積計算、 (iii) 特定された領域の包含、のいずれかである形の命題列+証明の概略。
(C) 同値な別形: 実曲線(の無限族)に対する評価 L ≥ (l(l+1)/12 － 1)·|log(q)| の導出 (F3 により (P) の一様供給とこれは同値である)。
5. 予備的注記(想定される応答について)
略
6. 検証のコミットメント
(A)(B)(C) のいずれかが供給されれば、我々はそれを既存の形式化 (受け口となる構造は実装済み)に接続して機械検証することを約束する。
導出が成立すれば、検証結果は「Thm 3.11 ⟹ Cor 3.12 の連鎖は結論の独立な導出を含む」 —— すなわち望月理論側の確定 —— に翻り、その旨を同じ厳密さで記録する。
本要請は反駁ではなく、係争を機械検証可能な一点に絞り込んだ上での、 その一点についての情報提供の依頼である。
2. 論点の単離: ただ一つの入力
上記を全て投入すると、「Thm 3.11 ⟹ Cor 3.12 ⟹ 高さ不等式」の連鎖の検証は、 次の一命題の導出に正確に還元される(これが我々の主定理群の内容である):
(P) [IUTchIV] Thm 1.10 証明 Step (v) において、Θ-標対象の可能な像の合併 (indeterminacies (Ind1), (Ind2), (Ind3) 込み)が、v_j ∈ V^bad の成分で λ := ord(q^{j²}) とした容器 φ(p^λ·(R_I)~) ⊆ p^{⌊λ－d_I－a_I⌋}·log_p(R_I^×) に含まれる —— ここで体積は、[IUTchIII] Cor 3.12 証明 Step (xi-d)–(xi-f) で q-標対象の測定に用いられるものと同一の procession 正規化 mono-analytic 対数体積(受信側 (1,◦) の正規化)である
(P) を認めれば以降は全て機械的に従う(検証済み)。問題は (P) 自身の導出である
(引用終り)
589:１３２人目の素数さん
26/07/28 10:54:11.24 GrrSkgiT.net
>>588 補足
これで
ID:13yLpBZq さん Claude Opus4.8とFable5使っての分析では
”「Thm 3.11 ⟹ Cor 3.12 ⟹ 高さ不等式」の連鎖の検証は、 次の一命題の導出に正確に還元される(これが我々の主定理群の内容である):”
”(P) を認めれば以降は全て機械的に従う(検証済み)。問題は (P) 自身の導出である”
１）要するに、「Thm 3.11 ⟹ Cor 3.12 ⟹ 高さ不等式」の部分が問題
”(P) を認めれば以降は全て機械的に従う(検証済み)。問題は (P) 自身の導出”
２）なので、IUTのThm 3.11までは、OK
３）「Thm 3.11 ⟹ Cor 3.12 ⟹ 高さ不等式」で
”6. 検証のコミットメント
(A)(B)(C) のいずれかが供給されれば、我々はそれを既存の形式化 (受け口となる構造は実装済み)に接続して機械検証することを約束する。
導出が成立すれば、検証結果は「Thm 3.11 ⟹ Cor 3.12 の連鎖は結論の独立な導出を含む」 —— すなわち望月理論側の確定 —— に翻り、その旨を同じ厳密さで記録する。”
なので
>>588の(A)(B)(C) のいずれか を 提供せよ が、Claude Opus4.8とFable5からの結論だが
LANAの現時点での 結論はどうか？ そこの細部を オープンにした方が良いだろう
もう一つは、Leanコードの公開な
公開すれば、だれかがAI走らすかもしれんが、それはそれで仕方ない
(参考)
>>339より再録
転載：ID:dythpcIC さん、ありがと
URLﾘﾝｸ(rio2016.5ch.io)
2026/07/17(金) 14:18:47.39 ID:dythpcIC
LANAプロジェクトに一定の敬意を払いつつも
逃げ腰でLEANの公開なしってのは流石にどうかと思ったから俺のOpus4.8とFable5で作った
プロトタイプ、スケルトン、未完成、言い方は何でも良いが公開しとくわ
コメントはほぼ日本語なんで海外勢向けではないがな
まぁAIに読み込ませてコメント英語化するとか容易だろうし許せ
URLﾘﾝｸ(github.com)
Opus4.8とFable5で作ったIUTの形式化
590:１３２人目の素数さん
26/07/28 10:54:20.54 Qb5wOfI3.net
これからiutが数学者の議論の俎上に上がるとすれば、基礎論教育の必要性とか、leanのような形での証明の提出の義務化をどうするかとかでの過去事例とかで上がるくらいやろな
591:１３２人目の素数さん
26/07/28 11:02:44.96 GrrSkgiT.net
>>589 補足
念押し
”>>588の(A)(B)(C) のいずれか を 提供せよ”
の達成とか
その他
なんらかの形で IUTのギャップが
埋まる可能性は 大いにあると見ています （＾＾
592:１３２人目の素数さん
26/07/28 12:28:11.80 W5E/+Q+m.net
「(P) [IUTchIV] Thm 1.10 証明 Step (v) において、
Θ-標対象の可能な像の合併 (indeterminacies (Ind1), (Ind2), (Ind3) 込み)が、
v_j ∈ V^bad の成分で λ := ord(q^{j²}) とした容器 φ(p^λ·(R_I)~) ⊆ p^{⌊λ－d_I－a_I⌋}·log_p(R_I^×) に含まれる ——
ここで体積は、[IUTchIII] Cor 3.12 証明 Step (xi-d)–(xi-f) で q-標対象の測定に用いられるものと同一の
procession 正規化 mono-analytic 対数体積(受信側 (1,◦) の正規化)である」
(P)が証明できないので望月真一は死んだ
593:１３２人目の素数さん
26/07/28 12:31:48.95 W5E/+Q+m.net
もう、10年以上前の2015年からここで止まってる
要するに2015年に既に死んでいる
594:１３２人目の素数さん
26/07/28 12:32:48.45 W5E/+Q+m.net
2018年にはScholzeとStixにより具体的に指摘されている
要するに2018年に死亡宣告されている
595:１３２人目の素数さん
26/07/28 12:51:54.57 GrrSkgiT.net
こういうとき
やるべきことは一つで
決まっている
事実を冷静に見つめること
そのために、事実を隠さずに公開すること
みなで議論すること
596:１３２人目の素数さん
26/07/28 13:31:21.90 3yi27Rrd.net
事実を冷静に見つめた結果IUTは終わった
597:１３２人目の素数さん
26/07/28 16:09:10.42 oI5rxyHc.net
出すも何もlanaが出さないんだから議論のしようもないわな
このままなんも出なくて終わりやろな
598:１３２人目の素数さん
26/07/28 16:47:51.79 vnZMvZgk.net
最後には出るのでは？ソレが目的の1つでしたし
599:１３２人目の素数さん
26/07/28 17:14:40.46 FP8AsHWZ.net
他責メンヘラおじさん望月
「ボクは悪くないも〜んみんながいじめる〜
ショルツが〜スティックスが〜
あいつらは学部レベルもわかってないバカです(キリッ」
↑情けないにも程があるだろw
600:１３２人目の素数さん
26/07/28 17:47:20.95 FP8AsHWZ.net
他責メンヘラおじさん望月
「ボクは悪くないも〜んみんながいじめる〜
ショルツが〜スティックスが〜
あいつらは学部レベルもわかってないバカです(キリッ」
↑情けないにも程があるだろw
601:１３２人目の素数さん
26/07/28 17:56:18.52 3Y4+2uQh.net
事実を冷静に見つめ
事実を隠さず公開し
みなで議論した結果
ＩＵＴ死す
602:１３２人目の素数さん
26/07/28 18:12:25.18 GrrSkgiT.net
>>595 追加
人生 ピンチはチャンスでもある
IUTは、ここを突破すれば、ひと皮むける 脱皮して 成虫になる
そう思って、がんばってください→望月先生たち
夜明けは近い
603:１３２人目の素数さん
26/07/28 20:30:07.86 yTgttQOx.net
⚫︎2018年.
森重文京大教授のscholzeへ提案より数理研でscholze.stix.望月.星の4者ミーティング。
・個人的に、scholzeは"abc予想の証明へ近づく重要なアイデアは本当に見られなかった"と述べた。
quanta magazine 2018.9.20
⚫︎2019年.
1 望月新一。
川上量生が企画した望月新一監修加藤文元著IUT本刊行。
・本文 P37
>ワイルズの理論と望月教授の理論の違いは、、要するに言葉の違いです。
望月教授は、言うなれば、だれも 話したことがない、新しい言語を 用いて理論を組み立てました。
・本文 IUT語 p51
>IUT理論は、一般的な数学の パラダイムの枠内では語れない、
全く新しいフレームワークと言語・ 概念体系を基盤として構築されている
2 scholze。
>Scholze .Clausenは「凝縮集合」と名付けて研究を開始。
2019年4月、ショルツェはボン大学で「凝縮数学（condensed mathematics）」に関する講義を開始し、5月には77ページにわたるノートを公開した。
そのノートは、「コヒーレント双対性（coherent duality）」と呼ばれる重要な定理に対する、新しく洗練された証明へと結実していた。
後にショルツェと共同研究を行うヨハン・コメリンの回想「コヒーレント双対性については、それまでは極めて回りくどく技術的な証明しかなかった」。ショルツェとクラウセンの証明は、明快かつ優雅なものだった。
deepl
➖
condensed mathematics. condensed set
URLﾘﾝｸ(www.quantamagazine.org)
604:１３２人目の素数さん
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]。