Inter-universal geometry と ABC予想 (応援スレ) 53

1 ：１３２人目の素数さん：2021/03/08(月) 09:48:25.28 ID:lrQeWltU.net

テンプレは後で

68 ：１３２人目の素数さん：2021/03/10(水) 18:49:18.97 ID:imsXFuCu.net

>>66
ずいぶん自信満々だけど
あなたのスペックが知りたい
どこ大学なの？

69 ：１３２人目の素数さん：2021/03/10(水) 18:55:11.35 ID:E6r9/wkS.net

>>64
少なくとも査読者の外国人は理解していますよ

70 ：１３２人目の素数さん：2021/03/10(水) 18:57:44.73 ID:EplnUdUQ.net

>>68
ただの会社員ですよ。
出身は、旧帝大のどれかです。

71 ：１３２人目の素数さん：2021/03/10(水) 19:03:48.47 ID:EplnUdUQ.net

>>69
ものが取れないような、
ただのパラドクスも立派な成果ですし、それでいいんじゃないですかね。

「abc が解けた」と考えることとは別の問題な気がします。

72 ：１３２人目の素数さん：2021/03/10(水) 19:04:13.50 ID:yHnn7FCx.net

>>65 ABC予想の解決、などの強い主張には、説明責任が伴います。
　これが果たせない(果たしたとみなせない)なら、
　相対論は間違っているおじさんやフェルマーの簡単な証明おじさんと
　同列の扱いを受けるだけです。
　批判や検証に耐えられないものは学問的に正しいとは認められないし、
　ABC is still a conjectureという結論になるわけです。

73 ：１３２人目の素数さん：2021/03/10(水) 19:06:05.31 ID:EplnUdUQ.net

しかし、「解けた！」

って言ってるようにしか見えないから、反対の皆さん多数いるわけなんでしょうけど…


タルスキが、
質量保存の法則は、誤りで、世界は魔法でできているなんて言っていたら、
お笑い者ですよね。

74 ：１３２人目の素数さん：2021/03/10(水) 20:12:12.73 ID:W1ory5ZA.net

>>70
ギャグセンス高いですね

75 ：１３２人目の素数さん：2021/03/10(水) 21:22:24.27 ID:qDom6aob.net

>>61
>しかし、なんで選択公理でモデル作ったん？
>馬鹿じゃないの？
>って批判は受けて当然ですよね。

ZFにおいて、選択公理はZornの補題と同値
で、Zornの補題は代数学では、基底の存在とか極大イデアルとかが証明される

Zornの補題を捨てると、面白いって話は聞かないし
「なんで選択公理でモデル作った」という批判は、初耳です。IUT論文が発表された2012年から見ているけど

そもそも、IUTの論文中では、選択公理 or Zornの補題は、明示的には使われていなかったと思うけど（圏論ベースの議論が主？）
（見落としているかもしれないが）

https://ja.wikipedia.org/wiki/%E3%83%84%E3%82%A9%E3%83%AB%E3%83%B3%E3%81%AE%E8%A3%9C%E9%A1%8C
ツォルンの補題
命題 (Zorn の補題)
半順序集合Pは、その全ての鎖(つまり、全順序部分集合)がPに上界を持つとする。このとき、Pは少なくともひとつの極大元を持つ。

この補題は関数解析学においてはハーン・バナッハの定理を、線型代数においては基底の存在を、位相空間論においては「任意のコンパクト集合の直積はまたコンパクトである」というチコノフの定理を、そして代数学においては全てのゼロでない（単位元を持つ）環は極大イデアルを持ち、任意の体における代数的閉包の存在をそれぞれ証明する際に使われる。

ツォルンの補題と同値な命題
ツォルンの補題は三つの主要な成果と(ZFにおいて)同値である

ハウスドルフの極大原理
選択公理
整列可能定理
テューキーの補題

76 ：１３２人目の素数さん：2021/03/10(水) 21:43:12.96 ID:EplnUdUQ.net

>>75
見落としてる。
IV のsection3 先に読め。

77 ：１３２人目の素数さん：2021/03/10(水) 21:43:47.25 ID:EplnUdUQ.net

いや、読まんでええけど。
読むだけ無駄やから。

78 ：１３２人目の素数さん：2021/03/10(水) 22:38:57.14 ID:brZVbxEp.net

>>61
選択公理は今の標準的な数学では普通に認められるもんだよ
そんなとこにケチをつける方がアホと思う

79 ：１３２人目の素数さん：2021/03/10(水) 22:42:36.32 ID:brZVbxEp.net

Cor3.12は結局何を主張してるのかな

80 ：１３２人目の素数さん：2021/03/10(水) 22:48:04.04 ID:EplnUdUQ.net

>>78
えっ
まだこんなのいるの？
それはあなたの分野だけであって、モデルつくんのに選択公理は、馬鹿でしょ？って何回も書いてますけど。

81 ：１３２人目の素数さん：2021/03/10(水) 22:48:40.64 ID:EplnUdUQ.net

頭ついてる？

82 ：１３２人目の素数さん：2021/03/10(水) 22:54:51.69 ID:brZVbxEp.net

>>80
数学における大部分はそうだよ。。
そこまで啖呵きったからには
選択公理使用してモデル（集合論の意味でいいのかね？）を作ることがダメなことについて
・望月論文のどこで選択公理を使用してモデルを作ってるか（何ページ番号のどこかを具体的に示すこと）
・選択公理を使用してモデルをつくることがダメな理由
・実際それが説明されてる文献
について説明してな
できなかったら君はただの嘘つきだから

83 ：１３２人目の素数さん：2021/03/10(水) 23:35:13.43 ID:EplnUdUQ.net

>>82
もう指摘してるけど、
頭ついていないまま生きた鶏にあなた、失礼だと思いませんか？

84 ：１３２人目の素数さん：2021/03/10(水) 23:37:40.19 ID:brZVbxEp.net

>>83
じゃあ箇条書きした三点について、君のどのレス番号で言及してるか教えてくれ

85 ：１３２人目の素数さん：2021/03/10(水) 23:40:36.06 ID:EplnUdUQ.net

鶏、頭切り取られても生きてるんだぜ。

お前、なんのために頭付いてるの？
教えてやるよ。
そのマウスカーソルをいくつか上にスクロールして文言を見つけるためだけにお前の脳味噌はついてるんだよ。

86 ：１３２人目の素数さん：2021/03/10(水) 23:42:47.14 ID:brZVbxEp.net

>>85
なんだやっぱ示せてないし大嘘つきじゃん

87 ：１３２人目の素数さん：2021/03/10(水) 23:43:43.86 ID:brZVbxEp.net

