Inter-universal geometryとABC予想(シン応援スレ) 92

前スレ：Inter-universal geometryとABC予想(シン応援スレ) 91
https://rio2016.5ch.io/test/read.cgi/math/1777882286/
詳しいテンプレは、下記旧スレへのリンク先ご参照
Inter-universal geometry と ABC予想 (応援スレ) 52
://rio2016.5ch.net/test/read.cgi/math/1613784152/1-13

（2030 ICM 日本開催に向け 力をためようということか）
https://www.mathunion.org/icm/icm-2026
ICM 2026
https://www.icm2026.org/event/ac193975-5d24-4628-8c30-ddb23de19a8b/catalog
Titles & Abstracts

https://ahgt.math.cnrs.fr/news/index.html
News of the AHGT project [Special year]2027-2028
Special year ``Arithmetic Homotopy Geometry'' at RIMS Kyoto, April 2027-March 2028.
Three Seasons: with main conferences, introductory lectures, and workshops

＜2026年は 数学でもAIの時代になるかもです。そういう兆候が2025年から顕著になっていますですｗ （＾＾； ＞
＜IUT最新文書＞
・News – Ivan Fesenko https://ivanfesenko.org/?page_id=80
・望月新一＠数理研 https://www.kurims.kyoto-u.ac.jp/~motizuki/
https://ja.wikipedia.org/wiki/%E5%AE%87%E5%AE%99%E9%9A%9B%E3%82%BF%E3%82%A4%E3%83%92%E3%83%9F%E3%83%A5%E3%83%A9%E3%83%BC%E7%90%86%E8%AB%96
宇宙際タイヒミュラー理論 ＜新展開＞ 2025年5月、中国の若手数学者の周忠鵬はフェルマーの最終定理の一般化がIUT理論から得られると発表した
・日仏遠アーベル共同研究 Arithmetic & Homotopic Galois Theory IRN https://ahgt.math.cnrs.fr/activities/
＜Grokipedia＞
Inter-universal Teichmüller theory https://grokipedia.com/page/Inter-universal_Teichm%C3%BCller_theory
遠アーベル幾何学 https://grokipedia.com/page/Anabelian_geometry
アーベル圏 abelian category Grokipedia https://grokipedia.com/page/Abelian_category

https://zen.ac.jp/lp/icp
IUT Challenger Prizeの紹介 2023年7月
審査の対象とする論文については、MathSciNetに載っていて、かつ、過去10年間に数論幾何の論文が10本以上掲載されている数学の専門誌に査読の上でアクセプトまたは掲載されたもの

://ahgt.math.cnrs.fr/activities/
Anabelian Geometry and Representations of Fundamental Groups. Oberwolfach workshop MFO-RIMS Sep. 29-Oct. 4, 2024
Org.: A. Cadoret, F. Pop, J. Stix, A.. Topaz （J. Stix IUT支持側へ）

://collas.perso.math.cnrs.fr/documents/Collas-Anabelian%20Arithmetic%20Geometry-IUT.pdf
“ANABELIAN ARITHMETIC GEOMETRY - A NEW GEOMETRY OF FORMS AND NUMBERS: Inter-universal Teichmüller theory or “beyond Grothendieck’s vision” Benjamin Collas Version 11/15/2023”

このスレの番号は前スレ43を継いでNo.44からの連番としています
（なお、このスレは本体IUTスレの43からの分裂スレですが、分裂したNo43スレの中では このスレ立ては最初だったのです！）
(余談)
Langlands program Geometric conjectures https://en.wikipedia.org/wiki/Langlands_program
つづく

(譫言しか書かなくなったか)

いやー、本当にこの時代に生まれてラッキーだった。
この国に生まれてね。

ワイドショー的週刊誌的な興味対象でしかなくなった数学を見ることになるのをラッキーとはね

>>455-462
さすが 場末の5ch 過疎数学便所板だね
素人が好き放題書いている

>>463
>ワイドショー的週刊誌的な興味対象でしかなくなった数学を見ることになるのをラッキーとはね

まったくね
数学にAIが入り込んできています
今後の展開やいかに

（あち～）

素人でない書き込みの見本が見てみたいところw
参考にさせて頂きたい。

>>464
x,yが集合ならx^yも集合ですよど素人さん

なるほど、素人じゃなくてド素人だったのか！
な～んちゃってw

>『Qを構成した瞬間に有理数列全体の集合 Q^N も存在しており、作る必要など無い』か・・
>独自説だねぇ〜、ユニークで笑える、が面白すぎｗｗ（＾＾
↑
ど素人がなんか言ってます

>>466
>素人でない書き込みの見本が見てみたいところw
>参考にさせて頂きたい。

当然、わたくしめも、素人だが
プロ数学者は、ここでは 知る限り御大（名誉教授）くらいだが
彼は、主に お天気日誌を書いています（＾＾

おっと、めずらしく お天気日誌以外のコメントを書かれたね
　>>445 より
>いずれにせよこれで一段落ということにしてはどうか
>suspendedと思った者は皆無に等しい

だね
多分、今回のLANA中間発表で 一段落（ある程度の結論は出た）という意見
まあ、これが本因坊戦とすれば 5番勝負の第一局は LANAチームの中押し勝ち！
次の対局を始めろということでしょうねｗ　（＾＾

>当然、わたくしめも、素人だが
何を己惚れてるのか　君はど素人だよ
x^yが集合であることは理解できた？

