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
つづく

>>377
少なくともペレルマンは指摘された問題点に素直に向き合って照明のギャップを埋める作業をやったわけだが。

>>426
ギャップが小さければほとんど望月の仕事と認められるだろうけど
その可能性は全くないよね
8年間改善できなかったんだから
小さいギャップなら望月かショルツか他の誰かがとっくに埋めてる
みんな何処に問題あるか知ってたんだから

下記(参考)引用
「 Interuniversal geometry とABC 予想61 」からだが
これは いい話だね

思うに
１）望月＆星氏は 加藤氏のLANAプロジェクトに 現状のLeanコードを公開すべきだろう
２）そして、問題点を明らかにして オープンな議論を惹起すべし
３）望月＆星氏は 今回の加藤氏のLANAプロジェクト中間発表について コメントを出すべきだろう
４）その上で、今後どうしていくのかのロードマップを公表すべきだ

要するに
衆知を集めて 遠アーベル関係者みなで議論して 解決策を模索するべし！だね
その理由は
１）IUT論文は、すでに２つ投稿され 査読掲載されている
　一つは望月氏自身のIUTの大作で もう一つは5人共著のフェルマー解決論文で Kodai mathに掲載された
　さらには、中国の若手の周忠鵬の論文もある
　さらには、日仏合同 Arithmetic & Homotopic Galois Theory IRN も進んでいる
２）このような背景から考えて、できるだけ早く 事態を収拾すべき
　混乱を長引かせるのは、よろしくない

三人寄れば文殊の知恵
問題をオープンにすべし
解決を長引かせるのはよろしくないだろう

(参考)
https://rio2016.5ch.io/test/read.cgi/math/1783860274/316-618
316１３２人目の素数さん
2026/07/20(月) ID:B6WVrHSM
>>312
もしかしてこれ？
With AI becoming increasingly capable of solving difficult problems, I've been wondering why LANA hasn't released its Lean formalization, even in an incomplete state. Even if the proofs themselves are unfinished, the definitions and overall formal framework would already be valuable to the community.

That's one of the reasons I decided to publish my own independent Lean formalization of IUT, developed with the help of Fable5. I also shared it on 4chan and 5ch in case anyone is interested in taking a look.

but, comment is japanese only.
https://github.com/Takkun-kohinata/IUT_LEAN
(google訳)
AIが難問を解く能力をますます高めている中で、LANAが未完成の状態であってもLean形式化を公開しないのはなぜだろうかと疑問に思っていました。証明自体が未完成であっても、定義と全体的な形式的枠組みは既にコミュニティにとって価値のあるものとなるはずです。
それが、私がFable5の協力を得て独自に開発したIUTのLean形式化を公開することにした理由の一つです。興味のある方がいらっしゃれば、4chanと5chにも投稿しました。

318１３２人目の素数さん
2026/07/20(月) ID:joumQYeu
>>316
それだよ
やっと承認されたか
woitの方にも似たこと書いたけど承認されんわ
(引用終り)
以上

>>429 タイポ訂正

１）望月＆星氏は 加藤氏のLANAプロジェクトに 現状のLeanコードを公開すべきだろう
　↓
１）望月＆星氏は 加藤氏のLANAプロジェクトに 現状のLeanコードを公開要請すべきだろう

補足
いまどき
Leanコードでの証明未達では
世間では通用しないことは
明白

査読を通って 掲載されてしまった論文だから
万機公論 議論をオープンにすべし！

leanをaiに学習させられないだろうか

>>428
ですね
分かりやすい指摘です

>>428
(引用開始)
ギャップが小さければほとんど望月の仕事と認められるだろうけど
その可能性は全くないよね
8年間改善できなかったんだから
小さいギャップなら望月かショルツか他の誰かがとっくに埋めてる
みんな何処に問題あるか知ってたんだから
(引用終り)

うん、君にだってチャンスあるぞｗ　（＾＾
いま、AIつかって 数学未解決問題を解かせたという話がどんどん出ている
実際にも 下記の別スレだが AI Claude を使う チャレンジをするらしい
LANAプロジェクトに先行すれば 面白いな 頑張って欲しいね （＾＾

それはともかく
「ポアンカレ予想物語」という本がある。ポアンカレ予想というのは、一見解けそうに見えて みんなチャレンジして 失敗したという