示せてるならレス番号書くだけで済むんだよ？こんな簡単なことはないだろ
それができない以上、ようは示せてないってこと

88 ：１３２人目の素数さん：2021/03/10(水) 23:44:19.52 ID:EplnUdUQ.net

>>86
信者乙

89 ：１３２人目の素数さん：2021/03/10(水) 23:44:51.09 ID:EplnUdUQ.net

まじで言ってるの？

90 ：１３２人目の素数さん：2021/03/10(水) 23:47:08.81 ID:brZVbxEp.net

>>88
まあ君が大嘘つきなことはよーく理解した
選択公理とかも最近知って、言いたくなっちゃったんだろうな（君の数学力からして、多分選択公理の正確なステートメントはWikipedia をコピペする以外だと無理だろう。。。）

91 ：１３２人目の素数さん：2021/03/10(水) 23:48:59.17 ID:brZVbxEp.net

既に言及してるなら
・望月論文のどこで選択公理を使用してモデルを作ってるか（何ページ番号のどこかを具体的に示すこと）
・選択公理を使用してモデルをつくることがダメな理由
・実際それが説明されてる文献
について、その「レス番号」を書いてみてよ
本当に言及してるなら、レス番号書けばいいだけじゃん
書けないってことは、示せてないってこと

92 ：１３２人目の素数さん：2021/03/10(水) 23:49:55.08 ID:qDom6aob.net

>>76
>IV のsection3 先に読め。

あのー、「IV のsection3」は、望月先生の編集後記みたいな余興のセクションですよ
下記ご参照。URLが通らないので”ユアペディア” ”宇宙際”くらいで検索して
ああ、確かに批判はあるみたいだね。下記批判を受けて、大分書き直されたみたい

（参考抜粋）
https://ユアペディア.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
宇宙際タイヒミュラー理論

数学基礎論による厳密な定式化
グロタンディーク宇宙や種の言語と呼ばれる理論により宇宙際の議論の数学的定式化の構想をしている。

グロタンディーク宇宙

公理から論理的演繹のみであらゆる数学を展開できるとされる公理的集合論ZFCのモデルとなる集合は、宇宙などと称されることが多い。圏の一般理論はZFCだけでは展開できないが、ZFCに新たに別の公理を加えたZFCGにおいては展開できるようになる。このモデルとなるのがグロタンディーク宇宙である。

ZFCに付け加える公理、つまり論理式によってことなるモデルであるグロタンディーク宇宙が無数に作れるようになる。このとき、ZFCで成り立つ論理式の集まりをひとつの構造とみなす。すると種の理論によって別の構造や種との理論が作られる。種の理論は決定的なアルゴリズムとして利用する。（ただし、通常の自己同型がこの理論では自己言及による非決定性問題となるという困難の解消が必要だという。）このような視点が'宇宙際'幾何という名称の由来となっているとしている。

以下の問題点が指摘されている。

・同じ言語上の二つの理論において、保存的拡大という用語を使用している。特にZFCGはZFCの保存的拡大ではない。
・ZFCは無限個の公理からできている。仮に有限個の公理型に分類しても定式化の仕方によるので9個とは言い切れない。
これらは細部や用語上の問題ではなく、一階述語論理などの基本的な性質に関連するため、Inter-universal Teichmuller Theory IV の Section3 は集合論や数理論理学における文脈では意味をなさない主張になっており、著者が数理論理学について理解をしていない可能性があるという意見がある。（ただし論文の構成上、宇宙際タイヒミュラー理論の正当性とは関係ないとみられている。）

93 ：１３２人目の素数さん：2021/03/10(水) 23:49:59.55 ID:EplnUdUQ.net

飛躍しすぎ、
意味わからんwww

頭ついてないよね。
盲目？

94 ：１３２人目の素数さん：2021/03/10(水) 23:50:36.25 ID:EplnUdUQ.net

>>92
違うやろwwww

頭大丈夫ですか？

95 ：１３２人目の素数さん：2021/03/10(水) 23:51:03.03 ID:EplnUdUQ.net

論文も読めんやばいのいて草www

96 ：１３２人目の素数さん：2021/03/10(水) 23:51:29.74 ID:brZVbxEp.net

>>93
具体的に突っ込まれるとタジタジになる
ま、三流の詐欺師だな

97 ：１３２人目の素数さん：2021/03/10(水) 23:52:10.01 ID:EplnUdUQ.net

そもそも望月の英語読めてるの？www

内容はともかく普通に書かれてるぞ。

98 ：１３２人目の素数さん：2021/03/10(水) 23:54:14.44 ID:EplnUdUQ.net

>>96
タジタジはお前やろwww

IV でモデルについて述べることは一番最初に書いてある。盲目ならしゃあない。

２ちゃんねるも、音声を頼りにやってるんけやな。

99 ：１３２人目の素数さん：2021/03/10(水) 23:59:37.06 ID:brZVbxEp.net

>>98
だからそれは
・何ページのどこか（一番最初とか誤魔化さずに、具体的にどこか示すこと）
・それによる問題点は何かを君の言葉で説明する
・参考となる文献があれば示す
を示して欲しいと言ってるわけだが

それでレス番号について一切書いてない以上、>>83記載の「もう既に指摘してるけど」は完全なる大嘘なわけだよね？

100 ：１３２人目の素数さん：2021/03/11(木) 00:05:26.01 ID:9MePmHqw.net

いや、お前自分で言ってるわけやろ。
ほんで読んだふりして、ここは違う。って、
詐欺師ですやん
wwwww

賛成派の質ww

101 ：１３２人目の素数さん：2021/03/11(木) 00:07:11.76 ID:9MePmHqw.net

「コピペ」ってお前やってることな。
ちなみに言うておくけど。

102 ：１３２人目の素数さん：2021/03/11(木) 00:11:27.01 ID:cXRxfpAy.net

すげーなｗ

学部でちょっと数学かじっただけの会社員風情が
いっちょ前に査読陣に駄目だしできるんだｗ

恐ろしい奴が世の中にはいるもんだ

103 ：１３２人目の素数さん：2021/03/11(木) 00:17:09.16 ID:A+IMn0lH.net

>>79
＞Cor3.12は結局何を主張してるのかな

その質問は、
ブライアンコンラッドが、
IUTシンポジュームでスライドを見せられたときに
同様の質問をしたとか読んだ気がするが
見つけられなかったな
ただ、Cor3.12は難しいらしいね（下記）
（参考）
http://taro-nishino.blogspot.com/2019/03/blog-post070.html
TARO-NISHINOの日記
識別の危機
3月 24, 2019