>>471
で、君は？
どど ど素人かね？ｗｗｗ

下らん

>>471
私の見るところ
君は、囲碁でいうセイモクだなｗｗｗ

Benjamin. Collas 氏なども
しっかり、望月・星氏らを叱咤激励してやってください
よろしく
衆知を合わせて問題解決を お願いします （＾＾

https://ahgt.math.cnrs.fr/activities/
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).

https://www.kurims.kyoto-u.ac.jp/~bcollas/
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.

ファルティングスは優しいね。
「論文は理解できなかった。 自分の研究に時間を割くことにした」
「数学になってない」と切って捨てるのではなく「自分の理解力が及ばない」とも解釈可能な表現で望月を傷つけることなくやんわりと距離を取っている。
フィールズ賞受賞者で人格者でもある。弟子とは大違いだね。

グロタンディークの名前が付いてたから一部のアホどもが有り難がってただけで
結局尊師のやったことって特殊な小さい問題ひとつ解いただけでしょ
甘やかしてきた取り巻きたちが尊師を増長させ続けて今回のような日本の恥晒しにまで行き着いてしまったわけだな

グロタンディークの名前が付いてたから一部のアホどもが有り難がってただけで
結局尊師のやったことって特殊な小さい問題ひとつ解いただけでしょ
甘やかしてきた取り巻きたちが尊師を増長させ続けて今回のような日本の恥晒しにまで行き着いてしまったわけだな

関連 コピーしておきます
https://plaza.rakuten.co.jp/shinichi0329/
新一の「心の一票」2026.01.01
Leanによる形式化は、長期的な検証や説明責任を可能にする記録装置となり得るか？
カテゴリ：研究関連の現状報告 https://plaza.rakuten.co.jp/shinichi0329/diary/ctgylist/?ctgy=3

​前回の記事​では、定理証明支援系ソフト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」ということになります。

つづく

つづき

私自身、2010年〜2011年頃、[IUTchIV]§3を執筆したとき、species/mutationは、特に難しい話でもなく、取り立てて新奇性のある話でもなく、多くの数学者が当たり前に脳内で無意識のうちにこなしている処理を、（同様の概念が明示的に記述されている適切な文献が見付からなかったために）ただ自分で明示的に記述してみただけのものに過ぎないという認識でした 略

一方で、species/mutationの、Leanによる形式化の可能性について調べ始めた途端、全く想定外の展開に見舞われてしまいました。まず、species/mutationの定義では、集合論的な（＝つまり、いわゆるZFCの）論理式が非常に中心的な役割を果たしますが、これまでのLeanの標準とされているライブラリMathLibでは、ZFCモデル（＝つまり、標準的な集合論のモデル）は用意されているため、特定の集合に対する特定の論理式をLean上で扱うことが可能となっていますが、一方で、species/mutationの理論において本質的な役割を果たす「不定元のような論理式」（＝特定されていない、「とある論理式Φ」のようなもの）を扱うには、一階述語理論としてのZFCが必要であり、それはMathLib上ではまだ掲載されていないということが判明しました。
略
(引用終り)
以上

私見だが
早く Leanによる形式化の詳細を公開して
みんなで議論して、早く前進させた方が良いと思う

ある方法がだめでも
おうおうにして
別の手段があるものです

アホ

アッポー

ほんとはなんもやってないんだよ

>>481
できてないのバレちゃうじゃん

species/mutationという用語を見てちょっと説明聞いて最初思ったのは
これcategoryとfunctorじゃないのってことだったけど
speciesはcatetoryのobjectだけをイメージしてるのかね？
morphismは考えてない？

>>480
>（＝特定されていない、「とある論理式Φ」のようなもの）

「のようなもの」じゃ形式化は出来ないだろ
それから形式化の仕事してるなら論理式なんて非専門用語は使わずに
命題なのか述語なのかはっきりさせないと
述語に量化記号使うなら二階述語論理になるし
大丈夫ですか

数学屋はたとえ公理の数を有限無限個にしても一階述語論理に閉じこもることを好むが
計算機科学屋はsystem Fとか昔から高階トポスに親しんでる人が多い
一階つまりエレメンタリートポスで充分なのかどうかはLean関係なく数学的な議論ができる
圏論的には量化をスライス圏における随伴関手として扱うのは当然知ってるだろうしそこまで難しくないだろ
そこをはっきりさせてくれないと形式化なんて無理
「のようなもの」なんて論外
まあIUT関連の論文ではよく出てくる言葉なんだけどw

>>487
>「のようなもの」じゃ形式化は出来ないだろ
∃φ
みたいなのを必要とすると言いたいのではナイかな

>>485
>できてないのバレちゃうじゃん

いや、それが大切だと思うんだ
つまり、出来ていることと、出来ていないこと
これを明確にして、公表するべし！

下記、向こうのスレからだけど
ほんと 同意で そう思う

IUT I〜IVは、望月氏の単著だから 望月氏が決断すれば良いだけ
「Leanコード出来たところまで、公開します！」とやればいい
そうして、広く みなで議論するべし

いまや、仏国まで巻き込んだ 一大遠アーベルプロジェクトになっているんだから
オープンな議論をしていかないと いけない
と思うよ

