[過去ﾛｸﾞ] Interuniversal geometry とABC 予想60
(1002ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
1(1): 03/26(木)21:43 ID:XTPL032M(1/5) AAS
未だにcontroversialなIU幾何やABC予想に関する会話のサロンとして使って下さい。
荒らしはご遠慮願います
2(2): 03/26(木)21:46 ID:XTPL032M(2/5) AAS
>>1
IUT応援スレと区別.混乱の防止のため、応援.信奉者の書き込みやこのスレのレスを応援スレへ引用は固く遠慮ねがいます 。
懐疑的な意見や関係者等の匿名の
論理的な擁護は歓迎です。
3(2): 03/26(木)21:47 ID:XTPL032M(3/5) AAS
>>2
前スレ
Inter-universal geometry とABC 予想59
4: 03/26(木)21:51 ID:XTPL032M(4/5) AAS
>>3
2chｽﾚ:math
5: 03/26(木)21:54 ID:XTPL032M(5/5) AAS
テンプレや資料は
前スレ Inter-universal geometry とABC 予想59などを参照下さい。
6(2): 03/31(火)23:52 ID:k/sIZtir(1) AAS
動画ﾘﾝｸ[YouTube]
7(2): 04/03(金)00:23 ID:EK1Ym4za(1) AAS
・Scholze-Stix（2018）は
「この図式を具体的に追うと、pilot objectのconcrete normalizationを入れると矛盾（または平凡化）する」
と具体的な反例・計算の道筋を示した。
・望月側は「それは単純化の誤り」と返すが、その「誤り」を避けた具体的な計算例・修正図式を第三者に見せられていない。
・Taylor Dupuyや一部のセミナー、Kirti Joshiの試みでも、
「ここで定義が曖昧で進められない」「Θ-pilotの扱いが追えない」
で詰まる報告が繰り返されている（2025年以降も進展報告なし）。
・2026年現在も
「具体的な楕円曲線（例：y² = x³ - x + 1 とか）で、Hodge theaterを1つ構築→Θ-link→log-link→不等式の数値評価」
のような最小限のtoy exampleすら公開・検証されたものがない。
8: 04/04(土)09:20 ID:NRfbTVfw(1) AAS
>>6
共同通信記者からケドレヤへ最後の質問は良かった。
9: 04/04(土)11:00 ID:yuM6gHuI(1/2) AAS
詳しい人が居ると面白いですね
もう1つのスレとは大違い
ところでlogが出てくるのは
別々にした積と和とを比較したいからなんですか？
10: 04/04(土)12:07 ID:dBkU46tJ(1/2) AAS
LANAプロジェクトにフェセンコが参加してないのはどうしてなんだろ
ZMC副所長でIUT理解者のはずなのに不自然じゃないですか？
記者会見によればプロジェクト構成員は
コアメンバー５名＋学生やポスドクなどの若手メンバー７名
ってことだったけど
11(1): 04/04(土)14:36 ID:C5zRkjXW(1/2) AAS
あえて望月ホルホルと見られてる輩は省いてる
スターだけは理論を理解するのにひとりは理解者が必要だろうとのことで入ってる
まあまあ望月と違って人もいいし丁寧に解説してくれるしな
12(1): 04/04(土)16:52 ID:dBkU46tJ(2/2) AAS
>>11
加藤と星が入ってる時点でフェセンコだけ外す意味なくね？
13(1): 04/04(土)18:11 ID:C5zRkjXW(2/2) AAS
>>12
加藤は一番理解してないのでカウントする必要ないな
フェセンコもまあ似たような理解だからな
役立たずのエセ理解者は最悪いらないけど、加藤はセンター長で、望月の腰巾着だから役目的にやらざるを得ない
14: 04/04(土)21:37 ID:iYZ75soN(1) AAS
>>7
>最小限のtoy example
そのレベルのことは論文執筆前の研究段階で嫌というほどやっててしかるべきなのに一つも出ないと
つまり実態を何一つ伴わない絵空事ってことか
ショルツェってめちゃくちゃナイスガイだね そんな絵空事を邪険にせず絵空事と分るように説明してくれたんだから
15(1): 04/04(土)21:38 ID:yuM6gHuI(2/2) AAS
>>13
>加藤は一番理解してない
ベストセラー書いたじゃん
あれで理解してないとかないわ
16: 04/05(日)04:47 ID:4xAsCVqr(1) AAS
>>15
肝心の3.12のブラックボックスは正直わからんと言ってた
世間はそれを「理解した」とは言わん
17(2): 04/06(月)11:04 ID:hVzOYkPT(1) AAS
伝え聞いた内部情報によると、LANA側は3.12の形式化を終えてギャップがあるという理解、は確定らしく、星を除く4名の結論は「限りなく誤り」
→しかし望月に聞いてもそれは違うの反応
→星が引き続き望月の手となり足となりLANA側に説明
7/17までに前向きな方向に行くのは難しいんじゃないの？
18: 04/06(月)12:07 ID:/cN+osS3(1) AAS
形式化ってもっとすごい時間が掛かるものかと思っていたけど、もうそんなに話が進んでいるのね。
19(1): 04/06(月)12:45 ID:s7vb23ls(1/2) AAS
>>17
デジャブで草
まんま8年前の望月とショルツェのやり取りじゃんｗ
20(1): 04/06(月)15:28 ID:CenSn2NL(1/4) AAS
>>19
ま、ショルツの2018年の論文はとある数論幾何の大家に「それは正しくない」と言われたみたいだから、ショルツが正しい、という当時の風潮は間違ってたことになってるのよね
21(4): 04/06(月)17:40 ID:GdEpdi6S(1/3) AAS
> とある数論幾何の大家
誰ですか？
サイディならマッチポンプで利益相反
だ
・IUTTの「理解者」は基本的にこの世に望月新一提唱者しかいない。
➖➖
IUTTの検証.進捗情報の報告
2014年12月現在
京大数理解析研究所教授.望月新一
>それらのテーマ(絶対遠アーベル幾何」や 「エタール.テ-タ関数の剛性性質」 「Hode.Arakelov理論)精通している研究者は(私自身を除けば)この世に存在しないのが実情です。
省1
22: 04/06(月)17:46 ID:GdEpdi6S(2/3) AAS
>>21
外部ﾘﾝｸ[pdf]:www.kurims.kyoto-u.ac.jp
23: 04/06(月)17:56 ID:F/SFnIZj(1) AAS
>>17
MSはこの期に及んでまだ自分の誤りを認めない
しかし自分は表にでず星に説明させる
星はMSに逆らえないので板挟み
星 このままだと●うんじゃないかな？
24: 04/06(月)18:40 ID:8+nhUUiI(1) AAS
天才レベル「鬼」：俺の理論が理解できない専門家は馬鹿
天才レベル「竜」：俺の理論が形式化できないLEANは無能
天才レベル「神」：俺の理論がフィットしないZFCは欠陥品
25: 04/06(月)18:59 ID:s7vb23ls(2/2) AAS
災害レベルやろ
26: 04/06(月)21:20 ID:CenSn2NL(2/4) AAS
>>21
ケドラヤだよ
27(1): 04/06(月)22:02 ID:GdEpdi6S(3/3) AAS
ケドレヤはIUTの理解者でありません
28(1): 04/06(月)22:11 ID:uNuhBh7s(1/2) AAS
>>20
その人が「正しくない」と言ったのが「正しい」？
29: 04/06(月)22:21 ID:CenSn2NL(3/4) AAS
>>27
いわゆるabc予想解決の3.12以外の部分のケドラヤの評価はポジティブだよ
30(1): 04/06(月)22:23 ID:CenSn2NL(4/4) AAS
>>28
検証チームが一年半議論してるからな、その結果は正しいんだろうよ、少なくとも外野の騒音よりはな
31(1): 04/06(月)22:27 ID:uNuhBh7s(2/2) AAS
>>30
つまりその人が「正しくない」と入ったのはLANAの検証作業過程を経た上での見解だということ？
32(1): 04/07(火)00:12 ID:AC2TF102(1/3) AAS
定理3.11から系3.12を導く論理について、LANAプロジェクトのメンバーの多くが、その中に何か超えられない壁があると感じている
33(2): 04/07(火)00:16 ID:jcor7xMj(1/3) AAS
それ、ショルツェが8年前に言ったそのまんま
34: 04/07(火)03:44 ID:3MtsO/lO(1/3) AAS
>>33
でもショルツの8年前のペーパーは正しいわけでなく、見解の相違がある
35: 04/07(火)03:44 ID:3MtsO/lO(2/3) AAS
>>31
そうだよ
36(1): 04/07(火)03:46 ID:3MtsO/lO(3/3) AAS
>>32
そうだね
でも検証の結果、ショルツも正しいとは言えないことも分かったようだよ
37: 04/07(火)04:42 ID:AC2TF102(2/3) AAS
そんなこと書いてないよ
38(1): 04/07(火)05:39 ID:4y4GADNM(1/4) AAS
>>36
そのことはどこから分かりますか？もしや内部情報？
39(1): 04/07(火)07:23 ID:Xqd4HQ+p(1/4) AAS
iut論文はnot even wrongで
誰でも一意に解釈できるようには書かれてない
s-sが主張したのはzfcの枠内で「彼らなりに」解釈すると
3.12を出せるほど強くないということ
同時に
別の解釈が成立したとしてどの可換図式が成り立つのか？
というchallengeを提案してる
だからs-sの解釈は誤解だって主張をするには
「ではiutを成立させる正しい解釈は何ですか？」に
答えられなければならない
省6
40: 04/07(火)07:37 ID:Xqd4HQ+p(2/4) AAS
さらに言えばs-s文書は
なぜiutが成立しないか
を説明したもので具体的なギャップを指摘したものではない
それに対してLANAが目指してるのは
具体的なギャップの有無を診断すること
だから目指してる場所が違う
41(2): 04/07(火)09:31 ID:jTXHI/bk(1/3) AAS
>>38
331のLANA記者会見の議事録
42(2): 04/07(火)09:36 ID:jTXHI/bk(2/3) AAS
>>39
SSの指摘は的外れという事実は確かで、それが正しい指摘だと喚いて乗っかっていた無関係の人々は恥を知れということ
かといって望月理論であることはが正しいともいえないわけだが、SSのあれが決定打というわけでもない
43: 04/07(火)09:49 ID:G9KM3QY/(1/3) AAS
>>21
重複などを訂正
「関わっている 数名の研究者(サイディ.山下剛.星)を除けば、世界の 全ての数論幾何の研究者(=連続論文が公開された時点.2012年8月での山下剛氏も含めて)はIUTの周辺にある数学に関しては「全くの素人」であり、での山下剛氏も含めて)はIUTの周辺にある数学に関しては「全くの素人」であり、これまでの研究業績の上に成り立っている「深い理解」を活用してIUTの成否に関する決定的な(=数学的に意味がある」)判定を下す資格が本質的にありません
↓
「既にIUTの検証活動に関わっている 数名の研究者(サイディ.山下剛.星)を除けば、世界の 全ての数論幾何の研究者(=連続論文が公開された時点.2012年8月での山下剛氏も含めて)はIUTの周辺にある数学に関しては「全くの素人」であり、これまでの研究業績の上に成り立っている「深い理解」を活用してIUTの成否に関する決定的な(=数学的に意味がある」)判定を下す資格が本質的にありません
44: 04/07(火)09:53 ID:G9KM3QY/(2/3) AAS
・キラン・ケドレヤ.Kiran Kedlaya。
望月新一ブログでNHKスペシャルの発言をダメ出しされた自称望月IUT信奉者Dupuyに近く、>IUTの周辺にある数学に関しては「全くの素人」かつ形式化も素人。
・望月新一認定IUT理解者(習熟)。
2014年12月3名(サイディ.山下剛.星)
2020年2月IUT論文受理時でも10人未満。
IUTの研究普及(布教？)が主目的の次世代幾何学研究センター(望月新一センター長)関連のメンバーは
森重文.柏原正樹 .清水達郎
玉川安騎男 .望月拓郎..
Kedlayaもfesenkoも認定理解者
の枠の外らしい
45: 04/07(火)09:53 ID:ACpvD+ha(1) AAS
よくわからない
46: 04/07(火)10:17 ID:G9KM3QY/(3/3) AAS
なぜケドレヤがIUT検証のメンバーなの
か、よくわからない。
共同通信記者からケドレヤへ質問は
よかった
47: 04/07(火)11:23 ID:jTXHI/bk(3/3) AAS
ケドラヤはこの一年半でIUTに習熟したらしい
ただし定理3.11から系3.12の飛躍はよくわからない（他の検証チームも同じ）
少なくとも外野の誰よりも数論幾何に詳しいし、IUTにも詳しい
そんな人の発言は重い
48: 04/07(火)12:45 ID:JeQLCzda(1) AAS
>>42
正しいかどうか判定して居た人は居ないでしょうよ
かなりの権威から指摘があったという事実だけで十分では？
49(1): 04/07(火)14:18 ID:AC2TF102(3/3) AAS
SSの指摘は的外れなんて言ってないじゃん
50: 04/07(火)19:59 ID:4y4GADNM(2/4) AAS
>>41
３３１？
51(1): 04/07(火)20:44 ID:Xqd4HQ+p(3/4) AAS
>>42 全く的外れではない
以下、数学が分かる人向け：
例えばjoshiに対する望月及びscholzeの批判は
（原理上）完全に正しいというわけにはいかないが
的を射ているという話
外部ﾘﾝｸ:mathoverflow.net
52(1): 04/07(火)21:11 ID:jFfiIrwe(1/2) AAS
>>49
正しいから望月アウト、とも言ってないぜ
53: 04/07(火)21:12 ID:jFfiIrwe(2/2) AAS
>>51
ケドラヤは「認識の違い」と言ってるぜ
54: 04/07(火)21:33 ID:Xqd4HQ+p(4/4) AAS
そもそも認識の相違の余地がある数学論文がダメダメ
別の解釈が数学として成立すればs-sに批判を回避できる
s-sもその可能性を否定していない
ただ別の解釈が成立するというなら
それを説明しろ
どう成立するか示してみろ
と言っている
十数年たって今更なんか起こる蓋然性なんてほぼないと思うが
どのような結論が出ようが
iut論文が証明責任を果たしてない
省1
55: 04/07(火)21:39 ID:jcor7xMj(2/3) AAS
>そもそも認識の相違の余地がある数学論文がダメダメ
その通り
56: 04/07(火)21:41 ID:jcor7xMj(3/3) AAS
だから not even wrong と評される
57: 04/07(火)21:43 ID:4y4GADNM(3/4) AAS
>>52
なんだ
正しくないなんて言ってないんだ
58: 04/07(火)22:25 ID:4y4GADNM(4/4) AAS
>>41
>LANA記者会見の議事録
公開されてるのそれ？
59: 04/08(水)02:03 ID:vaPI7+/u(1) AAS
記者会見の議事録では、
記者からの質問が削除してある。
>>6
60: 04/08(水)02:13 ID:lw7P/G19(1) AAS
望月アウトとは言っていない、だからSSの指摘は的外れということなんだ！
？？？？？？
61: 04/08(水)20:59 ID:dZTjN4Bw(1/2) AAS
LANA記者会見とMの新年blogから分かったのは
LANAが躓いてるって箇所がMが素人である「基礎論」部分ってこと
対するMの言い分が「当たり前」や「専門家も認めている」だけじゃ
深刻なred flagと言えるんジャマイカ
「基礎論」部分への疑義は論文公表時からあったわけで
外部ﾘﾝｸ:quomodocumque.wordpress.com
外部ﾘﾝｸ:inference-review.com （"Model theorists"以下）
加えて「基礎論」部分こそが問題の核心だってS-Sの指摘もあったんだから
外部ﾘﾝｸ[pdf]:ncatlab.org
外部ﾘﾝｸ[pdf]:www.kurims.kyoto-u.ac.jp （§4(T1), (T2)）
省15
62: 04/08(水)21:13 ID:6Td7DQgv(1/2) AAS
数学板にも基礎論を軽視、ややもすると差別するような発言が見受けられるが、やっぱ基礎論は大事やねえ〜
ま、数学の基礎付けをする学問なんだから言うに及ばずか
63: 04/08(水)21:41 ID:Tpw5aZqI(1/2) AAS
ここはabc予想のスレだから、今の京都の現状を話せばそれで良いのではないか。
64: 04/08(水)21:42 ID:dZTjN4Bw(2/2) AAS
いやいや「基礎論」なんてフツーの数学者にはイランじゃろ
テンパって
＞いわば現代の数学では、禁じ手になってるようなことも取り入れて、
＞何かできないかということを考えたということなんですね
みたいなことを始めない限りは
65: 04/08(水)21:46 ID:Tpw5aZqI(2/2) AAS
桶は桶屋で良いんじゃね。
自分の生き残りのポストを掴む為に頑張れば、最低限良いのではないか。
数学者でない人がガヤガヤ言うものではないと思う。
66: 04/08(水)22:32 ID:6Td7DQgv(2/2) AAS
みたいなことを始める基礎論音痴が多いのが現実
67(1): 04/09(木)03:27 ID:d20JIJ4D(1/4) AAS
MSが公開したスライドを見たが、実際にできたのは
MS論文には書かれていないTh3.11.5からCor3.12を導く証明
Th3.11からTh3.11.5を導けるかどうかは現在奮闘中
あと、ZFCのLeanによる形式化云々のところで名前が出てくる
Shogo Saitoは、東北大学にいる数理論理学の研究者らしい
外部ﾘﾝｸ:sites.google.com
68: 04/09(木)03:33 ID:d20JIJ4D(2/4) AAS
なお、3.11.5 (=3.11+Rmk. 3.9.5) らしい
69(2): 04/09(木)06:01 ID:EqPOXqMH(1/9) AAS
>>67
>MSが公開したスライド
どこにあるんですか？
70(2): 04/09(木)06:12 ID:d20JIJ4D(3/4) AAS
>>69
外部ﾘﾝｸ[pdf]:www.kurims.kyoto-u.ac.jp
71(1): 04/09(木)06:27 ID:EqPOXqMH(2/9) AAS
>>69
ありがとうございます
証明の正しさが検証されるまでもう少しですね
72(1): 04/09(木)06:41 ID:d20JIJ4D(4/4) AAS
>>71
3.11.5⇒3.12はOKだとしても
3.11⇒3.11.5でNGと判明しそうな悪寒…
73: 04/09(木)07:23 ID:2q0zBkRC(1/4) AAS
>>70
species/mutationの理論の射程が
＞independent of any particular model ZFC set theory!
とか強調してて、この人、完全性定理とか全く理解してないでしょ
（論文にZFCGがZFCの保存拡大だなんて書いてたくらいだから）
そんなもんはspecies/mutationとかのワケワカ独自理論でなく
圏と関手の枠組みで論じることが出来るはずです
＞ZFC as a first order theory
のくだりも何かものすごくヘンなことを考えてるでしょ
人間に無限を扱う能力があるみたいな
省12
74: 04/09(木)07:52 ID:EqPOXqMH(3/9) AAS
メタ数学が要らないでは無くて
lIUT全体をleanに落とし込む必要なしにleanに落とし込まれたZFCを使って種／変種を定式化できるだろう
といっているのでは？
つまり
この概念はIUT全体の成否にかかわらず
leanによって正しいと認められそうだと言いたいのかな？
75: 04/09(木)07:58 ID:2q0zBkRC(2/4) AAS
ああその通り
species/mutations理論の形式化がいらないかも
って言ってるだけでした
76: 04/09(木)10:28 ID:EqPOXqMH(4/9) AAS
>>72
そもそも3.11は正しいの？
77(1): 04/09(木)10:49 ID:JcdXFJ++(1/5) AAS
From a purely technical point of view, the essence of LeanForm —atleast in the case of IUT — lies in undertaking a fundamental reorganization of the theory into suitable purely formal/combinatorial blackboxes
純粋に技術的視点から、Lean形式の核心は−少なくともIUTの場合−理論の、適切で純粋に形式的/組合せ的なブラックボックス群（数学の群ではなく”むれ”の意）への抜本的再編制を保証することの中にある
要するに「理論をブラックボックス群へ再編制することがLean形式化の核心だ」と言っている。
それは別に否定しないが、ブラックボックスはあくまでブラックボックスだから、最終ゴールである完全形式化に向けての（かなり手前の）中間ゴールだろと思う。
しかもその中間ゴールへの途上で早くも「超えられない壁」にブチ当たっている。
つまり「最終ゴールは遥か彼方にあって今の段階では目途の立て様が無い」という進捗ってことなんだろう。知らんけど。
78(1): 04/09(木)10:52 ID:EqPOXqMH(5/9) AAS
>>77
やっぱleanによる形式化って
全数学を基礎から検証するようなものじゃなくて
ある程度の共通認識をブラックボックス化して
そこから形式的に導けるかだけ検証するってことか
これまでのライブラリってのも
全部そういうものなのかな？
79(1): 04/09(木)10:56 ID:JcdXFJ++(2/5) AAS
だってブラックボックス群への再編制が完了したからって「そのブラックボックス達はそれぞれ本当に正しいの？」に答えられないじゃん
80: 04/09(木)11:02 ID:EqPOXqMH(6/9) AAS
それともこれまでのライブラリってZFCから全部導出してるの？
最近気になってるのが
順序対(x,y)={{x},{x,y}}と定義していいのかとか
写像f:A→BをP(A×B)の部分集合とみなしていいのかとか
P(A)と2^A={f:A→2}を同一視していいのかとか
直和A+Bを(A∪B)×2の部分集合と見ていいのかとか
ZFCにおける「解釈」みたいなのはZFCの一部じゃないよなってこと
こういう「解釈」もleanに折り込んでるとすると
ZFCよりより武器が多いものになってないのかな？
81: 04/09(木)11:02 ID:EqPOXqMH(7/9) AAS
>>79
だよねー
82: 04/09(木)11:02 ID:JcdXFJ++(3/5) AAS
AIに聞いたら
・ブラックボックスは望月が初めて言い出した概念
・ブラックボックス無しの完全形式化が達成されない限り証明を検証したことにならない
だとさ
ま、そうだわな
83: 04/09(木)11:19 ID:JcdXFJ++(4/5) AAS
>>78
>これまでのライブラリってのも
>全部そういうものなのかな？
AIいわく
ライブラリ＝検証済み
ブラックボックス＝未検証、つまり単なる仮定
理論のブラックボックス群への再編は一般的なLean検証では用いられない独自の方法論
とのこと
84(1): 04/09(木)11:23 ID:JcdXFJ++(5/5) AAS
まあLean形式化はIUT論争を長引かせることが目的の確信犯的アクションなんじゃね？とも思えてしまう
85: 04/09(木)11:41 ID:EqPOXqMH(8/9) AAS
>>84
なるほど
86(1): 04/09(木)20:46 ID:2q0zBkRC(3/4) AAS
LEAN形式化の過程で幾つかの定理をブラックボックスとして
使うのは普通のことです
例えばBuzzardのFLT形式化プロジェクトでも1990年以前の結果で
形式化されてないものはブラックボックスとして使うと言っています
しかし今回のようにブラックボックスそのものに疑義がある場合
moduloブラックボックスの形式化にどのような意義があるのか不明です
>>70の文書のSkeletal Lean codeが何を示唆しているのか不明です
そもそも>>70の文書はmoduloブラックボックスで形式化するとも
言ってないのでこの議論自体無意味なのかもしれないよ
87(1): 04/09(木)21:51 ID:EqPOXqMH(9/9) AAS
>>86
>1990年以前の結果で
>形式化されてないものはブラックボックスとして使う
全くダメじゃん
19世紀までの数学は全部検証して始めて意味がある
88: 04/09(木)22:04 ID:2q0zBkRC(4/4) AAS
>>87
1990年以前の結果はwell-documentedだから
早晩AIで自動形式化できるようになるでしょう
詳しくはAITPMでBuzzard講演のスライドでも見てくださいな
89(1): 04/10(金)08:05 ID:PiV+adzo(1/2) AAS
ブラックボックス化自体が悪、とはいわない
何が証明されてないかが明確に意識されていれば構わない
今回、系3.12が”定理”3.11.5から導けたといってるから
証明されてない予想は、系3.12から”定理”3.11.5に移った
”定理”3.11から”定理”3.11.5は証明できるか？
なんともいえないが、今ここでつまってそうな感じがする
90(1): 04/10(金)08:08 ID:+ehfyzLa(1/2) AAS
>>89
>”定理”3.11から”定理”3.11.5は証明できるか？
定理3.11が成立することは
誰もが合意できているんですかね？
91(1): 04/10(金)08:14 ID:PiV+adzo(2/2) AAS
>>90
>定理3.11が成立することは誰もが合意できているんですかね？
そんなこといってないよ
もし、”定理”3.11から”定理”3.11.5が証明できたら、
今度は証明されてない予想が、”定理”3.11.5から”定理”3.11に移る
それだけ
これをつづけていくことで、自明な前提まで遡れれば、証明の正しさが認められる
自明な前提がどこなのか？ さあ
LANAの人に聞いてくれ（笑）
92: 04/10(金)10:30 ID:HwiXYTux(1) AAS
ショルツの指摘はまあ普通に回答されるべき質問ではあるわな。
あれに変ないちゃもんつける方がどうかしてる
93: 04/10(金)11:01 ID:kk9Dwm0v(1/2) AAS
>>91
そんな手法でいいんですかね
上から引き下ろしていくんじゃなくて
下から積み上げていくのが数学でしょうに
IUTの最初からその正しさを検証していくのかと思ってました
94: 04/10(金)11:26 ID:YuSWdLD+(1/5) AAS
上からでも下からでも完全に形式化された瞬間が証明完了。それまでは未完了。
95(1): 04/10(金)11:57 ID:kk9Dwm0v(2/2) AAS
そりゃそうですが
IUTは最初の方はあんまりおかしなところがないというのが共通認識なのかなあ
それとも
その辺におかしなところがあるなしにかかわらず
Th3.11→Th3.11.5→Cor3.12
が正しいと分かればあとはどうにか
よってたかってTh3.11の証明ができれば良いから
何とかなるんじゃないかという希望的観測も？
96: 04/10(金)13:24 ID:Ms9Bi2om(1) AAS
>>95
ねーよw
問題ない部分は部品パートだろ
97: 04/10(金)20:15 ID:QhMfyZk3(1) AAS
系3.12が定理3.11.5から導けたって、アンタ、誇大広告でしょ
（実際、望月氏もそんなこと言ってないっすね）
望月氏はもともと定理3.11から系3.12が導けるって主張してるワケ
中間定理3.11.5を形式化して
そこから3.12が出ることを形式化したってんのなら
それなりにスゲーけど
望月氏の言う"Skeletal Lean code"ってナニ？
LEANの世界でもワケワカの独自用語でdiscommunication？
98: 04/10(金)22:00 ID:YuSWdLD+(2/5) AAS
>望月氏の言う"Skeletal Lean code"ってナニ？
ブラックボックス間の論理的つながりをコード化したもの、つまり「こんなことを考えてるよ」を伝えるためのもの（as a communication tool）で、証明の検証からは程遠いもの
じゃね？ 知らんけど
99: 04/10(金)22:05 ID:YuSWdLD+(3/5) AAS
なにかと独自用語を持ち出すのは、要するに、検証としての進捗が皆無であることに対して鋭意推進中と言い訳するための言葉が必要だから
100: 04/10(金)22:08 ID:YuSWdLD+(4/5) AAS
独自用語を持ち出さないと「進捗ゼロ」という報告にしかならないが、それだと予算取れない
上下前次1-新書関写板覧索設栞歴
あと 902 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.037s