イニシャルPSで通っている数学者が"論文が出現した直後から私は系3.12の証明の中の図3.8以降のロジックを全く分からないと注意している"3と書いた。彼だけではなかった。ブライアン・コンラドは"私は審査過程が最終的に3.12の証明を完全に明らかにした改訂に当然つながるだろうと思った"4と書いた。噂は間違いだと判明したが、望月は系3.12をはっきりさせることを何もしなかった。"ミスプリントを正した"と彼は変更履歴の中に書いて括弧を削除した5。これはコンラッドが予期していた改訂の類には見えない。

PSは数論幾何学における研究でフィールズ賞を受賞したピータ・ショルツだと判明した。2018年の3月、ショルツとジェイコブ・スティクスは彼等の懸念を議論するために京都に望月を訪問した。会合は内部者達だけに知られていたが、数か月後常識となった6。どちら側も他を納得させられなかった。

104 ：１３２人目の素数さん：2021/03/11(木) 00:17:14.50 ID:QVbPlyma.net

>>100
日本語になってないな
>>83で書いてる「もう既に指摘してるけど」はどのレス番号を指してるのか、早く示してくれ
それか適当なことを言ってしまったと認めろ

105 ：１３２人目の素数さん：2021/03/11(木) 00:20:28.83 ID:9MePmHqw.net

ちょっと一日黙っててね。
あぼーんするので :-)

106 ：１３２人目の素数さん：2021/03/11(木) 00:22:44.74 ID:QVbPlyma.net

Cor3.12は知る人が見れば（証明ができるかは別にして）直感的に明らかなものなんだろうか
ABC予想の主張自体は非常に非自明ではあるけど、それが直感的には明らかかもしれないCor3.12に置き換わってるなら、とても意義のあることのように思う

107 ：１３２人目の素数さん：2021/03/11(木) 00:23:44.62 ID:QVbPlyma.net

>>105
効きすぎてて草

108 ：１３２人目の素数さん：2021/03/11(木) 00:39:14.00 ID:50kZehgD.net

初めて来たもんだが、
直感的に明らかな選択公理を認めると、バナッハ=タルスキーみたいな非自明な定理ができるということか？

109 ：１３２人目の素数さん：2021/03/11(木) 00:47:06.19 ID:9MePmHqw.net

>>108

直感的に自明だと言うのは、思い込みではないんか？

なぜならば、
我々の知ってる全ての関数を定義するためには、
連続体濃度回数選択する必要はないでしょ。

110 ：１３２人目の素数さん：2021/03/11(木) 07:18:27.99 ID:2i+RmBSU.net

IUTのabc以外の具体的な応用で注目すべきものっていうのはあるのかね？

111 ：１３２人目の素数さん：2021/03/11(木) 07:55:55.51 ID:A+IMn0lH.net

>>92
自己レス
(引用開始)
>IV のsection3 先に読め。
あのー、「IV のsection3」は、望月先生の編集後記みたいな余興のセクションですよ
下記ご参照。URLが通らないので”ユアペディア” ”宇宙際”くらいで検索して
ああ、確かに批判はあるみたいだね。下記批判を受けて、大分書き直されたみたい
(引用終り)

1）「IV のsection3」をもう一度読み直してみたが、「IV のsection3」はなくてIVの論文は数学的には成り立っている
2）つまり、「IV のsection3」はあくまで補足説明です
3）「IV のsection3」の中で、望月先生が説明しているが、選択公理は必要と考えているみたいですね
4）単純に考えて、ZFとZFCとの比較で、Cが加わっているだけ、証明できる定理が増えて豊かになっている
（おもちゃのレゴのブロックみたく、”C”というブロックが増えた分だけ、作れるものが増える。
　ZF⊂ZFCみたいな。ZFで証明できる定理は全て、ZFCでも証明できる）
5）なので、”C”を抜けという話が分からない。ZFだけってこと？　それとも、”C”（選択公理）の代わりになにか追加するのかな？
　IUTは、20世紀までの現代数学を存分に使った成果の上に成り立っている
　”C”（選択公理）を抜いて、IUTは成り立たないのでは？

発言の意図が分からない

112 ：１３２人目の素数さん：2021/03/11(木) 09:02:21.70 ID:9MePmHqw.net

>>111

ZF がおかしいんじゃねーのか。


解析的に何でも扱うことができる。
とした20世紀の数学が誤り。
解析的考えから、synthetic な数学へ戻るべきだってのがモデル理論の現在。


あんなカスみたいなタワー作ってもうたら、連続体濃度一瞬で超えてまう。
元取れなくなって当たり前。

そもそもZF iff ZFC も集合論という解析的枠組みで示されただけだろ？


いっぺん

Univalence Axiom 調べてみ。
公理のあり方が全く、
今までのものと異なるから。


ホモトピーから公理をつくったら、
次元に対しての真理が、公理に含まれている。

グロタンディーク学派が、21世紀の頭から、やっている仕事に対して、モッチーが前世紀の間違いを持ってきて、発表しただけなのはおわかりいただけただろうか。

113 ：１３２人目の素数さん：2021/03/11(木) 09:04:40.47 ID:9MePmHqw.net

モデルの素人が「とんでもな」モデル作って、
ただ無視されてるだけ。

114 ：１３２人目の素数さん：2021/03/11(木) 09:10:37.20 ID:2i+RmBSU.net

この件は明確な決着つかずに消えそうなにかね。そうなると問題は京都周辺だなぁ。
数学の国際的な社会から京都が孤立しないといいけどね。
宇宙際よりも国際の方が現実的だからな。

115 ：１３２人目の素数さん：2021/03/11(木) 09:19:39.26 ID:+6M65SfV.net

>>94
IV のsection3に随分詳しいみたいだが質問していい？

116 ：１３２人目の素数さん：2021/03/11(木) 09:23:06.11 ID:9MePmHqw.net

タオ、ショルツ、はじめ、フィールズ賞レベルは、そのあたりの話が合意形成が取れていて、第一課題として選択関数を回避する作業が、水面下で着々と行われている。

ZFC はアウトやと大体みんなおもとるけど、
メンツや過去の仕事に対する敬意などがあるから、大きく口を開いてアウトとは言わん。
それをあんたらが勘違いして、ガラパゴスしてるわけや。ただ空気読めん人ら。


わざわざ、ショルツが来て、
元取れるんか？って聞いたけど、
答えられんのやろ？

元も取れん非自明な集合なんて、
集合論やと、いくらでもつくれてまう。

元が取れるかどうか、
ってのは、根源的な問題であり、
Synthetic な立場では、
それか明確な言葉として、組み込まれている。


モデルとして本当に正しいんかZF(C) は？
カスみたいなモデルが正しく動いていることを立証するには、それが、パラドクスでなく、実際に元が取れていることを説明する必要がある。

117 ：１３２人目の素数さん：2021/03/11(木) 09:24:19.65 ID:9MePmHqw.net