(参考)
https://rio2016.5ch.io/test/read.cgi/math/1783860274/512-
2026/07/25(土) ID:ncTQQ9AA
>> 509
>アイデア自体が無力なので修正・補強は無意味なのよ
ABCに対するアプローチ方法としては面白いとは思うけどな
ディオフォントス幾何においては遠アーベルとかじゃ無いとABCに接近出来ないのは研究者からしたらほぼほぼ気づいてることだし

>abcが出るくらい非自明な主張を証明なしに使っていただけ
その主張に証明を与えればいいんでしょ
数学によくある予想の置き換えというか、もとからある予想Aは予想Bと等価ということを証明すること自体に意味がある
あとは予想Bを証明するか何なら予想Bが新たな予想Cと等価だと証明して予想Cを証明するだけ

ABC予想関連で不毛だなと思うのは望月先生の証明を議論すること
さっさとABC予想はコレコレの形の予想を証明すると自動的に成立するから、望月の研究ではそれを確認しただけ
さあ皆さんコレコレの形の予想を証明、反証しましょうねで済む話

>特定されていない、「とある論理式Φ」のようなもの
算術におけるゲーデル数のアイデアを集合論へ適用すればよくね？
有限種類の記号の有限列であるところの論理式と集合との1対1対応を定義できるだろうから、論理式（に対応する集合）全体の集合 Form を定義できて、∃φ∈Form とすればよくね？

>一階述語理論としてのZFCが必要であり、それはMathLib上ではまだ掲載されていないということが判明しました。
ん？　一般的なZFCは一階述語理論としてのZFCじゃないの？　何を言ってるんだろう？

>>490 追記

下世話な話だが
望月氏は、世事に疎いみたいなので書いておくと
IUTがLean形式化がパスしないと
世間からは、IUT証明はしっぱいと判定されるだろう

が、後付けでも ロジック追加で Lean形式化のギャップを埋めることができれば
一応格好はつく

さて、IUT証明しっぱいと判定されて困ることは
・まず、望月研の院生が困る
（あの有名な望月研か と言われるか 悪名高い望月研出身かとなるかのちがい）
　フェセンコ氏や彼の弟子 周忠鵬も同じ
・RIMS のIUT論文別冊出版のとき
　巻頭に編集者連名で「ちゃんと審査したので大丈夫」宣言を書いた
　柏原先生が 筆頭だったが、10名くらい居たはず
・遠アーベルプロジェクト
　”Arithmetic & Homotopic Galois Theory IRN” https://ahgt.math.cnrs.fr/activities/
　ここに 仏国の人もいるから、おおげさには国際問題

そんなこんなで 繰り返すが
後付けでも Lean形式化のギャップを埋めることができれば 一応格好はつく
が もしダメでも それは仕方ない。人間だもの
（スポーツなら 後のVAR判定で再逆転もありかも）
ともかく、事態の収束を加速する必要がある

>>493 補足
>・RIMS のIUT論文別冊出版のとき
>　巻頭に編集者連名で「ちゃんと審査したので大丈夫」宣言を書いた
>　柏原先生が 筆頭だったが、10名くらい居たはず

類似例は、数学史ではしばしばある
自然言語系では、当然視・自明視していた事項が
実は、公理系の選び方で、自明ではないと判明することがある
下記の可算選択公理みたく

多くの人が 賛同したことは
後世から見て「まるっきり間違いとは言えない」ねと

そこらがハッキリすれば
それはまた数学の更なる発展に繋がる
ともかく、オープンな議論にすることが大切なことだろう

(参考)
https://ja.wikipedia.org/wiki/%E9%81%B8%E6%8A%9E%E5%85%AC%E7%90%86
選択公理
可算選択公理
カントール、ラッセル、ボレル、ルベーグなどは、無意識のうちに可算選択公理を使ってしまっている。

>>493
その通りだとは思うがどう考えても誰かはダメージを受けるね。
そしてその可能性のある人間が問題解消に動くとはとても思えない。

>後付けでも ロジック追加で Lean形式化のギャップを埋めることができれば
>一応格好はつく
格好つくどころか世紀の大証明

>>494
>>493
後付けすれば勝てる！！
パチンコ中毒朝鮮人の主張w

>>490
オープンに望月新一の大惨敗を認めればいいだけ

>>493
IUT証明は大失敗
後付けで証明したら
望月新一ではなくLean形式化チームのみの大成果
望月も星も蚊帳の外　残念でした　南無阿弥陀仏

>>494
自明でないなら即敗北
はいっ、死にました！

そのギャップを解決する本質的なアイデアがなくて空虚なのなら一からABC予想証明するより難しいかもしれないけど

>>501
GAP解消に至らなくても
とても良いアイデア満載なんだろ

しかっし
IUTダメなら
F1何てもっとダメダメだろうに

>>480
↑これって望月先生本人の？
まじですか

順番にいくよ

>>504
>↑これって望月先生本人の？
>まじですか

多分、望月先生ご本人でしょう
他にも多数の投稿があるよ
それらは、望月先生ご本人と仮定しても 完全に無矛盾だから

>>495-503
>その通りだとは思うがどう考えても誰かはダメージを受けるね。

理系では仕方ない
よくあることです
論文が間違っていました
これのゴマカシは きかない

>オープンに望月新一の大惨敗を認めればいいだけ

それに近いが 「Lean形式化未達」を
まず 率直に認めることだね
全ては そこが出発点だ

>後付けで証明したら
>望月新一ではなくLean形式化チームのみの大成果
>望月も星も蚊帳の外　残念でした　南無阿弥陀仏

