26/07/23 10:47:22.98 1JAnhQP1.net
>>434-442
>いずれにせよこれで一段落ということにしてはどうか
>suspendedと思った者は皆無に等しい
ID:5zPtkw66 は、御大か
巡回ありがとうございます
コメントありがとうございます。
１）まあ、それをリアル界で決めるのは、望月・星氏らでしょう
ここは、バーチャル 場末の５ｃｈです
２）私見ですが、先週7/17金のLANAプロジェクトの中間発表は
3.11→3.12導出が 現状ではLean形式化に乗らなかったが
可能性は残っているという
３）その可能性とは、おそらく 遠アーベルのLeanライブラリー不足で
Leanライブラリーを 何らか追加するとか
あるいは別に、3.12そのものではなく 3.12をなんらか変形して IUT IVを導けるようにすること
４）さて、まずこの状況（中間発表）を受けて、望月・星氏らが彼ら自身の見解と見通しを発表すべきでしょうね
というのは、日仏合同の Arithmetic & Homotopic Galois Theory IRN 共同研究プロジェクトが走っている URLﾘﾝｸ(ahgt.math.cnrs.fr)
ここには、日本の予算もさることながら 仏の予算も入っている。その落とし前が必要となる
５）ところで 数学では「数列の収束加速法」が、古代から研究されている （＾＾
いまの場合、事態の収束加速法は、事実を隠さずにオープンにして 議論することですね
Leanコードも隠さずに、オープンにして 議論することが、収束加速の要諦でしょう！
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
数列の加速法
収束の遅い数列を収束の速い数列に変換するアルゴリズムの総称である[1]
歴史
19世紀以前
ヨーロッパと日本で研究が始まった。古典的な二つの加速法はオイラー変換[2] と クンマー変換である。日本では関孝和、建部賢弘など、ヨーロッパではアイザック・ニュートンなどが取り組んだ[3]。
446:１３２人目の素数さん
26/07/23 12:31:09.48 j87TBArl.net
>>445
こいつが国粋🐎🦌のSet Aか
>それをリアル界で決めるのは
LANAプロジェクト
そしてもうほぼアウト
>先週7/17金のLANAプロジェクトの中間発表は
>3.11→3.12導出が 現状ではLean形式化に乗らなかった
もう何年もギャップだといわれていて
改めてそれが分かった時点で、ほぼアウト
>が、可能性は残っている
ダメだという証明ができないだけの話でしかない
実際は、まあアウト
>おそらく 遠アーベルのLeanライブラリー不足で
遠アーベルではなく宇宙際の理論がない
>Leanライブラリーを 何らか追加するとか
何年もそういわれつづけて何もできてないが
>あるいは別に、3.12そのものではなく 3.12をなんらか変形して IUT IVを導けるようにすること
諦めろ 国粋🐎🦌
447:１３２人目の素数さん
26/07/23 12:33:27.39 j87TBArl.net
>>446
>さて、まずこの状況（中間発表）を受けて、
>望月・星氏らが彼ら自身の見解と見通しを
>発表すべきでしょうね
切腹しろってか？（笑）
>というのは、日仏合同の共同研究プロジェクトが走っている
>ここには、日本の予算もさることながら 仏の予算も入っている。
>その落とし前が必要となる
自●しろってか？
Set A おまえは自●しなくてええんか 国賊
448:１３２人目の素数さん
26/07/23 12:38:14.81 p5pZvalq.net
国粋野郎は国賊でしたとさ（嘲）
449:１３２人目の素数さん
26/07/23 12:45:44.91 4ighMvmG.net
>>448
ドワンゴ周りは国粋じゃなくて
旧満州(北朝鮮＆中国瀋陽)由来の朝鮮人偽右翼だとあれほど
450:１３２人目の素数さん
26/07/23 12:46:15.69 4ighMvmG.net
IUTGtrのプーアノンばりのアイコンで爆笑した
451:１３２人目の素数さん
26/07/23 12:59:16.78 p5pZvalq.net
>>449
アイシンギョロとかいう女真族ではなく？（笑）
452:１３２人目の素数さん
26/07/23 13:13:31.49 pntzDx39.net
後金
453:１３２人目の素数さん
26/07/23 13:37:08.08 2lT1ceCI.net
望月＝頭の良いクズ
セタ＝頭の悪いクズ
454:１３２人目の素数さん
26/07/23 15:44:59.19 1JAnhQP1.net
>>445 追加
ゴミが湧いているが、ムシムシ
こういうとき
危機管理（下記の存立危機事態までは行ってないだろうがｗ）
１）事実の把握
そのために、関係者の招集をする
望月、星、加藤文元、玉川、山下・・などなど
（一部の人はwebでも可だろうが）
２）そこで状況を説明して 事実共有をする
Leanコード公開などを決める
３）その後の行動計画を議論する
施策と役割分担（宿題分担）を決める
次に集まる日時を決める
これを必要なだけ繰り返す
まあ、みんなで知恵をだせば、なんとかなるっぺよ
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
存立危機事態
台湾有事をめぐる議論
→「高市早苗による台湾有事発言」を参照
455:１３２人目の素数さん
26/07/23 16:25:37.31 2lT1ceCI.net
アホ
456:１３２人目の素数さん
26/07/23 16:39:05.20 fAGcExUh.net
>>454
既に原爆が落とされてる状況で
本土決戦とかいってる🐎🦌
457:１３２人目の素数さん
26/07/23 16:43:03.74 m/0H6KbX.net
1945年7月26日に、英中米の3か国はポツダム宣言を発し、日本軍の無条件降伏を要求した。
日本政府は、日ソ中立条約があるソ連に和平講和の仲介を託していたが、
8月6日に広島市に原子爆弾が投下され、8月8日未明にソ連対日宣戦布告、
8月9日に長崎市にも原子爆弾が投下されるという重大事態が続いた。
8月10日午前0時3分[2]から行われた御前会議での議論は、
東郷茂徳外相、米内光政海相、平沼騏一郎枢密院議長は、
天皇の地位保障のみを条件とするポツダム宣言受諾を主張、
それに対し阿南惟幾陸相、梅津美治郎陸軍参謀総長、豊田副武軍令部総長は
「受諾には多数の条件をつけるべきで、条件が拒否されたら本土決戦をするべきだ」
と受諾反対を主張した。
しかし、唯一の同盟国となっていた大ドイツ国政府が5月8日に無条件降伏したことで、
イギリスとアメリカ、オーストラリアやカナダなどの連合軍は日本本土に迫っており、
さらに唯一の頼みの綱であった元中立国のソ連も先日の宣戦布告により日本への侵攻を開始しており、
北海道上陸さえ時間の問題であった。
ここで鈴木貫太郎首相が昭和天皇に発言を促し、天皇自身が和平を望んでいることを直接口にしたことにより
御前会議での議論は降伏へと収束し、8月10日の午前3時から行われた閣議で承認された。
458:１３２人目の素数さん
26/07/23 16:47:22.05 m/0H6KbX.net
日本政府は、ポツダム宣言受諾により全日本軍が降伏を決定する事実を、
8月10日の午前8時に海外向けのラジオ国営放送を通じ、
日本語と英語で3回にわたり世界へ放送し、同
盟通信社からモールス通信で交戦国に直接通知が行われた。
中立国の加瀬俊一スイス公使と岡本季正スウェーデン公使より、
8月11日に両国外務大臣に手渡され、両国より連合国に渡された。
しかしその後も日本政府と軍内部、
特に鈴木首相や東郷外相らと阿南陸相ら陸海軍の上層部内で意見が紛糾し、
御前会議での決定を知らされた陸軍省では、
天皇の元の会議で決定されたにもかかわらず、
徹底抗戦を主張していた多数の将校から激しい反発が巻き起こった。
8月12日午前0時過ぎ、連合国はアメリカのジェームズ・F・バーンズ国務長官による返答、
いわゆる「バーンズ回答」を行った。その回答を一部和訳すると
「降伏の時より、天皇及び日本国政府の国家統治の権限は、
降伏条項の実施の為其の必要と認むる処置を執る連合軍最高司令官に『subject to』する」
というものであった。
外務省は「subject to」を「制限の下に置かれる」だと緩めの翻訳・解釈をしたが、
参謀本部はこれを「隷属する」と曲解して阿南陸相に伝えたため、
軍部強硬派が国体護持について再照会を主張し、鈴木首相もこれに同調した。
8月13日午前9時から行われた、軍と政府の最高戦争指導会議では
「バーンズ回答」をめぐり再度議論が紛糾した上、
この日の閣議は2回行われ、2回目に宣言の即時受諾が優勢となった。
459:１３２人目の素数さん
26/07/23 16:48:59.55 m/0H6KbX.net
8月14日午前11時より行われた再度の御前会議では、
まだ阿南陸相や梅津陸軍参謀総長らが戦争継続を主張したが
（この時阿南陸相や梅津陸軍参謀総長は陸軍内でクーデターが起こることを認知していた）、
昭和天皇が「私自身はいかになろうと、国民の生命を助けたいと思う。
私が国民に呼び掛けることがよければいつでもマイクの前に立つ。
内閣は至急に終戦に関する詔書を用意して欲しい」と訴えたことで、
鈴木首相は至急詔書勅案奉仕の旨を拝承し、
14日夕方に閣僚による終戦の詔勅への署名、
深夜に昭和天皇による玉音放送が録音された。
夕方に加瀬スイス公使を通じて、宣言受諾に関する詔書を発布した旨、
受諾に伴い各種の用意がある旨が連合国側に伝えられた。
460:１３２人目の素数さん
26/07/23 16:50:14.21 p5pZvalq.net
8月15日正午の昭和天皇による玉音放送をもって、
改めてポツダム宣言受諾を全国民と全軍に表明し、
戦闘行為は停止された。
昭和天皇がラジオで国民に向けて直接話すのは
これが初めてのことであった。
461:１３２人目の素数さん
26/07/23 17:08:41.95 n/8j5UZO.net
(譫言しか書かなくなったか)
462:１３２人目の素数さん
26/07/23 17:13:48.69 RrXTUC0u.net
いやー、本当にこの時代に生まれてラッキーだった。
この国に生まれてね。
463:１３２人目の素数さん
26/07/23 17:26:54.36 n/8j5UZO.net
ワイドショー的週刊誌的な興味対象でしかなくなった数学を見ることになるのをラッキーとはね
464:１３２人目の素数さん
26/07/23 20:36:01.84 r0btaSCl.net
>>455-462
さすが 場末の5ch 過疎数学便所板だね
素人が好き放題書いている
>>463
>ワイドショー的週刊誌的な興味対象でしかなくなった数学を見ることになるのをラッキーとはね
まったくね
数学にAIが入り込んできています
今後の展開やいかに
465:１３２人目の素数さん
26/07/23 20:43:24.94 RrXTUC0u.net
（あち～）
466:１３２人目の素数さん
26/07/23 20:53:46.59 RrXTUC0u.net
素人でない書き込みの見本が見てみたいところw
参考にさせて頂きたい。
467:１３２人目の素数さん
26/07/23 22:14:49.09 2lT1ceCI.net
>>464
x,yが集合ならx^yも集合ですよど素人さん
468:１３２人目の素数さん
26/07/23 22:18:41.77 RrXTUC0u.net
なるほど、素人じゃなくてド素人だったのか！
な～んちゃってw
469:１３２人目の素数さん
26/07/24 00:07:10.29 /RjtiMHB.net
>『Qを構成した瞬間に有理数列全体の集合 Q^N も存在しており、作る必要など無い』か・・
>独自説だねぇ～、ユニークで笑える、が面白すぎｗｗ（＾＾
↑
ど素人がなんか言ってます
470:１３２人目の素数さん
26/07/24 07:59:16.77 wCcHV2Pm.net
>>466
>素人でない書き込みの見本が見てみたいところw
>参考にさせて頂きたい。
当然、わたくしめも、素人だが
プロ数学者は、ここでは 知る限り御大（名誉教授）くらいだが
彼は、主に お天気日誌を書いています（＾＾
おっと、めずらしく お天気日誌以外のコメントを書かれたね
>>445 より
>いずれにせよこれで一段落ということにしてはどうか
>suspendedと思った者は皆無に等しい
だね
多分、今回のLANA中間発表で 一段落（ある程度の結論は出た）という意見
まあ、これが本因坊戦とすれば 5番勝負の第一局は LANAチームの中押し勝ち！
次の対局を始めろということでしょうねｗ （＾＾
471:１３２人目の素数さん
26/07/24 09:30:25.36 /RjtiMHB.net
>当然、わたくしめも、素人だが
何を己惚れてるのか 君はど素人だよ
x^yが集合であることは理解できた？
472:１３２人目の素数さん
26/07/24 09:42:41.67 pd0or1JQ.net
>>471
で、君は？
どど ど素人かね？ｗｗｗ
473:１３２人目の素数さん
26/07/24 09:44:41.66 B7dUo32s.net
下らん
474:１３２人目の素数さん
26/07/24 09:45:35.86 pd0or1JQ.net
>>471
私の見るところ
君は、囲碁でいうセイモクだなｗｗｗ
475:１３２人目の素数さん
26/07/24 15:53:39.41 pd0or1JQ.net
Benjamin. Collas 氏なども
しっかり、望月・星氏らを叱咤激励してやってください
よろしく
衆知を合わせて問題解決を お願いします （＾＾
URLﾘﾝｸ(ahgt.math.cnrs.fr)
Arithmetic & Homotopic Galois Theory IRN
Org.: B. Collas (RIMS, JP), Y. Hoshi (RIMS, JP), K. Sawada (RIMS Kyoto), P. Dèbes (Lille, FR), A. Mézard (ENS, FR).
URLﾘﾝｸ(www.kurims.kyoto-u.ac.jp)
COLLAS, Benjamin
Since 2023 this activity takes place in the CNRS France-Japan International Research Network LPP-RIMS ``Arithmetic & Homotopic Galois Theory'' (AHGT), see AHGT seminar and workshops, and AHGT references and publications.
476:１３２人目の素数さん
26/07/24 17:25:35.26 /RjtiMHB.net
ファルティングスは優しいね。
「論文は理解できなかった。 自分の研究に時間を割くことにした」
「数学になってない」と切って捨てるのではなく「自分の理解力が及ばない」とも解釈可能な表現で望月を傷つけることなくやんわりと距離を取っている。
フィールズ賞受賞者で人格者でもある。弟子とは大違いだね。
477:１３２人目の素数さん
26/07/24 18:44:38.86 ELp+18O9.net
グロタンディークの名前が付いてたから一部のアホどもが有り難がってただけで
結局尊師のやったことって特殊な小さい問題ひとつ解いただけでしょ
甘やかしてきた取り巻きたちが尊師を増長させ続けて今回のような日本の恥晒しにまで行き着いてしまったわけだな
478:１３２人目の素数さん
26/07/24 18:54:27.91 ELp+18O9.net
グロタンディークの名前が付いてたから一部のアホどもが有り難がってただけで
結局尊師のやったことって特殊な小さい問題ひとつ解いただけでしょ
甘やかしてきた取り巻きたちが尊師を増長させ続けて今回のような日本の恥晒しにまで行き着いてしまったわけだな
479:１３２人目の素数さん
26/07/24 21:26:14.80 wCcHV2Pm.net
関連 コピーしておきます
URLﾘﾝｸ(plaza.rakuten.co.jp)
新一の「心の一票」2026.01.01
Leanによる形式化は、長期的な検証や説明責任を可能にする記録装置となり得るか？
カテゴリ：研究関連の現状報告 URLﾘﾝｸ(plaza.rakuten.co.jp)
前回の記事では、定理証明支援系ソフトLeanに関連した活動が昨年後半、（私を含め）私の周辺において益々活発になっていることについてご報告しましたが、今回の記事では、少なくとも私の現在の認識において、このような活動に関わることにどのような意義があるかについて検証し、解説していきたいと思います。
略す
昨年後半、理論の形式化に関する議論を、Leanの専門家と進める上においても、Leanに関する技術的な問題という面においてはこれまでの事例と違うものの、再び同様の事象が見られました。（これについては、以下の「species/mutations」に関する解説をご参照いただきたい。）
略す
Leanに対する、通常の考え方と多少違う方向性の活用方法の話に戻りますが、[Rpt25]§3.1で解説している通り、略
宇宙際タイヒミューラー理論の場合、最も基本的な用語・概念は間違いなく、「関手的アルゴリズム」（＝「functorial algorithm」）ということになります。この用語ないしは概念は、本当は、宇宙際タイヒミューラー理論だけでなく、数理研において1990年代半ばから盛んになっている流儀の遠アーベル幾何全般において、非常に基本的な立ち位置にあるものです。
この「関手的アルゴリズム」という概念は、宇宙際タイヒミューラー理論の原論文4編の第4論文[IUTchIV]の§3で解説している「species/mutations」という概念によって定式化されており、つまり、理論の形式化を進める上においても、まずしっかり押さえておきたいのは、「species/mutations」の形式化ということになります。因みに、技術的な詳細に関しては、[IUTchIV]§3をご参照いただきたいと思いますが、簡単に嚙み砕いて説明すると、
・species（＝「種」）は、集合論的論理式で定義される、「数学的対象の種類」（＝つまり、「群」、「環」、「代数多様体」のようなもの）で、
・mutation（＝「突然変異」）は、集合論的論理式で定義される、あるspeciesから別のspeciesへの変換、つまり構成の手順
ということになります。つまり、「関手的アルゴリズム」というのは、より技術的な用語で表現すると、まさしく「mutation」ということになります。
つづく
480:１３２人目の素数さん
26/07/24 21:26:41.47 wCcHV2Pm.net
つづき
私自身、2010年～2011年頃、[IUTchIV]§3を執筆したとき、species/mutationは、特に難しい話でもなく、取り立てて新奇性のある話でもなく、多くの数学者が当たり前に脳内で無意識のうちにこなしている処理を、（同様の概念が明示的に記述されている適切な文献が見付からなかったために）ただ自分で明示的に記述してみただけのものに過ぎないという認識でした 略
一方で、species/mutationの、Leanによる形式化の可能性について調べ始めた途端、全く想定外の展開に見舞われてしまいました。まず、species/mutationの定義では、集合論的な（＝つまり、いわゆるZFCの）論理式が非常に中心的な役割を果たしますが、これまでのLeanの標準とされているライブラリMathLibでは、ZFCモデル（＝つまり、標準的な集合論のモデル）は用意されているため、特定の集合に対する特定の論理式をLean上で扱うことが可能となっていますが、一方で、species/mutationの理論において本質的な役割を果たす「不定元のような論理式」（＝特定されていない、「とある論理式Φ」のようなもの）を扱うには、一階述語理論としてのZFCが必要であり、それはMathLib上ではまだ掲載されていないということが判明しました。
略
(引用終り)
以上
481:１３２人目の素数さん
26/07/24 21:30:09.55 wCcHV2Pm.net
私見だが
早く Leanによる形式化の詳細を公開して
みんなで議論して、早く前進させた方が良いと思う
ある方法がだめでも
おうおうにして
別の手段があるものです
482:１３２人目の素数さん
26/07/24 21:37:08.87 /RjtiMHB.net
アホ
483:１３２人目の素数さん
26/07/24 21:45:13.30 S3KDKg/8.net
アッポー
484:１３２人目の素数さん
26/07/24 21:46:28.52 Dnxx1y9G.net
ほんとはなんもやってないんだよ
485:１３２人目の素数さん
26/07/24 23:02:38.54 Ey8rJ4AB.net
>>481
できてないのバレちゃうじゃん
486:１３２人目の素数さん
26/07/24 23:06:37.17 B7dUo32s.net
species/mutationという用語を見てちょっと説明聞いて最初思ったのは
これcategoryとfunctorじゃないのってことだったけど
speciesはcatetoryのobjectだけをイメージしてるのかね？
morphismは考えてない？
487:１３２人目の素数さん
26/07/25 02:06:23.75 XoBvX2Rg.net
>>480
>（＝特定されていない、「とある論理式Φ」のようなもの）
「のようなもの」じゃ形式化は出来ないだろ
それから形式化の仕事してるなら論理式なんて非専門用語は使わずに
命題なのか述語なのかはっきりさせないと
述語に量化記号使うなら二階述語論理になるし
大丈夫ですか
数学屋はたとえ公理の数を有限無限個にしても一階述語論理に閉じこもることを好むが
計算機科学屋はsystem Fとか昔から高階トポスに親しんでる人が多い
一階つまりエレメンタリートポスで充分なのかどうかはLean関係なく数学的な議論ができる
圏論的には量化をスライス圏における随伴関手として扱うのは当然知ってるだろうしそこまで難しくないだろ
そこをはっきりさせてくれないと形式化なんて無理
「のようなもの」なんて論外
まあIUT関連の論文ではよく出てくる言葉なんだけどw
488:１３２人目の素数さん
26/07/25 07:07:32.31 bmdqsgm3.net
>>487
>「のようなもの」じゃ形式化は出来ないだろ
∃φ
みたいなのを必要とすると言いたいのではナイかな
489:１３２人目の素数さん
26/07/25 08:39:56.42 AuqA/R3q.net
>>485
>できてないのバレちゃうじゃん
いや、それが大切だと思うんだ
つまり、出来ていることと、出来ていないこと
これを明確にして、公表するべし！
490:１３２人目の素数さん
26/07/25 10:07:28.06 AuqA/R3q.net
下記、向こうのスレからだけど
ほんと 同意で そう思う
IUT I～IVは、望月氏の単著だから 望月氏が決断すれば良いだけ
「Leanコード出来たところまで、公開します！」とやればいい
そうして、広く みなで議論するべし
いまや、仏国まで巻き込んだ 一大遠アーベルプロジェクトになっているんだから
オープンな議論をしていかないと いけない
と思うよ
(参考)
URLﾘﾝｸ(rio2016.5ch.io)
2026/07/25(土) ID:ncTQQ9AA
>> 509
>アイデア自体が無力なので修正・補強は無意味なのよ
ABCに対するアプローチ方法としては面白いとは思うけどな
ディオフォントス幾何においては遠アーベルとかじゃ無いとABCに接近出来ないのは研究者からしたらほぼほぼ気づいてることだし
>abcが出るくらい非自明な主張を証明なしに使っていただけ
その主張に証明を与えればいいんでしょ
数学によくある予想の置き換えというか、もとからある予想Aは予想Bと等価ということを証明すること自体に意味がある
あとは予想Bを証明するか何なら予想Bが新たな予想Cと等価だと証明して予想Cを証明するだけ
ABC予想関連で不毛だなと思うのは望月先生の証明を議論すること
さっさとABC予想はコレコレの形の予想を証明すると自動的に成立するから、望月の研究ではそれを確認しただけ
さあ皆さんコレコレの形の予想を証明、反証しましょうねで済む話
491:１３２人目の素数さん
26/07/25 11:14:22.89 +LSaq+7s.net
>特定されていない、「とある論理式Φ」のようなもの
算術におけるゲーデル数のアイデアを集合論へ適用すればよくね？
有限種類の記号の有限列であるところの論理式と集合との1対1対応を定義できるだろうから、論理式（に対応する集合）全体の集合 Form を定義できて、∃φ∈Form とすればよくね？
492:１３２人目の素数さん
26/07/25 11:22:54.15 +LSaq+7s.net
>一階述語理論としてのZFCが必要であり、それはMathLib上ではまだ掲載されていないということが判明しました。
ん？ 一般的なZFCは一階述語理論としてのZFCじゃないの？ 何を言ってるんだろう？
493:１３２人目の素数さん
26/07/25 13:42:05.74 AuqA/R3q.net
>>490 追記
下世話な話だが
望月氏は、世事に疎いみたいなので書いておくと
IUTがLean形式化がパスしないと
世間からは、IUT証明はしっぱいと判定されるだろう
が、後付けでも ロジック追加で Lean形式化のギャップを埋めることができれば
一応格好はつく
さて、IUT証明しっぱいと判定されて困ることは
・まず、望月研の院生が困る
（あの有名な望月研か と言われるか 悪名高い望月研出身かとなるかのちがい）
フェセンコ氏や彼の弟子 周忠鵬も同じ
・RIMS のIUT論文別冊出版のとき
巻頭に編集者連名で「ちゃんと審査したので大丈夫」宣言を書いた
柏原先生が 筆頭だったが、10名くらい居たはず
・遠アーベルプロジェクト
”Arithmetic & Homotopic Galois Theory IRN” URLﾘﾝｸ(ahgt.math.cnrs.fr)
ここに 仏国の人もいるから、おおげさには国際問題
そんなこんなで 繰り返すが
後付けでも Lean形式化のギャップを埋めることができれば 一応格好はつく
が もしダメでも それは仕方ない。人間だもの
（スポーツなら 後のVAR判定で再逆転もありかも）
ともかく、事態の収束を加速する必要がある
494:１３２人目の素数さん
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月に設置された。