>>115
詳しくはない。
否定するのに必要な材料だけ読んだだけ。

118 ：１３２人目の素数さん：2021/03/11(木) 09:27:51.49 ID:+6M65SfV.net

>>117
きちんと読まないと「余興のセクション」を否定するには足りない

119 ：１３２人目の素数さん：2021/03/11(木) 09:30:29.47 ID:9MePmHqw.net

>>118
余興ではない。
論文の冒頭読め。

120 ：１３２人目の素数さん：2021/03/11(木) 09:44:50.21 ID:+6M65SfV.net

>>119
論文の冒頭であるIUT IV,P3の「Finally, in §3,」から続く文章を見ると、「極めてナイーブ/非専門家の観点ではありますが」とあるが

121 ：１３２人目の素数さん：2021/03/11(木) 09:50:29.25 ID:9MePmHqw.net

>>120
んならIUT はただの立派なパラドクスやろ。
abc 解決ではない。

122 ：１３２人目の素数さん：2021/03/11(木) 09:55:09.17 ID:2i+RmBSU.net

abc予想はおいておいて、IUTの数学全般もしくは数論幾何における応用力はどう評価されているのか？
昔「角の三等分家」という専門家をこまらせるアマチュアについて書かれた記事の中で、
一人の三等分家が書いた「120度の三等分」という分厚い自費出版書というが言及されていたが、
その本の「方法」は「120度だけに有効なものであった」そうな。。
IUTがそんなものではないことを祈る。何かいろいろ応用の広いものであることがよい普及理由になるしね。
まあ、まずはその正しさが広く認められるのが先かもしれないが。。。

123 ：１３２人目の素数さん：2021/03/11(木) 10:46:44.73 ID:+6M65SfV.net

>>121
一応タオもショルツもIVはCor 3.12とは無関係と結論づけてるから、パラドクスではないんだろう
まあそんな非専門家の論文の査読を通す理由はよく分からないが……

124 ：１３２人目の素数さん：2021/03/11(木) 10:56:10.81 ID:+6M65SfV.net

§2までを査読して§3はカット、というなら(Cor3.12の問題は残るが)まだ分かるが、EMSを見るとIVのページ数がそんなに変わってないので、§3を査読してアクセプトしたということになる
だが、数学的に意味を成していないアイデア出しを権威のある雑誌がアクセプトするなんてことあるのか？

125 ：１３２人目の素数さん：2021/03/11(木) 11:04:58.05 ID:sM1ssJOA.net

>>112
>ZF がおかしいんじゃねーのか。
>Univalence Axiom 調べてみ。
>公理のあり方が全く、
>今までのものと異なるから。

１．”Univalence Axiom”は、検索すると、Homotopy type theoryか（下記）
２．Steve Awodey先生ね。圏論の基礎だったかのあとがきにあったね
３．Voevodskyが、”Univalence Axiom”を提案して、定理のコンピュータ証明が前進したとかね（Voevodskyは、若くして亡くなったが）
４．でな、Homotopy type theoryは、ZFなりZFCを包含しているんじゃね？
　つまり、ZF ⊃ ZFC ⊃ Homotopy type theory （記号の濫用）
５．私見だが、ZFやZFCは、基本は一階述語論理なんだわ
　で、高階論理使いたいって話があって、圏論使えばやれるかもってのは昔からある。Homotopy type theoryもそれかね？（素人なんで詳しくないが）
６．戻ると、Homotopy type theory は、ZFCの定理は全て証明できるのでないと、コンピュータ証明には使えないよね
　（物理では、新（量子）力学は古典（ニュートン）力学を包含し、ある極限では古典力学と一致するべきという、ボーアの指導原理があるよ
　　数学でも同じで、ZFCで導かれる有用な定理が、Homotopy type theory で導けないなら、「使えないんじゃね？」となると思うよ）
７．文句のつけ方間違ってない？
８．それと、Univalenceの”Univa”と、Inter-universal の”Univa”と、”Univa”繋がりだけど、両者の意味は全く別物だろ？
９．あと「IV のsection3」は、モデルを作っているのではなく、「望月IUTをモデルで説明したらこうなる」という単なる解説と読むべきですよ
以上
つづく

126 ：１３２人目の素数さん：2021/03/11(木) 11:05:59.47 ID:sM1ssJOA.net

>>125
つづき
（参考）
https://en.wikipedia.org/wiki/Homotopy_type_theory
Homotopy type theory

Contents
1 History
1.1 Prehistory: the groupoid model
1.2 Early history: model categories and higher groupoids
1.3 The univalence axiom, synthetic homotopy theory, and higher inductive types

4 Key concepts
4.1 "Propositions as types"
4.2 Equality
4.3 Type equivalence
4.4 The univalence axiom

5 Applications
5.1 Theorem proving
5.2 Computer programming

Early history: model categories and higher groupoids
The first higher-dimensional models of intensional type theory were constructed by Steve Awodey and his student Michael Warren in 2005 using Quillen model categories.

The univalence axiom, synthetic homotopy theory, and higher inductive types
The concept of a univalent fibration was introduced by Voevodsky in early 2006.[16]

The univalence axiom
The univalence axiom states that this function is itself an equivalence.[27]:115 Therefore, we have
(A=B)＝〜 (A＝〜 B)
"In other words, identity is equivalent to equivalence. In particular, one may say that 'equivalent types are identical'."[27]:4

127 ：１３２人目の素数さん：2021/03/11(木) 11:08:12.07 ID:9MePmHqw.net

>>123

ほんなら、ただのイカレタ論文じゃねえか。
IV はIUT の土台と書いてあって、そこに ZFC の上に、イカレタタワー拵えて、勝手に宇宙の果定めてる、人間に、フィールズ賞とった数学者が一週間も時間をそのためだけにわざわざ時間をとって、指摘してもらっといて、

カスみたいなブログで、
うんこ晒して、

まじで日本の恥やな。

128 ：１３２人目の素数さん：2021/03/11(木) 11:10:41.33 ID:sM1ssJOA.net

>>125 訂正

　つまり、ZF ⊃ ZFC ⊃ Homotopy type theory （記号の濫用）
　　↓
　つまり、ZF ⊂ ZFC ⊂ Homotopy type theory （記号の濫用）

すまん、
包含関係の記号が逆だった（＾＾；

129 ：１３２人目の素数さん：2021/03/11(木) 11:20:19.35 ID:2i+RmBSU.net

理論といいながら、この分野のベテランとも言える望月氏の経験値をもとにした、
力技の「解法」なのかもしれないね。ところどころ証明ではなく「直観的」になっているような。
正しいけど、説明不足であり、本人には感覚的に説明の必要性が実感できない。
ただ、相互理解という点では望月氏に若干非があると思う。