もし、そうなっても仕方ないだろう
数学では ゴマカシはきかない

>そのギャップを解決する本質的なアイデアがなくて空虚なのなら一からABC予想証明するより難しいかもしれないけど

まあ、現実を
誤魔化さずに素直に 直視すること
そこが、基本で出発点ですよ

内容ゼロ

とんでも論文なのに権威のゴリ押しでごね得狙うのはAIでできなくなりそうだね
望月に限らずちゃんと証明書いてないのにプロには当たり前だ！とか居直る困ったエライ人も多いからね
深谷小野vsMcDuffはどうなるのかな？

>>488
それならそうはっきりと言えばいいだろ

>>508
言ってると思うが

>>509
のようなものじゃ駄目だろ
そもそもRIMSの人たちは圏論から述語論理に翻訳出来るのかね

n変数の論理式はV^n={(x1,…,xn)}の部分クラスとみなせないかな
V^nの部分クラス全部がn変数論理式とは見なせないかもと思うけど
φ(x1,…,xn)
に対して
P={(x1,…,xn)|φ(x1,…,xn)}
を考えてやれば
φ⇔ψ
であるものを同一視するので十分じゃ無いかな
どうせ使うのはφ(x1,…,xn)の真偽だけだから
論理式として異なっていても真偽が一致すれば
問題にならないんじゃ無いかな

>>505 補足
>まあ、現実を
>誤魔化さずに素直に 直視すること
>そこが、基本で出発点ですよ

みなさん
コメントありがとう

繰り返すが
１）望月、星、加藤で話をして 現状のLeanのコードを含めて
　あらいざらい、オープンにすること
２）望月＋星他 一族で 今回の中間報告への応答を発表すること
　まず、すなおに Lean形式化未達であること
　その原因についてを述べて
　その後,これからどうするのか？ 計画と見通しを述べる
３）その後、Lean形式化達成に向けて、シンポジュームとか
　オープンな議論の場を持つ（議論は公開する）
　これを繰り返す。その中で、Lean化達成できればGood！

これ本人だとすると全くleanわかってない
公式文書読めよ

みなさんありがとうとか言ってんの笑う
文字読めてねえw

ID:bmdqsgm3
こいつマジで言語障害以前に知恵遅れてるだろ

>>513
>これ本人だとすると全くleanわかってない
>公式文書読めよ

うん
１）まず、本人かどうかだが、下記の全33件で 最初が 2016.11.25で
　このときから 本人かどうかが問題になった
　が、それから10年、いまでは、まずご当人だろうとされている
（当人しか書けそうもないことも書いてあるから）
２）”全くleanわかってない”は、自身でも発言しているし 正しいだろう
　だから、leanチームとのインターフェイスは 星さんが担ってきた
３）ゆえに、leanチームの許諾を得て、現状のleanコードを公開してもらって
　それを 遠アーベル関係者（仏国も含め）で共有して
　leanに詳しい京大の人にも入って貰って、3.11→3.12を いろいろ突き回すことも検討しないとね

そう思うわけです
私も leanは 詳しくないが
ともかく オープンにすること、衆知を集めること、マンパワーを増やすこと
ここらが、基本ですね

(参考)
　>>479 より
新一の「心の一票」
https://plaza.rakuten.co.jp/shinichi0329/diaryall/
新着記事一覧(全33件)

https://plaza.rakuten.co.jp/shinichi0329/diary/201611250000/
はじめまして
ブログを開設しました。仕事で忙しくてそれほど頻繁に更新することはできないかもしれませんが、とりあえず、この通り、略式でブログ開設のご挨拶をさせていただきたいと思います。どうぞよろしくお願い致します。（因みに上の画像は富士山の写真です。もう少し補足しますと、2015年11月、親戚の結婚式に出席するために静岡を訪問した際に撮った写真です。）
2016.11.25

>>515
下らないね君

>>517
文盲のセリフがこれw

「のようなもの」を形式化して新しい数学の地平ですね
定義ははっきりしないのようなもの
のようなものから始まる数学
「の・ようなもの」のエリザベスがRIMS呆酷暑読んでたりする世界か

>>505
>>オープンに望月新一の大惨敗を認めればいいだけ
>それに近いが

誤　それに違いが
真　そのものズバリだが

さっさと玉音放送を流しなさい

今後帝國ノ受クヘキ苦難ハ固ヨリ尋常ニアラス
爾臣民ノ衷情モ朕善ク之ヲ知ル
然レトモ朕ハ時運ノ趨ク所
堪ヘ難キヲ堪ヘ忍ヒ難キヲ忍ヒ
以テ萬世ノ爲ニ太平ヲ開カムト欲ス

>>後付けで証明したら
>>望月新一ではなくLean形式化チームのみの大成果
>もし、そうなっても仕方ないだろう

トンデモ過ぎて、そうなりそうもない

数学界の「竹槍三百万本論」

>>520
>真　そのものズバリだが
>さっさと玉音放送を流しなさい

証明は、成立か 不成立か ２値の世界だが
数学は、勝った 負けた の世界ではない

>>後付けで証明したら
>>望月新一ではなくLean形式化チームのみの大成果
>もし、そうなっても仕方ないだろう

例え話で 補足しておくと
・望月さん 詰め将棋の長手数問題を作った。名前が ”遠アーベル流IUT”
・それを、ある将棋ソフトの解析にかけたら、ある部分で詰まないよ と出た
・それを受けて、詰め将棋作者の望月氏がどうするか？