ABC予想は、その逆かもね
難しすぎて、チャレンジする人があまり居ないというか
望月以外には 「解かれた（解いた）ぞ」という話が あまり聞こえてこない（ジョシさんは別として）

望月IUTは、いままでで 一番ABC予想解決に近づいた論文かもしれない

なので望月IUTの延長線上でも、だれかがギャップを埋めるか
あるいは だれかが 望月IUTの改造で
それはAIの力もかりてでも Leanに乗せることができれば
間違いなく数学の進歩でしょう

＜アマゾン＞
ポアンカレ予想物語 (数セミ・ブックス 13)
本間 龍雄 (著) 日本評論社 発売日 ‏ : ‎ 1985/11/1

(参考)
https://rio2016.5ch.io/test/read.cgi/math/1783860274/378-382
378１３２人目の素数さん
2026/07/21(火) 09:12:45.13ID:rReqYplZ
「3.11 = 3.12」 を分解して形式化をはじめている
前半 (3.11)
APT (アルゴリズム的並行移動)
IPL (入力整合性)
→第1~第3三角形
後半 (3.11.5= 3.12)
SHE (同時正則表現可能性)
IPL (input prime-strip link)
→第4三角形 (現在RIMSが形式化に取り組んでいる箇所)

382１３２人目の素数さん
2026/07/21(火) 09:38:04.19ID:rReqYplZ
lUTのLean形式化は、次の段階に分けて進める
・Stage1
[IUTchlll] 定理3.11=系3.12
・Stage2
[UTchll]定理3.11の証明
・Stage3
[UTchl-ll]
・Stage4
1995年以降の先行研究
・Stage5
数値的側面 ([IUTchlV],[ExpEst])

解決策がある前提なのが馬鹿

>>433
>望月IUTは、いままでで 一番ABC予想解決に近づいた論文かもしれない
IUTは、複数の異なる宇宙を用意しその間を通信経路で結ぶことで、通常の数学（ひとつの宇宙）では分離できない掛け算と足し算の絡み合いを解きほぐそうとするもの。
このアイデアが機能するかは系3.12を証明できるかにかかっている。証明できなければIUTはただのゴミでABC予想解決にまったく近づいていない。
そしてLANAは証明に失敗し解決の見通しはまったくの白紙、1年後を目途に次の報告をしたいと述べるのがやっとの惨憺たる有様。

ショルツェは流石だね。単にギャップを指摘するだけではなくIUTというアイデア自体がゴミであることを正確に見抜いていた。
一方でLANAは2年がかりでショルツェの発言を補強したに過ぎない。
国粋馬鹿よ、これが現実だ。

>>436
あいつらは国粋じゃない
旧満州由来の在日朝鮮人偽右翼

jin は頭の病気

>>429-430
>望月＆星氏は 加藤氏のLANAプロジェクトに
>現状のLeanコードを公開要請すべきだろう

見せてもらっても無駄だろ
望月も星も答えをもってないんだから

>そして、問題点を明らかにして
>オープンな議論を惹起すべし

問題点は明らか
すでにオープンに議論されてる

>望月＆星氏は
>今回の加藤氏のLANAプロジェクト中間発表について
>コメントを出すべきだろう

まいりました、って？（笑）

>その上で、今後どうしていくのかの
>ロードマップを公表すべきだ

ロードマップなんかないだろ
ノープランなんだから（笑）

国粋高卒Set A君、頭、大丈夫？

>>429
>衆知を集めて 遠アーベル関係者みなで議論して 解決策を模索するべし！

無駄　誰もノープランなんだから議論にならない

>IUT論文は、すでに２つ投稿され 査読掲載されている
>一つは望月氏自身のIUTの大作で
>もう一つは5人共著のフェルマー解決論文で Kodai mathに掲載された

前者は不正査読な
後者は前者を認めた上での評価として逃げられるだろうけど

>さらには、中国の若手の周忠鵬の論文もある

査読通ってるの？違うだろ　じゃ無意味

>さらには、日仏合同 Arithmetic & Homotopic Galois Theory IRN も進んでいる

それIUTと無関係

>できるだけ早く 事態を収拾すべき
>混乱を長引かせるのは、よろしくない

RIMSが不正査読を認めて解体されればいい

日本の数学は不正査読で自爆しましたとな

ｷﾞｬﾊﾊﾊﾊﾊﾊ!!!