130 ：１３２人目の素数さん：2021/03/11(木) 11:20:56.42 ID:sM1ssJOA.net

>>227
>IV はIUT の土台と書いてあって、そこに ZFC の上に、イカレタタワー拵えて、勝手に宇宙の果定めてる、人間に、フィールズ賞とった数学者が一週間も時間をそのためだけにわざわざ時間>をとって、指摘してもらっといて、

・おれの主張は、>>125-126 >>128(訂正)な
・事実を曲げちゃいけないね
　「フィールズ賞とった数学者」ではないよね、時間軸
　議論は、2018年3月。フィールズ賞は2018年8月だった（と思う）
　なので「フィールズ賞とりそうな数学者」だな。森重文先生は、分かっていたと思うが
・ショルツェ氏の指摘は、「ZF？ ZFC？ だめだめ。”The univalence axiom”使え〜！」って主張ではないよね
　論点ずれているよ

事実を曲げちゃいけないね

131 ：１３２人目の素数さん：2021/03/11(木) 11:25:50.02 ID:sM1ssJOA.net

>>129
>正しいけど、説明不足であり、本人には感覚的に説明の必要性が実感できない。
>ただ、相互理解という点では望月氏に若干非があると思う。

同意
望月先生の文、難しいよね
IUT誘いとか
その点、中村博昭先生の文は丁寧だね
中村博昭先生に、IUTの解説書いてほしいな

132 ：１３２人目の素数さん：2021/03/11(木) 11:34:54.72 ID:9MePmHqw.net

>>130
論点ずらしてるのはお前。
世界の数学者の直感は、IUT でなくホモトピー。

説明不足はその通り。
正しいことはまるで実証されていない。
直感は尊重するが、望月は仕事をしていない。

133 ：１３２人目の素数さん：2021/03/11(木) 11:37:31.16 ID:9MePmHqw.net

>>125
素人意見で草w

HoTT はコンピュータで証明するためのマシンに過ぎん。

134 ：１３２人目の素数さん：2021/03/11(木) 11:49:04.43 ID:9MePmHqw.net

>>125

お前の脳みそで理解するような包含なんてしてねーよww

オブジェクトを層化することで古典的な、排中律の理論をひっくるめることができるわけで、ZFC なんて成り立つわけ無いだろww

135 ：１３２人目の素数さん：2021/03/11(木) 11:53:10.38 ID:9MePmHqw.net

圏論まともにやってりゃ、
オブジェクトが集合論における「集合」とは全く異なる概念だと理解できるはずだが…

136 ：１３２人目の素数さん：2021/03/11(木) 12:04:00.72 ID:sM1ssJOA.net

>>131-135
なんか、論旨メタメタだね

＞世界の数学者の直感は、IUT でなくホモトピー。

意味わからん

＞正しいことはまるで実証されていない。


「IUTをコンピュータ検証にかけろ」
という意見は、初期からあるけど
やれるなら、やってみなよ

＞HoTT はコンピュータで証明するためのマシンに過ぎん。

それいうなら、まだしも
”HoTT はコンピュータで証明するための一つのロジックに過ぎん。”じゃね？

で、問題になっている証明が、コンピュータ処理しやすくなるってことは
多分、人間にも分かりやすいってことだと思う

>オブジェクトを層化することで古典的な、排中律の理論をひっくるめることができるわけで、ZFC なんて成り立つわけ無いだろww

なんか、おかしくね？ ”ZFC なんて成り立つわけ無いだろ”？ なんか、おかしくね

>圏論まともにやってりゃ、
>オブジェクトが集合論における「集合」とは全く異なる概念だと理解できるはずだが…

？ 米田の補題は？

あと
望月IUTが、ZFC風に書かれているとして
それを、Homotopy type theory（HoTT）で書き直したら、すっきり表現できて
正しいか間違いかも、分かりやすくなるというならば

こんなところで、グダグダいわずに、それさっさと論文にしなよ
玄人気取りさん

137 ：１３２人目の素数さん：2021/03/11(木) 12:11:01.70 ID:9MePmHqw.net

>>136
なんで会社員の俺が、オタクに刺されるリスクを犯してわざわざ泥塗らんとあかんねん。

俺は今の生活で結構や。

子供のために、コンピュータを使いやすくすることが、最優先課題なんで望月みたいな偏見の塊になんて構ってられん。

HoTT は今後も修整されることはあるだろうが、人間が証明する有限ステップをコンピュータで再現することは、可能だという検証機の役割を外されることはまずない。

その意味で、HoTT は重要な出発点であることは確か。

IUT が同様に重要なら、それなりの方法できちんとモノを示さないといけない。

138 ：１３２人目の素数さん：2021/03/11(木) 12:13:03.52 ID:sM1ssJOA.net

>>136
>>圏論まともにやってりゃ、
>>オブジェクトが集合論における「集合」とは全く異なる概念だと理解できるはずだが…
>？ 米田の補題は？

米田の補題なんて、全く詳しくないけど
なんか、”米田の補題”ってキーワードが浮かぶんだけど？（＾＾

https://ja.wikipedia.org/wiki/%E7%B1%B3%E7%94%B0%E3%81%AE%E8%A3%9C%E9%A1%8C
米田の補題

米田の補題（よねだのほだい、英: Yoneda lemma）とは、小さなhom集合をもつ圏 C について、共変hom関手 hom(A, -) : C → Set から集合値関手 F : C → Set への自然変換と、集合である対象 F(A) の要素との間に一対一対応が存在するという定理である。 名称は米田信夫に因む。

概要
局所的に小さい（locally small）圏を C とする、すなわち各対象 A, B に対して hom(A, B) は集合であるとする。対象Aを固定するとき、C の各対象 B に対して集合（Set の対象）hom(A,B) を割り当てる関数は、C から Set への関手の対象関数として考えることができる。この関手は大抵 hA = hom(A, -) : C → Set と表記され、共変hom関手（covariant hom functor）と呼ばれる。

ここで、 F : C → Set を任意の集合値関手とし、hA から F へのすべての自然変換 θ : hA {\displaystyle {\dot {\rightarrow }}}{\dot {\rightarrow }} F のクラス[1] Nat(hA, F) [2]について考える。

米田の補題の骨子は、射 hA(f) = hom(A, f) : hom(A, A) → hom(A, B) の恒等射 1A に対する特性

hom(A, f)1A ＝ f
である[3]。

139 ：１３２人目の素数さん：2021/03/11(木) 12:14:35.96 ID:9MePmHqw.net

逆にいうが、複素解析の正しい直感があるなら、
あるいは、不安定ホモトピー を正しく見れてるなら、HoTT の枠組みを拡大してそれこそ新理論ができるんでないか？