普通は、下記
１）将棋ソフトの解析をオープンにする
２）なぜ詰まないのか？ どこか改善できないか？
３）まれに、将棋ソフトのバグの可能性もあるかもです（Lean ライブラリー不備）

で、仏国との遠アーベルの国際研究プロジェクトが 走っている
https://ahgt.math.cnrs.fr/activities/

早く解決した方がいいよね
（否定か肯定か 最終結果に関わらず）
仏国にも 「どうなってんの？」「こうなっています」と オープンに全てを報告した方がいい

アホ

S-S同様IUTは間違いと言っていて
しかし自分がその間違いを正したと主張してた人居たと思うけど
その人はLANAの発表を受けて何か言ってないの？
S-Sはもうとおに興味失っているだろうから
特に何も言わない？
でも加藤さんがS-Sも間違ってると言っているのには
コメントしてイイと思うけどね

>>522 補足
>証明は、成立か 不成立か ２値の世界だが
>数学は、勝った 負けた の世界ではない

囲碁では、形勢判断が非常に重要で
かつ 将棋よりも 変化の手段の余地は大きい

”考えれば手はあるもの”（坂田栄男『囲碁名言集』（下記））と言われる

数学でも、最初のアイデアは厳密さが欠けていたが
後世に 厳密な証明が与えられた例は多数ある
例えば
１）ニュートン・ライプニッツの微分積分：結構直観的な議論だが、後世厳密化された
２）5次代数方程式の冪根解法：イタリア ルフィニ氏が不可だと言った。アーベルが厳密な証明を与えた
３）ガロアの方程式理論：決闘前夜の走り書きで、ある部分では”証明は思いつくであろう”と流したりがあったが（不成立の命題もあった）、後世正しいとされた
４）リーマン面：リーマンの議論は厳密性を欠くと言われたが、結局正しかった

IUTに戻ると、現状Lean形式化に乗らない部分があると言われるが
一方で、IUT論文を正しいと認めた 数学者 多数
筆頭が 玉川先生かな？ 仏国の数学者も多数 認めた
なので、上記例のように 何某かの数学的真理を含んでいる可能性はあると見ています

望月先生、頑張って下さい！

(参考)
https://rendaico.jp/igo/ishigonomi/3_3.html
囲碁吉の天下六段の道
更新日／２０２４（平成３１．５．１栄和改元／栄和６）．３．１日
(抜粋)
【坂田の「1　心理編」】
　「坂田栄男『囲碁名言集』（有紀書房、1988年）」の「1　心理編」は次の通り。
あきらめる前に、もう一度考えよう。考えれば手はあるものだ

アホ

>>524
>S-S同様IUTは間違いと言っていて
>しかし自分がその間違いを正したと主張してた人居たと思うけど

うん、下記のKirti Joshiさんだね

>でも加藤さんがS-Sも間違ってると言っているのには

”S-Sも間違ってる”の部分は、下記動画でキラン・ケドラヤ氏が報告していた
公開文書にも、記載があったと思う
えーと Contents ”10. An examination of Scholze-Stix document 46”だね

(参考)
https://sites.arizona.edu/kirti-joshi/
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.]

https://zen.ac.jp/news/zmcpostevent0717
2026/07/17 Zen大学
プレスリリース
IUT理論のコンピューターによる検証を目指す LANAプロジェクト、「Project LANA Interim Report on IUT Theory」を公開
——現時点での評価、残された課題、Scholze–Stix報告書との関係を報告

公開文書「Project LANA Interim Report on IUT Theory」
報告書全文 ▶ https://github.com/katobungen/LANA_report_202607/blob/pdf/LANA_report_202607.pdf
発表動画
https://youtu.be/g0QLL8iYECY?t=590

https://zen.ac.jp/news/zmcpostevent0331
2026/03/31
プレスリリース
IUT（宇宙際タイヒミューラー）理論のコンピューターによる検証を目指すZEN数学センターの新プロジェクト「LANA」を発表
――世界3大学による国際共同研究として始動――

バカ朝鮮人のセルフコピペQ&Aかよw
でも論理で繋がってない低学歴キチガイ仕草w

負けを認められない国粋狂人 Set A

>>529
朝鮮偽右翼に国粋とか言うのやめろよ

>>525
証明論に限らず数学の形式化が進んでるから
昔みたいなことはもう起きないよ

>>531
>証明論に限らず数学の形式化が進んでるから
>昔みたいなことはもう起きないよ

たぶん 違うんじゃ無いかな
１）まず、下記の 渕野先生が書いている
”厳密性を数学と取りちがえるという勘違い”
２）さらには、形式化の限界
　これは、下記ゲーデル不完全性定理の話（下記）
　”証明できない真実: 第一不完全性定理により、内容としては正しい（真である）にもかかわらず、その体系の中のルール（公理）だけでは「正しい」と証明できない命題が必ず存在することが示されました”

要するに、数学とは IUTのLean形式化の失敗をのり超えて 進んでいくものだと思う
（それは、何かを追加して Lean形式化が出来るのか 逆に IUTは根本に問題あり となるか どちらか不明だが）