いずれにせよこれで一段落ということにしてはどうか

>誰もノープラン
その通り。実際加藤はギャップを埋める目途は皆無、有限時間で埋まるかもしれないし埋まらないかもしれないと言った。全くの白紙ということだ。

>いずれにせよこれで一段落ということにしてはどうか
白紙を認めた以上望月論文はrejectedとすべき、白紙なのにsuspendedはおかしい。

suspendedと思った者は皆無に等しい

通常は1年後に最終報告と言っても
fade awayしていくもんだけど
加藤の生真面目さがそれを許さないだろうw

>>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 共同研究プロジェクトが走っている https://ahgt.math.cnrs.fr/activities/
　ここには、日本の予算もさることながら 仏の予算も入っている。その落とし前が必要となる
５）ところで 数学では「数列の収束加速法」が、古代から研究されている （＾＾
　いまの場合、事態の収束加速法は、事実を隠さずにオープンにして 議論することですね
　Leanコードも隠さずに、オープンにして 議論することが、収束加速の要諦でしょう！

(参考)
https://ja.wikipedia.org/wiki/%E6%95%B0%E5%88%97%E3%81%AE%E5%8A%A0%E9%80%9F%E6%B3%95
数列の加速法
収束の遅い数列を収束の速い数列に変換するアルゴリズムの総称である[1]
歴史
19世紀以前
ヨーロッパと日本で研究が始まった。古典的な二つの加速法はオイラー変換[2] と クンマー変換である。日本では関孝和、建部賢弘など、ヨーロッパではアイザック・ニュートンなどが取り組んだ[3]。

>>445
こいつが国粋🐎🦌のSet Aか

>それをリアル界で決めるのは

LANAプロジェクト
そしてもうほぼアウト

>先週7/17金のLANAプロジェクトの中間発表は
>3.11→3.12導出が 現状ではLean形式化に乗らなかった

もう何年もギャップだといわれていて
改めてそれが分かった時点で、ほぼアウト

>が、可能性は残っている

ダメだという証明ができないだけの話でしかない
実際は、まあアウト

>おそらく 遠アーベルのLeanライブラリー不足で

遠アーベルではなく宇宙際の理論がない

>Leanライブラリーを 何らか追加するとか

何年もそういわれつづけて何もできてないが

>あるいは別に、3.12そのものではなく 3.12をなんらか変形して IUT IVを導けるようにすること

諦めろ　国粋🐎🦌

>>446
>さて、まずこの状況（中間発表）を受けて、
>望月・星氏らが彼ら自身の見解と見通しを
>発表すべきでしょうね

切腹しろってか？（笑）

>というのは、日仏合同の共同研究プロジェクトが走っている
>ここには、日本の予算もさることながら 仏の予算も入っている。
>その落とし前が必要となる

自●しろってか？

Set A　おまえは自●しなくてええんか　国賊

国粋野郎は国賊でしたとさ（嘲）

>>448
ドワンゴ周りは国粋じゃなくて
旧満州(北朝鮮＆中国瀋陽)由来の朝鮮人偽右翼だとあれほど

IUTGtrのプーアノンばりのアイコンで爆笑した

>>449
アイシンギョロとかいう女真族ではなく？（笑）

後金

望月＝頭の良いクズ
セタ＝頭の悪いクズ

>>445 追加
ゴミが湧いているが、ムシムシ

こういうとき
危機管理（下記の存立危機事態までは行ってないだろうがｗ）

１）事実の把握
　そのために、関係者の招集をする
　望月、星、加藤文元、玉川、山下・・などなど
　（一部の人はwebでも可だろうが）
２）そこで状況を説明して 事実共有をする
　Leanコード公開などを決める
３）その後の行動計画を議論する
　施策と役割分担（宿題分担）を決める

次に集まる日時を決める
これを必要なだけ繰り返す
まあ、みんなで知恵をだせば、なんとかなるっぺよ

(参考)
https://ja.wikipedia.org/wiki/%E5%AD%98%E7%AB%8B%E5%8D%B1%E6%A9%9F%E4%BA%8B%E6%85%8B
存立危機事態
台湾有事をめぐる議論
→「高市早苗による台湾有事発言」を参照

アホ

>>454
既に原爆が落とされてる状況で
本土決戦とかいってる🐎🦌