140 ：１３２人目の素数さん：2021/03/11(木) 12:17:08.59 ID:9MePmHqw.net

米田は、
圏論ではオブジェクトの中身が見えん。

それを外に出す（externalize）するための道具。

米田の補題の舞台は presheaf だ。
これが重要だということくらい聞いたことがあるだろう。

141 ：１３２人目の素数さん：2021/03/11(木) 12:17:25.19 ID:sM1ssJOA.net

>>137
＞その意味で、HoTT は重要な出発点であることは確か。
＞IUT が同様に重要なら、それなりの方法できちんとモノを示さないといけない。

なんかへん
・IUTとHoTT とを、並列に等置することが間違いでは？
・IUTはディオファントスの数論の論文であって、
　数学基礎論でも、圏論でも、ロジックのコンピュータ検証プログラムに寄与するものでもありませんよ

142 ：１３２人目の素数さん：2021/03/11(木) 12:25:37.56 ID:9MePmHqw.net

だいたい、現代理論は、
圏と層
で語られる。

オブジェクトの中身を見れるようにした「米田」と
オブジェクトに対して排中律的な考え方を適用できるようにした「層化」

これが現代の理論の中核で
半世紀前からある数学者の常識。

いつまでも複素解析"だけ"をやって、
正則行列の自明な同値命題を並べて喜んでいてはいかんのだよ。

143 ：１３２人目の素数さん：2021/03/11(木) 12:29:45.31 ID:9MePmHqw.net

>>141
お前が変。

混乱してる。
俺は別に数論がどうこういうてないし、
数論はしらん。

ペレルマンの論文やらも、タウはおかしいかもおもてるなど、数学者にとって、何が正しいかどうかわかったもんじゃない。

そこに、基礎のあり方として、
ZFC を考えようというのは、
おかしいから、数学者はいろいろ感考えてるんやろ。

144 ：１３２人目の素数さん：2021/03/11(木) 12:43:37.66 ID:9MePmHqw.net

>>141
検証機で証明したものは、
検証機が正しく、かつ、
アホな定義でもない限り、かつ、
余計な公理がなければ、必ず正しく、
再現ができる。

数論の分野では、
選択公理が認められていることは、知ってる。さらに、もしかしたら、数論をするには、HoTT の公理だけでは足らんかもしれん。とも聞く。

あるいは、数論の結果で真理と異なるものが、混じっている可能性もある。

しかし、分野が変われば、そうでないところがある。量子論なんかは、わりかし証明器での証明が進んでいる。

そんなさなか、「あのタワーはないわ。」
って誰もが感じてる。

俺が言いたいのはそれだけ。
むしろ、p-adic teichmuller について教えてほしい。

145 ：１３２人目の素数さん：2021/03/11(木) 13:01:35.43 ID:2i+RmBSU.net

STAPの時に同じ分野の研究者の様子をいろいろ記事で読んでいた時に、みな各人己の仕事で忙しいわけで、
その時間を疑わしい論文の検証なぞに使うのはなかなか難しいものだという、考えれば当たり前のことに気づいたけど。
IUTも同じようなところがあるね。STAPは同じ理研の若い研究者がかなりきちんと反論したからすごいなと思ったけど、
STAPはそういう身内から実のある批判が出てきていろいろ見えてくるとよいのだけどね。
なんか、みんな望月氏になんも言えない感じ（と外からは見られている）だね。

146 ：１３２人目の素数さん：2021/03/11(木) 13:03:31.17 ID:2i+RmBSU.net

STAPはそういう身内から実のある批判が出てきていろいろ見えてくるとよいのだけどね。
STAP→IUT

147 ：１３２人目の素数さん：2021/03/11(木) 13:16:17.10 ID:sM1ssJOA.net

>>139
>逆にいうが、複素解析の正しい直感があるなら、
>あるいは、不安定ホモトピー を正しく見れてるなら、HoTT の枠組みを拡大してそれこそ新理論ができるんでないか？

その議論は、スレ違い

>>140
>米田は、
>圏論ではオブジェクトの中身が見えん。
>それを外に出す（externalize）するための道具。

いや、
言いたいことは
オブジェクトと集合が全く別ものというから
出したんだけど？

あと繰り返しだが
１）IUT IV論文のセクション3は、あくまで付けたしの感想文程度
　数学基礎論の新モデル提案でもないし、新理論でコンピュータロジックに貢献しようというのでもない
２）但し、望月先生は主観として「グロタンディーク宇宙」からヒントを得て、”Inter-universal ”を着想したのでしょうね
３）それをIUT IV論文のセクション3を書いたけど、「宇宙」の定義がはっきりしない。なので、それもあって、かえって混乱したようにも思います

148 ：１３２人目の素数さん：2021/03/11(木) 13:19:21.34 ID:9MePmHqw.net

>>147
あぼーんやな、また明日。

149 ：１３２人目の素数さん：2021/03/11(木) 13:29:49.03 ID:sM1ssJOA.net

>>144
>むしろ、p-adic teichmuller について教えてほしい。

https://ja.wikipedia.org/wiki/P%E9%80%B2%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
P進タイヒミュラー理論

http://www.kurims.kyoto-u.ac.jp/~motizuki/papers-japanese.html
望月論文
p進Teichmuller理論（PDFへのリンクは原文からたどれ）
[1] A Theory of Ordinary p-adic Curves. PDF Comments NEW !! (2011-07-15)
[2] Foundations of p-adic Teichmuller Theory. Comments NEW !! (2018-04-03)
[3] An Introduction to p-adic Teichmuller Theory. PDF

>>145-146
>STAPはそういう身内から実のある批判が出てきていろいろ見えてくるとよいのだけどね。
>なんか、みんな望月氏になんも言えない感じ（と外からは見られている）だね。

あのー
「なんも言えない」つーけど
印刷版の序文に名を連ねるお歴々は
望月先生より格上の人もいるよね
数学で、STAPみたいなゴマカシは通用しないと、みんな思ってますよ（当然）

150 ：１３２人目の素数さん：2021/03/11(木) 13:35:48.80 ID:2i+RmBSU.net

ワイルズのフェルマー予想の時も一度「ギャップ」が指摘されたのだったよね。
それを1年以上かけて修正して受け入れられていったわけだよね。
どうしてそういうことがIUTでは起きないのだろう。。。
望月氏はギャップ指摘自体が「誤った認識をもとにした指摘」であると言っているわけだよね。
それが去年のブログで書いている「よんさん」と「きゅーさん」の喩えなわけだ。
ワイルズの時と同じ状況ではないということなんだろうけど、素人には数学でそんな認識自体の「ギャップ」が起こるのかと思う。