(google検索)
ゲーデル不完全性定理の数学における意義は何か？
AI による概要
ゲーデルの不完全性定理の数学における意義は、「すべての数学の真理を完全に証明できる一つの完璧なルールブック（公理系）を作ることはできない」と示したことです。主な意義として、ヒルベルト・プログラムの挫折、真と証明の乖離、数学基礎論の発展があげられます
ヒルベルト・プログラムの挫折
略
「真理」と「証明」の限界
・証明できない真実: 第一不完全性定理により、内容としては正しい（真である）にもかかわらず、その体系の中のルール（公理）だけでは「正しい」と証明できない命題が必ず存在することが示されました

　>>30より再録
＜厳密だけが、数学ではない＞
＜数学と厳密＞
あなたのまったく逆を、渕野先生が書いている
”厳密性を数学と取りちがえるという勘違い”
https://www.amazon.co.jp/dp/4480095470
数とは何かそして何であるべきか デデキント 訳解説 渕野昌 筑摩書房2013
「数学的直観と数学の基礎付け 訳者による解説とあとがき」
P314
(抜粋)
数学の基礎付けの研究は，数学が厳密でありさえすればよい， という価値観を確立しようとしているものではない.
これは自明のことのようにも思えるが，厳密性を数学と取りちがえるという勘違いは，
たとえば数学教育などで蔓延している可能性もあるので，
ここに明言しておく必要があるように思える
多くの数学の研究者にとっては，数学は，記号列として記述された「死んだ」数学ではなく，
思考のプロセスとしての脳髄の生理現象そのものであろう
したがって，数学はその意味での実存として数学者の生の隣り合わせにあるもの，と意識されることになるだろう
そのような「生きた」「実存としての」(existentialな)数学で問題になるのは，
アイデアの飛翔をうながす(可能性を持つ)数学的直観」とよばれるもので，
これは， ときには，意識的に厳密には間違っている議論すら含んでいたり，
寓話的であったりすることですらあるような，
かなり得体の知れないものである

（何かを理解しているつもりになっている）

>>532 補足
(引用開始)
>証明論に限らず数学の形式化が進んでるから
>昔みたいなことはもう起きないよ
たぶん 違うんじゃ無いかな
(引用終り)

意味が分らないだろうから、ABC予想の歴史を振りかえろう
１）昔々 フェルマーさんが、フェルマー予想を出した。証明を得たが、余白が狭いという名言を書いた
　https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A7%E3%83%AB%E3%83%9E%E3%83%BC%E3%81%AE%E6%9C%80%E7%B5%82%E5%AE%9A%E7%90%86
２）みんな挑戦したけど、最終解決にならない状態で 数百年
　”1984年、ゲルハルト・フライは、フェルマー方程式とモジュラリティ定理（当時はまだ予想だった）との関連性を指摘した”（下記）
３）モジュラリティ定理は、日本では谷山志村予想で有名だが
　当時は、モジュラリティ定理の証明は多くの数学者は「無理！」とあきらめた
　そこで考えられたのが、abc予想だ
　これは フェルマー予想で使われた 楕円曲線（フライ曲線とも呼ばれる）の性質から予想された不等式

要するに 流れは
フェルマー予想→フライが楕円曲線に関連づけ→谷山志村予想→谷山志村予想は難しいので迂回路して abc予想
→ 望月新一 おいらが 遠アーベルで証明するぞ とIUT理論を提出
→ LANA：Lean形式化に乗らないのでは？という中間報告（2026年07月 いまここ）

この数学数百年の大河の流れは、だれが考えても まだまだ 数学形式化だけでは 説明できないだろう
そもそも、ABC予想にもいろんなバリエーションありだしね（例えば 下記スピロ予想とか）

(参考)
https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem
(google訳)
1984年、ゲルハルト・フライは、フェルマー方程式とモジュラリティ定理（当時はまだ予想だった）との関連性を指摘した。フェルマー方程式が指数p > 2に対して解( a , b , c )を持つ場合、半安定楕円曲線（現在ではフライ・ヘレグアルク曲線として知られている[注4 ]） が成り立つことが示された。

ワイルズの一般証明
1986年にリベがε予想を証明したことで、フレイが提案した2つの目標のうち最初の目標が達成された。リベの成功を知った、フェルマーの最終定理に幼い頃から魅了され、楕円曲線の研究をしていたイギリスの数学者アンドリュー・ワイルズは、後半の目標、すなわち半安定楕円曲線に対するモジュラリティ定理（当時は谷山・志村予想として知られていた）の特殊な場合を証明することに尽力することを決意した

https://ja.wikipedia.org/wiki/ABC%E4%BA%88%E6%83%B3
ABC予想
オステルレ＝マッサー予想（英語: Oesterlé–Masser conjecture）[1][2]は、1985年にジョゼフ・オステルレとデイヴィッド・マッサーにより提起された数論の予想（未解決問題）である
https://en.wikipedia.org/wiki/Abc_conjecture
abc conjecture
(google訳)
abc予想は、オステルレとマッサーが楕円曲線に関するスピロ予想を理解しようとした試みの結果として生まれたものであり、[ 4 ]スピロ予想はabc予想よりも多くの幾何学的構造を含んでいます。abc予想は修正されたスピロ予想と同等であることが示されました。[ 1 ]

>>532
>１）まず、下記の 渕野先生が書いている
>”厳密性を数学と取りちがえるという勘違い”
数学は厳密でなくてもよいと勘違いしてるのがおまえ。