1945年7月26日に、英中米の3か国はポツダム宣言を発し、日本軍の無条件降伏を要求した。
日本政府は、日ソ中立条約があるソ連に和平講和の仲介を託していたが、
8月6日に広島市に原子爆弾が投下され、8月8日未明にソ連対日宣戦布告、
8月9日に長崎市にも原子爆弾が投下されるという重大事態が続いた。

8月10日午前0時3分[2]から行われた御前会議での議論は、
東郷茂徳外相、米内光政海相、平沼騏一郎枢密院議長は、
天皇の地位保障のみを条件とするポツダム宣言受諾を主張、
それに対し阿南惟幾陸相、梅津美治郎陸軍参謀総長、豊田副武軍令部総長は
「受諾には多数の条件をつけるべきで、条件が拒否されたら本土決戦をするべきだ」
と受諾反対を主張した。

しかし、唯一の同盟国となっていた大ドイツ国政府が5月8日に無条件降伏したことで、
イギリスとアメリカ、オーストラリアやカナダなどの連合軍は日本本土に迫っており、
さらに唯一の頼みの綱であった元中立国のソ連も先日の宣戦布告により日本への侵攻を開始しており、
北海道上陸さえ時間の問題であった。

ここで鈴木貫太郎首相が昭和天皇に発言を促し、天皇自身が和平を望んでいることを直接口にしたことにより
御前会議での議論は降伏へと収束し、8月10日の午前3時から行われた閣議で承認された。

日本政府は、ポツダム宣言受諾により全日本軍が降伏を決定する事実を、
8月10日の午前8時に海外向けのラジオ国営放送を通じ、
日本語と英語で3回にわたり世界へ放送し、同
盟通信社からモールス通信で交戦国に直接通知が行われた。

中立国の加瀬俊一スイス公使と岡本季正スウェーデン公使より、
8月11日に両国外務大臣に手渡され、両国より連合国に渡された。

しかしその後も日本政府と軍内部、
特に鈴木首相や東郷外相らと阿南陸相ら陸海軍の上層部内で意見が紛糾し、
御前会議での決定を知らされた陸軍省では、
天皇の元の会議で決定されたにもかかわらず、
徹底抗戦を主張していた多数の将校から激しい反発が巻き起こった。

8月12日午前0時過ぎ、連合国はアメリカのジェームズ・F・バーンズ国務長官による返答、
いわゆる「バーンズ回答」を行った。その回答を一部和訳すると
「降伏の時より、天皇及び日本国政府の国家統治の権限は、
降伏条項の実施の為其の必要と認むる処置を執る連合軍最高司令官に『subject to』する」
というものであった。

外務省は「subject to」を「制限の下に置かれる」だと緩めの翻訳・解釈をしたが、
参謀本部はこれを「隷属する」と曲解して阿南陸相に伝えたため、
軍部強硬派が国体護持について再照会を主張し、鈴木首相もこれに同調した。

8月13日午前9時から行われた、軍と政府の最高戦争指導会議では
「バーンズ回答」をめぐり再度議論が紛糾した上、
この日の閣議は2回行われ、2回目に宣言の即時受諾が優勢となった。

8月14日午前11時より行われた再度の御前会議では、
まだ阿南陸相や梅津陸軍参謀総長らが戦争継続を主張したが
（この時阿南陸相や梅津陸軍参謀総長は陸軍内でクーデターが起こることを認知していた）、
昭和天皇が「私自身はいかになろうと、国民の生命を助けたいと思う。
私が国民に呼び掛けることがよければいつでもマイクの前に立つ。
内閣は至急に終戦に関する詔書を用意して欲しい」と訴えたことで、
鈴木首相は至急詔書勅案奉仕の旨を拝承し、
14日夕方に閣僚による終戦の詔勅への署名、
深夜に昭和天皇による玉音放送が録音された。
夕方に加瀬スイス公使を通じて、宣言受諾に関する詔書を発布した旨、
受諾に伴い各種の用意がある旨が連合国側に伝えられた。

8月15日正午の昭和天皇による玉音放送をもって、
改めてポツダム宣言受諾を全国民と全軍に表明し、
戦闘行為は停止された。

昭和天皇がラジオで国民に向けて直接話すのは
これが初めてのことであった。

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

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

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

>>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　心理編」は次の通り。
あきらめる前に、もう一度考えよう。考えれば手はあるものだ

アホ