151 ：１３２人目の素数さん：2021/03/11(木) 13:54:58.73 ID:sM1ssJOA.net

>>140
>米田は、
>圏論ではオブジェクトの中身が見えん。
>それを外に出す（externalize）するための道具。
>米田の補題の舞台は presheaf だ。

なるほど
この人、いいこというね
（参考）
http://www.is.nagoya-u.ac.jp/dep-ss/phil/kukita/others/Yonedas_lemma.pdf
米田埋め込みと米田の補題
久木田水生
Cate 研 2011 年 10 月 20 日

2 米田埋め込み
Definition 2.1 (前層). 任意の圏 C に対して Cop から Set への関手からなる関手圏 SetCop を C 上の前層
presheaf と呼ぶ．
米田埋め込みは任意の局所小圏 C から SetCop への埋め込み関手である．本節では米田埋め込みの定義と
米田の補題の証明を行う．
（引用終り）

>>142
>だいたい、現代理論は、
>圏と層
>で語られる。

なるほど
https://ja.wikipedia.org/wiki/%E3%83%88%E3%83%9D%E3%82%B9_(%E6%95%B0%E5%AD%A6)
トポス（topos）とは、位相空間上の層のなす圏を一般化した概念である。アレクサンドル・グロタンディークによるヴェイユ予想解決に向けた代数幾何学の変革の中で、数論的な図形（スキーム）の上で有意義なホモトピー・コホモロジー的量が定義できる細かい「位相」を考えるために導入された。 その後数理論理学者たちによる更なる公理化を経て、集合論のモデルを与える枠組みとしても認識されるようになった。
目次
1 定義
2 グロタンディーク・トポス
2.1 古典的な層の理論との対応
3 分類トポス
4 数理論理学との関わり
5 歴史

152 ：１３２人目の素数さん：2021/03/11(木) 14:40:48.21 ID:pyJ5obj9.net

外部と交流せず、周りのイエスマンとだけ付き合ってきた結果、
ああいうピエロが生まれるわけだ。

153 ：１３２人目の素数さん：2021/03/11(木) 14:56:42.79 ID:sM1ssJOA.net

>>152
>外部と交流せず、周りのイエスマンとだけ付き合ってきた結果、

事実を曲げてはいけません
１）IUTの国際シンポジウムは何度もやった。国内もね
２）英 フェセンコ先生、米 Dupuy氏、Joshi氏、仏リール大の方々
　国内では、東京工大が一大勢力で、あと阪大の安田先生とか、勿論京大とRIMSはいうに及ばず
３）正当な指摘には、きちんと対応してきたよ
　IUTの論文内に記述がある

事実を曲げてはいけません
・今年４回の国際会議

まあ、見ていれば
IUTが着々と前進していることが分かるだろう

154 ：１３２人目の素数さん：2021/03/11(木) 15:05:26.71 ID:2i+RmBSU.net

全然素人だから、表面的なものしか見えていないけど、海外の反応の中にいまだに懐疑的なものが少なくないわけで、
理解者、肯定者が増えてきているのであれば、その懐疑を一般の人にもアピールするような仕方で払拭すべきではないのかなぁ。
少なくとも、望月氏側が歩み寄っていない印象があるのが残念。
ペレルマンの時は彼があまり社交的な人ではなかったけども、論文自体は肯定的に受け取られていた印象がある。

155 ：１３２人目の素数さん：2021/03/11(木) 15:33:54.08 ID:EDOyqx0E.net

>>116
いや、例えば
Peter Scholze, Lecturers on Condensed Mathematics.
で、the category of κ-condensed abelian groupsがcompact projective objectsで生成されることの証明に、Zorn's lemmaを使ってるが

156 ：１３２人目の素数さん：2021/03/11(木) 15:39:31.55 ID:9MePmHqw.net

>>155
話読めよ。
そこで、数論のモデル作るような大それたことしとらんやろww

157 ：１３２人目の素数さん：2021/03/11(木) 17:11:19.37 ID:D9quWJCg.net

とりあえず無理に変な関西弁使わないでいただいて

158 ：１３２人目の素数さん：2021/03/11(木) 17:25:01.39 ID:sM1ssJOA.net

>>111
選択公理文献貼るよ

https://fuchinoddojp/books/intro-to-set-theory-and-constructibilitypdf
「ゲーデルと20世紀の論理学 第4巻」（東京大学出版会 2007）
渕野昌執筆第1部
(平成 27 年 5 月 11 日)
目 次
第 I 部 構成的集合と公理的集合論入門 1
第 1 章 公理的集合論 7
11 ツェルメロ=フレンケル集合論 7
12 集合論の 1 階の論理での公理化 18
13 クラスとベルナイス=ゲーデル集合論 23
第 2 章 公理的集合論の展開 29
21 整列順序 30
22 数学的帰納法による証明と関数の再帰的定義 36
23 順序数 44
24 基数 54
25 基数算術 62
26 共終数 66
27 連続体仮説 68
第 3 章 集合論のモデル 79
31 論理式の相対化と絶対性 79
32 比較的簡単な相対的無矛盾性の証明 91
33 集合論の内部での論理とモデル理論 95
第 4 章 構成的集合と強制法 101
41 構成的集合 101
42 強制法 109

P18
現代の数学的議論では次の選択公理 (Axiom of Choice) が頻繁に用いられる
P19
バナッハ=タルスキーの逆理など，我々の物˙ 理˙ 的直観と ˙
相容れない結果を導くこともあるため，問題視されることもある．それにも
かかわらずこの公理が通常仮定されるのは，
(110) Shoenfield の絶対性定理により，集合論での命題として表したとき
にそれほど複雑な形にならない数学的命題については14)，ZFC で
の証明が得られれば，それから選択公理を用いない証明を作りなお
すことができること；
(111) 選択公理のオルタナティヴと考えられる決定性公理の成り立つ世界
は，選択公理の成り立つ集合論の「宇宙」の内部モデルとしてとら
えることができること — ウディン (H Woodin) による（本書第 II
部を参照）；
そして何よりもまず，
(112) 選択公理の仮定のもとで展開される数学が非常に豊かなものである
こと，
などがその理由として挙げられるだろう15)．選択公理なしでは証明できない
命題の例としては，線型空間の基底の存在定理や極大イデアルの存在定理，
ハーン=バナッハの定理，非可測集合の存在定理などがあげられる．

P20
1.2 集合論の 1 階の論理での公理化

159 ：１３２人目の素数さん：2021/03/11(木) 17:28:25.09 ID:sM1ssJOA.net

>>158
選択公理追加
石井大海さん
貼るよ