>２）さらには、形式化の限界
>　これは、下記ゲーデル不完全性定理の話（下記）
>　”証明できない真実: 第一不完全性定理により、内容としては正しい（真である）にもかかわらず、その体系の中のルール（公理）だけでは「正しい」と証明できない命題が必ず存在することが示されました”
それは数学そのものの限界であって形式化の限界ではない。
数学で論ずる対象は「何を仮定すると何が結論できるか」つまり相対的真理であって絶対的真理ではない。形式化はそのことを明らかにした。

>要するに、数学とは IUTのLean形式化の失敗をのり超えて 進んでいくものだと思う
内容ゼロのポエム

ど素人さんは持論を語らない方が良い。どうしても語りたければチラシの裏でどうぞ。

jin は頭の病気

>>534
>この数学数百年の大河の流れは、だれが考えても まだまだ 数学形式化だけでは 説明できないだろう
この検索でヒットしたワードを訳も分からず並べただけの出来損ないのAIみたいなクソ文はなに？

>（何かを理解しているつもりになっている）
馬鹿である自覚が無いので「理解しているはずだ、理解していないなんてことはあり得ない」とでも妄想してるんでしょう

自覚の無い馬鹿ほど始末の悪いものは無い

>>532
＞”証明できない真実: 第一不完全性定理により、
＞内容としては正しい（真である）にもかかわらず、
＞その体系の中のルール（公理）だけでは
＞「正しい」と証明できない命題
＞が必ず存在することが示されました”

誤り
「内容としては正しい（真である）にもかかわらず、」が嘘
「内容として、正しい（真である）としたら」が正しい

「正しいとしたら、正しいことが証明できない命題」が正解

なぜなら、正しい、とわかってないから

やっぱ論理が分からん高卒には、そこがどうしても理解できんか

>>535
＞それ（ゲーデルの不完全性定理）は数学そのものの限界であって形式化の限界ではない。

そう　理論内で自身の命題の証明可能性を記述できるとすると、そういうことが起きる、という話

やっぱ論理が分からん高卒Set Aには、そこがどうしても理解できんか

結局
「q-pilot対数的体積の二つの計算が「tautologicalに同値」とされている点、
あるいは、アルゴリズムの出力から得られる複数の可能なデータのうちの一つが、
入力から定まるデータとどのように同一視されるのか」
という、2015年以来指摘され続けてきた問題点について
望月新一が全く説明できず「自明！」と吠え続ける限り
数学界からは相手にされない

10年同じことをいってるのが
実数の定義が理解できない高卒Set Aそっくり

>>539
真の馬鹿は己の馬鹿を決して認めたがらない
そしてそれゆえ無敵の馬鹿であり続ける

>>542
>望月新一が全く説明できず「自明！」と吠え続ける限り
>数学界からは相手にされない

１）数学界から相手にされて
　2026年7月17日 LANA中間報告だろ？
２）LANA中間報告が出た。
　それを受けて 望月一派がどうするか？
３）私の意見は、LANA中間報告のLeanコードを公開して
　IUTに賛成・反対両方入れて オープンな議論をすべし

ということ

スレがいつの間にか進んでいる
骨密度の数値か骨質のどちらかの数値が低下して背骨が弱くなって
脊椎を何ヶ所か圧迫骨折すると、骨折後体が不自由になって、
腰の腰椎などの脊椎が前に曲がって圧迫骨折の治療に時間がかかり
圧迫骨折した脊椎は元の状態に戻らないだけでなく
背中を思うように曲げたりして動かせなくなるから、
瀬田君も脊椎の圧迫骨折には気を付ける方がいい
まさかのまさかの大誤算でした

内服薬にも長期間服用すると副作用として
圧迫骨折を引き起こす薬剤があるんだね

>>545
ID:Lm9NjsrG は、おっちゃんか？
レスありがとうね
圧迫骨折のアドバイスありがとね

まあ、IUT+遠アーベルの話は
日本には 論客がたくさんいる
だから、玉川先生とか いろいろ入って貰って

解決策を議論すれば良い
LANAプロジェクトの中間報告に使った元データとか
洗いざらい出して オープンに議論することだね

数学の勉強は骨が折れる。

まだ寝言言ってるよ
leanで定式化できないなら数学でない
それがわからんのならもう出てくんな
能無し

>>532
＞”証明できない真実: 第一不完全性定理により、
＞内容としては正しい（真である）にもかかわらず、
＞その体系の中のルール（公理）だけでは
＞「正しい」と証明できない命題
＞が必ず存在することが示されました”
完全性定理の反例があると言ってる？

>>549
そんな狭い範囲の話じゃねーんだよw
低学歴ってすぐ完全表現使うから嘘になるんだよ
ケーキ切れない論理も集合も知らないからIUT信者なんてやってられるんだよお前はww

低学歴w

実際さあ
こんなんでさあ
「天才だ！天才だ！」とか
言ってんのも言われるのも恥知らずって感じだよな
よく平気で生きてられるな

>>550
完全表現って何？
俺がIUT信者？何盛大に勘違いしてんだこいつ？

>>549
もちろん反例なんて無いから、間違ってるのは>>532。

PAで考える。ゲーデル文「ゲーデル文は証明できない」をGと書く。
不完全性定理から¬Gは証明できない。・・・(1)
(1)と完全性定理から¬Gが偽となるモデルが存在する。・・・(2)
仮に標準モデルで¬Gが真とすると任意のモデルでも真であるはずだから(2)と矛盾。背理法により標準モデルで¬Gは偽、すなわちGは真。

真なのは標準モデルでであって、任意のモデルでではない。それが>>532の間違い。

>>534 補足
へんなやつらが湧いているな

追加しておくと
１）IUTを なんらかのコンピューター証明に乗せられないか？
　という案だけは、望月氏のIUT論文投稿後 随分初期からあった（10年以上前）
　が、当時のコンピューター環境では、コンピューター証明に乗せるには
　マンパワーとマシンパワーが足りなかっただろう（だれも出来なかった）
２）2026年の今は、Lean形式化と AIのアシストと マシンパワーで
　ようやく IUTの検証が可能なレベルになってきたのでしょうね
３）さて、先の中間報告 7月17日 >>327 ご参照方
　中間報告の結論は、現時点のLean形式化未達なれど 達成できる可能性はあるという

よって
１）みんなで手分けして 早く結論を出した法が良いだろう
　そうしないと、望月研の院生とか「おれたちどうなるの？」って話とかね
２）軌道修正の余地はあるのでは？
　現時点のギャップを埋めるライブラリー補充とか
　ギャップを迂回する別ルートを探すとか
３）いまどきなら AIエージェント使いをリクルートして
　AIエージェントを走らずとかもありだろう

収束を加速する手段は、いろいろ考えられるから
議論をオープンにすれば良いと思うよ

>>555 タイポ訂正

１）みんなで手分けして 早く結論を出した法が良いだろう
　↓
１）みんなで手分けして 早く結論を出した方が良いだろう

余談
いまどき、AIエージェントが一番頼りになったりしてｗｗ （＾＾

>>555
>現時点のLean形式化未達なれど 達成できる可能性はあるという
現時点のリーマン予想証明未達なれど 達成できる可能性はあるという
と同じくらい内容ゼロ。

>へんなやつらが湧いているな
ど素人さんは持論語らない方が良いというアドバイスも頑なに聞く耳持たない君がね

>>556
全体がクソなのにtypo気にしても無駄

（どんな未解決問題も証明される可能性は常にある）

>>534 補足

１）AI「ヤコビアン予想」反例 まあ、これはこれ
https://rio2016.5ch.io/test/read.cgi/math/1784575110/12
AI「Claude Fable 5」が87年来の難問「ヤコビアン予想」を覆す反例を生成したとAnthropic研究者が報告
https://gigazine.net/news/20260721-claude-fable-5-jacobian-conjecture/

２）将来的には いまの囲碁や将棋AIみたく 人間のプロ棋士より上位互換になるかもだが
　2026年現在の数学においては、総合的にはプロ数学者が上だろう
　しかし、人間＋最新AIなら 並みのプロ数学者を超えるかもね

３）LANAプロジェクトのLean形式化で言えば
　IUTがLean形式化をパスしなかった原因は いろいろ考えられるだろうが
　可能性としては IUTの”3.11→3.12”ギャップがあることも考えられる
　ここらは、議論を進めないと 分らないことだね

なので、話をオープンにして
早く進めた方が良いねと

>>560
>２）将来的には いまの囲碁や将棋AIみたく 人間のプロ棋士より上位互換になるかもだが
>　2026年現在の数学においては、総合的にはプロ数学者が上だろう

さて 補足
https://ja.wikipedia.org/wiki/%E9%81%A0%E3%82%A2%E3%83%BC%E3%83%99%E3%83%AB%E5%B9%BE%E4%BD%95%E5%AD%A6
遠アーベル幾何学
数体とその絶対ガロア群の初期の結果は、アレクサンドル・グロタンディークによる数体の双曲線[1]についての予想に先立ち、ユルゲン・ノイキルヒ、ギュンデュズ・イケダ、岩澤健吉、内田興二（ノイキルヒ・内田の定理）によって得られていた。
単語としての「遠アーベル」はアーベルに否定の接頭辞 an がついたもので、1980年代のグロタンディークの有名な著作である「Esquisse d'un Programme」で導入された[2] [3] 。
望月新一はいわゆる単(mono-)遠アーベル幾何学を導入および発展させた[6]。それは、数体または他のいくつかの体にわたる特定のクラスの双曲的曲線について、その代数的基本群からその曲線を復元するものである。単遠アーベル幾何学の主要な結果は望月の「絶対遠アーベル幾何学」などにある[7][8]。
遠アーベル幾何学は、類体論の一般化の1つと見なすことができる。 他の2つの一般化（高次アーベル類体論と、表現理論的ラングランズ・プログラム）とは異なり、遠アーベル幾何学は非常に非線形でnon-アーベルである[9]。
(引用終り)

この 遠アーベル幾何学 でも
いつの日か 数学AIが 自力で グロタンディークを超えるアイデアを出すかもだがｗ
さすがに いまは「ヤコビアン予想」反例(>>560) 程度が限界でしょう（それでも凄いけどね）

別に ”パーフェクトイド空間”というのがある（下記URL）
ペーター・ショルツェ氏によって 創始されたという
https://ja.wikipedia.org/wiki/%E3%83%91%E3%83%BC%E3%83%95%E3%82%A7%E3%82%AF%E3%83%88%E3%82%A4%E3%83%89%E7%A9%BA%E9%96%93
数学AIが パーフェクトイド体を 自力で考えたらエライと思う

2026年時点では、それらまだ無理でしょう
なので、IUTのLean形式化は かなり人間の数学者が 奮闘する必要があるだろう
望月先生、がんばって下さい！