https://konn-san.com/math/forcing-axiom-and-choice.pdf
強い選択公理としての強制公理
石井大海
2017/11/14 00:49:10 JST
概要
強制公理（Forcing Axiom）とは，ある種類の強制法による拡大と現在の宇宙がある意味で「近い」こと
を述べる公理ですが，これは Zorn の補題や従属選択公理（DC）の一般化と見ることも可能です．後者の
説明は，強制法の理論に関する知識が必要ないため，集合論以外の分野の人にもある程度理解しやすいこと
が期待されます．
そこで本稿では，強制公理の強い選出原理としての側面に焦点を当てて，強制法に馴染みの無い人にも強
制公理がどんなものなのかを解説し，ついでに強制法とは何かについても軽く説明していきたいと思いま
す．対象読者層としては，学部三〜四年程度の数学を知っていて Zorn の補題を使って何かを作る議論をし
たことがあれば十分なようにしたつもりです．
1 復習：選択公理と Zorn の補題，従属選択公理
選択公理が現代数学にとって不可欠な公理であることは，構成的数学や直観主義数学を別にすれば，多くの
数学者が認める所だろう．実際，次に挙げるような命題は，全て選択公理から導かれる：

定理 1 (ZFC). 次は ZFC の定理：
(1) 任意のベクトル空間は基底を持つ．
(2) Krull の定理：任意の単位的可換環は真の極大イデアルを持つ．
(3) Tychonoff の定理：コンパクト空間の任意集合個の直積はコンパクト．
(4) Baire の範疇定理：完備距離空間の可算個の稠密開集合の共通部分は稠密．

160 ：１３２人目の素数さん：2021/03/11(木) 17:30:04.84 ID:0JuCmY9q.net

今のトレンドは選択公理の可否じゃなくて
決定性公理でどこまでいけるかだぞ

161 ：１３２人目の素数さん：2021/03/11(木) 17:40:13.06 ID:9MePmHqw.net

>>160
ww

162 ：１３２人目の素数さん：2021/03/11(木) 19:27:20.17 ID:vs2ZylVF.net

∞-圏のことならなんでも知ってるっぽい ID:9MePmHqw さんに質問
たかが2-圏のことですけど

Q1. 2-圏で”円盤”ってどう定義されますか？
Q2. 2-圏で”球面”ってどう定義されますか？
Q3. 2-圏で”円筒”（２つ穴の球面）ってどう定義されますか？
Q4. 2-圏で”トーラス”ってどう定義されますか？
Q5. 2-圏で”パンツ”（３つ穴の球面）ってどう定義されますか？
Q6. 2-圏で”１つ穴開きトーラス”ってどう定義されますか？
Q7. 2-圏で”種数ｎの向きづけ可能曲面”ってどう定義されますか？

どれもこれも ID:9MePmHqw さんにとっては
瞬時に答えられる簡単な問題でしょうけど、
無知蒙昧な我々をお導きください_(_　_)_

163 ：１３２人目の素数さん：2021/03/11(木) 21:13:24.04 ID:9MePmHqw.net

球面の場合、
trivial な 2path 以外に nontrivial な nonpath を定義すればよいだけ。
以下同様。お前が考えろクソボケ、どうらいけんもしらん、正則行列自明リストオタクが、いっぺん4 んでこい。

164 ：１３２人目の素数さん：2021/03/11(木) 23:20:46.81 ID:9MePmHqw.net

nonpath て誤字っとるやないか 2path

4ね！

165 ：１３２人目の素数さん：2021/03/11(木) 23:42:27.31 ID:0whnWeR3.net

>>160
まぁ実際そうだよね
プロはもう選択公理の話題には食傷気味になっている

166 ：１３２人目の素数さん：2021/03/12(金) 06:29:45.68 ID:UFmX6v8k.net

>>103
>＞Cor3.12は結局何を主張してるのかな
>その質問は、
>ブライアンコンラッドが、
>IUTシンポジュームでスライドを見せられたときに
>同様の質問をしたとか読んだ気がするが

追加
下記でもご参照
（正直、私はDupuy氏が書いていることを理解した訳ではないが）

https://arxiv.org/abs/2004.13228
The Statement of Mochizuki's Corollary 3.12, Initial Theta Data, and the First Two Indeterminacies
Taylor Dupuy, Anton Hilado [v1] Tue, 28 Apr 2020

The present paper concerns the setup of Corollary 3.12 and the first two indeterminacies, the second \cite{Dupuy2020c} concerns log-Kummer correspondences and ind3, and the third \cite{Dupuy2020b} concerns applications to Diophantine inequalities (in the style of IUT4). These manuscripts are designed to provide enough definitions and background to give readers the ability to apply Mochizuki's statements in their own investigations. Along the way, we have faithfully simplified a number of definitions, given new auxillary definitions, and phrased the material in a way to maximize the differences between Theorem 1.10 of IUT4 and Corollary 3.12 of IUT3. It is our hope that doing so will enable creative readers to derive interesting and perhaps unforeseen consequences Mochizuki's inequality.

(PDF)
https://arxiv.org/pdf/2004.13228.pdf
1. Introduction
It has been almost seven years since Mochizuki first released his manuscripts online and the
content of his inequality remains poorly understood today. In fact, at the time of the Oxford
workshop in December 2015, things were so opaque that Brian Conrad famously asked during
one of the sessions whether Mochizuki’s inequality even represented an inequality of two real
numbers. We have come a long way since then. (Let us begin by stating unambiguously
that Mochizuki’s inequality is an inequality of real numbers.)

167 ：１３２人目の素数さん：2021/03/12(金) 07:47:11.86 ID:MvPZmcVm.net

こういう高度な数学の内容というのは、何か実験的なアプローチで検証できないのかね？
計算機による形式化された検証というのはあるみたいだけど、そもそもIUTが形式化に不向きなのかね。

168 ：１３２人目の素数さん：2021/03/12(金) 08:08:41.09 ID:K3P8iupM.net

>>163
Q1. 2-圏で”円盤”ってどう定義されますか？
→trivial な 2path
Q2. 2-圏で”球面”ってどう定義されますか？
→上記の他、nontrivial な 2path を定義すればよい

有り難う御座います_(_　_)_

で、後5つはどうなりますか?

Q3. 2-圏で”円筒”（２つ穴の球面）ってどう定義されますか？
Q4. 2-圏で”トーラス”ってどう定義されますか？
Q5. 2-圏で”パンツ”（３つ穴の球面）ってどう定義されますか？
Q6. 2-圏で”１つ穴開きトーラス”ってどう定義されますか？
Q7. 2-圏で”種数ｎの向きづけ可能曲面”ってどう定義されますか？

瞬時に答えられる簡単な問題でしょうけど、
無知蒙昧な我々をお導きください_(_　_)_