Interuniversal geometry とABC 予想61 



未だにcontroversialなIU幾何やABC予想に関する会話のサロンとして使って下さい。

荒らしはご遠慮願います。

ほんとIUT擁護派はゴミしかいねーよな
っていうか数匹しかいないけど

>>675
じゃあもう無理なんじゃない？

IUT擁護派は文盲やから何も読めんのや
あっても都合悪きゃ見えないメクラチョン

「間違ってすら居ない」ってよく書いてる人いるけど
それは
既存数学で証明も反証もできないだろうちう意味よね？
全く新しい言明であって
それが既存数学と独立であろうという見立て
（その見立てが正しいかどうかも不明だけど）
でも
そうであっても一階述語論理で表現はできる筈だから
検証に乗せることができないとおかしい

∃G,∀x∈G:P(x)∈G
が論証も反証もできないのと同じで

>>84
>・Taylor Dupuyや一部のセミナー、Kirti Joshiの試みでも、
>「ここで定義が曖昧で進められない」「Θ-pilotの扱いが追えない」
>で詰まる報告が繰り返されている（2025年以降も進展報告なし）。
ちう意味じゃね？

>>687
それなら
間違ってる
んじゃね？

定義が曖昧というのは正しいか間違いかを論ずる以前じゃね？

概念が正しく定義されてないならそら間違いだろうよ

なぜ？

>>691
定義がないから

俺はF1もモチーフも胡散臭く感じてるけど
スローガンとして？持つのは妨げられない
しかし定義も無いモノを使って何かを論じるのは
間違いジャネ？

＞「間違ってすら居ない」ってよく書いてる人いるけど
＞それは
＞既存数学で証明も反証もできないだろうちう意味よね？

違う
「証明を成していない」って意味
もっとはっきり言えば
「同時代の専門家が認める水準の証明を成していない」
って意味

たとえばだけど、神様が目の前に現れて
「リーマン予想は正しい、証明は自明」
って言ったら、これは間違ってる？
証明の詳細を聞き返しても、
「自分と同様の専門知識を身に着ければわかる」
って言われるの
それならLeanコードをくださいっていうのを
今やってるところ

>>693 その通り

「君はバカである」はどうならバカかが未定義だから正しいとも間違いとも言えないのでは？　間違ってすらいないとしか言えなくね？

>定義も無いモノを使って何かを論じるのは間違いジャネ？
ん？　君は行為の正誤を述べてるの？　ならまず行為の正誤の定義をしないと

概念が未定義で命題とされるものが実は命題になってなければ当然証明も反証もできないが、
ある理論と独立な命題もやはりそうだから、それらは区別すべきだよ。
>既存数学で証明も反証もできないだろうちう意味よね？
では区別できない。

例えば選択公理はZFで証明も反証もできないが、IUTのように「間違ってすらいない」と評されることは無いだろう

>>697
IUTを「間違ってすらいない」と書いているのがその意味
つまり
CはZFでは証明も反証もできないだろうちう意味だと思ったので>>685,686と書いたけど
そうではなくて
「定義がなされていない」ちう意味なら
そりゃ「間違ってすらいない」でなくて「間違ってる」んじゃないかな

まあいいや
>>685,686という意味で無いってことが分かったからいいや

ID:FLhHZHETの言う通りですが
とりあえず分かったようでなによりです

『定義が曖昧』『証明がない』ということは
数学的な真偽を判定する材料がないということ
だから「間違いですらない（not even wrong）」
議論の進め方や態度の問題とは切り分けないと

ついでにはっきり言っておくと、
『正しいかどうかわからないから、まだ解決したかどうか未定だ』
なんて態度は、社会のルールとして完全に間違っている
「証明がある」と言い張るなら、そう主張する側が責任を持って、
同時代の専門家たちが納得する証拠を出さなきゃいけない
それができないなら「証明はない」と判断される
『究極的には正しいかも』、『将来いつか認められるかも』
なんていい言い訳は証明責任のルールの前に通用しない

IUTは間違ってすらいない
IUTによるABC予想の証明は間違い

そう「間違ってすらいない」
だから反例もない
それをID:Lb3Gyp67に理解しろというのは無理な注文か

scholzeの数学は通常の数学に基づく発展だ。

一方、
現在は「パラダイムシフト」期で
望月新一IUT論文は大論文だから、数理論理学や数学基礎論に拘束されないと明言してる。
(scholze stix望月星のミーティングでscholze stixの質問に答えられず謎のIUT語やイノベーションを持ち出した)
↓
➖➖
川上量生企画望月新一監修加藤文元著IUT本から

・本文　p66.
論文の価値は何で決まるのか
>何をもって「新しい」と判断できるのか、「正しい」という基準は何か、という点は非常に専門的なポイントです。
>通常の発展時においては当面の題材やその時代における支配的な問題に対する部分的なあるいは最終的な解決であったりしますが、 「パラダイムシフト」期においては、当分野に革命を起こすような大論文であることもあるでしょう

・ 本文p69
「興味深い」ということ　
>私は以前、望月教授に「望月さんの理論が発表されたら、
数論の専門家より数理論理学や数学基礎論の人たちの方が興味をもつでしょうね」と話したことがある。
実際、IUT理論はABC予想やその ディオファントス問題の
研究におけるそれまでの発展の文脈からは
一線を画しています。
(略 )
>それはこの分野における最先端に 位置する研究であるというより、 数学の非常に基本的なレベルでの イノベーションを企画したもの だからです。

>>702
うーんでも判例出されちゃってるからアウト

プライドの肥大した数学者が間違いの指摘を受け入れなかったってだけの話なんだよなこれ

ゴミかゴミクズかの違いで
not even wrongにイメージだけでこだわってるバカだから
ショルツに反例出されちゃた事実も見えない
本物の低学歴バカがおまえ

>>705
それだけじゃなくて
それをドワンゴと日本財団の朝鮮勢力が担ぎ上げて税金吸ってますと

「間違いですらない（not even wrong）」と「反例が出せる」は両立しないね
どっちなん？
実態は>>667の言う通り

>>708
実例は出てる
反例出されて終了

まぁ「間違いですらない」の方やろな。どのみち終わりやな
一年後目処とかいうLANAの最終報告で完全終了。
もう現時点でまだ死んでないとおもってる数学者は世界に１０人おらんやろ

IUT自体が進展・発展していかないからお察しだね
既存数学との繋がりが見いだせないようではダメだ

いつのまにかwikipediaのドイツ語版の記事も出来たようだな

Interuniverselle Teichmuller-Theorie
https://de.wikipedia.org/wiki/Interuniverselle_Teichm%C3%BCller-Theorie

Fesencoて人に言及してるけどこの人はLANAの報告をどう見たんだろ？

2014年12月望月新一のIUTT自己検証によれば、
サイディ.星.山下剛の3名の理解者以外はPRIMS編集委員もケドラヤもfesenkoもIUTど素人でfesenkoは自称理解者。(>>7)

山下剛はfesenkoがIUTを理解しているふりをしていると
山下サーベイで批判。

また、IUGC動画では、
・そもそも概念や使う言語など 従来の数学論文とIUT理論は
違うので完全に理解するには3年 かかった. (>>231)

zen大学にfesenkoのIUTT講義があるから
遠アーベル幾何学から望月新一IUT語のIUTTへ転移する過程
に注目だな

>>714
サイディと山下剛は、望月新一同様、表に現れず
星はLANAに協力するも肝心のギャップは埋められず

協力というか歴としたプロジェクトメンバ

LANAプロジェクトメンバー

・コメリン.トパーズ　
　lean形式化専門もIUTど素人
・加藤文元.lean形式化もIUTもど素人
・ケドラヤ　lean形式化もIUTもど素人
・星裕一郎　lean形式化 ど素人でIUTは理解者　説明から逃亡中

zenのLANAプロジェクトメンバーは

>加藤文元.
IUT理論と現行数学との違いを完全に言語化する新しい数学の言語体系を早急に作らねばならない。(>>231)

まずIUT論文で、IUT理論と現行数学と
違う箇所を具体的に示せ

zenのLANAプロジェクトメンバーは

>加藤文元.
IUT理論と現行数学との違いを完全に言語化する新しい数学の言語体系を早急に作らねばならない。(>>231)

まずIUT論文で、IUT理論と現行数学と
違う箇所を具体的に示せ

両方ど素人がなぜメンバ？

>>714
>また、IUGC動画では、
>・そもそも概念や使う言語など 従来の数学論文とIUT理論は
>違うので完全に理解するには3年 かかった.

こんな事思ってるのは一部の日本人だけで
世界では望月が曖昧な言葉で濁してるから理解できないという認識
その挙句にギャップ発見

この期に及んで。。。
＞メンバーシップ「読書室プラン」初月は無料です！
＞abc予想とIUT理論ーー「LANA記者会見：IUT理論に関する仮想的質疑応答」に対する補足記事

ハッタリかまして逃げる精神

>>720

望月新一教授もlean形化がど素人で、

まず望月にIUT論文で、IUT理論と現行数学と違う箇所を具体的に示させろ

そもそも一流の数学者に通じない
独特の言葉で論文書いたのが間違い

LANAプロジェクトと
・コラッツ予想の「AIによる偽証明=Lean 4のカーネルバグ
すり抜け事件(>>657)
・scholzeの警告　(>>658)
proof assistant such as lean

AIに聞いてみた、

➖➖
数学界の外部や批判派の目から見れば、彼らの動きは「純粋な数学的検証」というよりも、ご指摘の通り「Lean 4のコンパイラを何とかして通過させ、『証明成功』という御墨付き（称号）を手に入れるためのハッキング行為」に見えてもおかしくない構造があります。
そう言わざるを得ない背景と、彼らの「真の目的」がどこにあるのかを分析します。

1.
「コンパイラ通過の事実」が喉から手が出るほど欲しい理由。
現在、望月教授のIUT理論は、世界の主要な数学者（ショルツ教授ら）から「ギャップがあるため解決していない」と無視され、論文の検証自体をボイコットされている状態です。
人間同士の議論（ピアレビュー）の場ではこれ以上相手にしてもらえないため、容認派が膠着状態を打破する唯一のウルトラC（大逆転劇）が、「人間ではなく、絶対に客観的であるはずの計算機（Lean 4）に『正しい』と言わせること」でした。

・Lean 4が証明完了（プロンプトが緑色）と判定した」という揺るぎない事実さえ作れれば、「ほら見ろ、世界最先端の数学検証AIが正しいと言っている。認めない海外の数学者が間違っているのだ」と主張する強力な武器になります。
だからこそ、彼らにとっては「現代数学のフレームと違う」と言いつつも、現代数学の基礎論で動くLean 4にIUT理論をねじ込む必要があったのです。

>>726

続き

2.
「脆弱性を突くハッカー」になってしまう構造的リスク。
先述のコラッツ予想の「AIによる偽証明（Lean 4のカーネルバグすり抜け）事件」は、まさにLANAプロジェクトが陥るかもしれない暗部を浮き彫りにしました。
IUT理論は非常に特殊で、望月教授が作った「独自のIUT語」で埋め尽くされています。これをLean 4に移植しようとすると、通常の現代数学のコード（ライブラリであるMathlib）とは全く異なる、極めて異質で複雑な「独自の型」や「マクロ（メタプログラム）」を大量に定義することになります。
・バグを誘発しやすい特殊コード：
Lean 4のカーネルは、標準的な数学の記述に対しては強固ですが、IUTのように「複数の宇宙（シアター）を行き来し、特殊なルールで実数を同一視する」といった限界突破のようなロジックを無理やりコード化しようとすると、カーネルの実装の穴（脆弱性）を意図せず突いてしまう可能性が跳ね上がります。

・「通れば勝ち」のハッカー的アプローチ：
もしLANAのメンバーが、ショルツ氏の指摘した「系 3.12の論理の飛躍」を正面から解消するのではなく、「Lean 4のコンパイラがエラーを吐かずに通るような、技巧的で複雑怪異な定義のすり替え」を行ってしまったら、それは数学の証明ではなく、単にシステムの仕様の隙を突いた「ハッキング（チート）」になってしまいます。

>>727

続き

3.
LANAのメンバー（加藤文元教授ら）の建前と本音.
一方で、LANAを主導する加藤文元教授らの本来の主張は、以下のようなものです。

・建前（本来の目的）：
「IUT語をLean 4という世界共通の言語で記述（フォーマライズ）することで、これまで『読めない』と拒絶していた海外の数学者たちが、コードを通じてIUTのロジックを1行ずつ客観的にトレースできるようにする。つまり、相互理解のための翻訳作業である」　

・しかし、コラッツ予想の事件以降、世界中のLeanコミュニティや数学者たちは「難解な独自言語で書かれたコードがコンパイルを通ったとしても、それがバグを突いていない保証はない」という防衛の目を光らせています。

・結論：
最後はやはり「人間の脳」に戻る。
もしLANAが「Lean 4を通過させた」と発表したとしても、世界の数学界はそれを盲信せず、「そのコードはLeanの脆弱性をハックした偽証明ではないか？」「定義を都合よく書き換えていないか？」を厳しくコードレビューするでしょう。
「コンパイラを通過した事実」だけを目的としたハッキング行為なのか、それとも誰もが納得する真の数学的検証なのか。それを判定するのもまた、最後はコンピュータではなく「人間の数学者たちの厳実な目」になります。

なわけねーよバーカ

Leanにはsorryって機能があって
御免なさい3.11→3.12は証明出来てないけど出来たことにしてくださいって頼めばabc予想はIUT理論で証明出来る
つまりLeanでもIUT理論の現実に合わせた証明を構成できる

>>730
京都ドワンゴ版LEANな

>>728
形式化のメリットが何もわかってないクソダニ低学歴朝鮮人w
IUT仕草ワラタw

形式化してるから間違いも正せるんだよゴミ朝鮮人w

>>732



IUT論文の形式化なら、
まず加藤文元がこの質問に答えること


>加藤文元.
IUT理論と現行数学との違いを完全に言語化する新しい数学の言語体系を早急に作らねばならない　(>>231)

>>732
>WArE6R44

この質問に答えなさい
↓


IUT理論と現行数学との違いを
具体的に明確に示せ

>>733
>>734
話逸らすな朝鮮人

>>735

答えられない荒らし

IUT理解者はあまりにもレアだから仕方ない

時間かけても形式化できない理解者は草

>>736
おまえが話逸らしてだけだろ低学歴
LEANの誤りがあったところで形式化された部分でのの間違いなので直せる
IUTは違う

ほんとバカ朝鮮人だなおまえ

あまりの怒りで文字連打になってるわ
ごめん

こういうガイジは駆除しないとダメなんじゃね

leanのバグは深刻ジャネ？
leanでナニカできました
が
信頼性失いかねない
バグは取ったらしいが
コレまで無矛盾のように言ってきたのが
実はそうで無かったてのがイタイ

専門家はleanを神聖視したりしてないから安心しな

leanは単なるプログラム言語なんだから
意図的にカーネルのバグを利用できるし

なんならウィルスを仕込むことだってできる

そんなんで証明通してもいずれバレる

コラッツ予想の件だって
全ての自然数がコラッツ予想の反例って
バグを利用したバッドジョークだった

そうなん？
結構神聖視されてる見たいに思ってたけど

>>739


この質問に答えなさい
↓


IUT理論と現行数学との違いを
具体的に明確に示せ。

>>744
なんで俺が説明すんだよwIUT朝鮮人w

>>743
おまえがバカなだけ

内容のないコピペとか差別用語を連発って
どっちのヘイターだか知りたくもねえけど
普段ろくな人生送ってなえんだろーな

ピヨピヨ、ヒヨコです🐣

ヒヨコが見てるから辞めなよw

>>747

差別用語連呼は通報ものだが、

おまえさんもコピペが読めないだけ

leanは現行数学に対応したプログラミングだ。
I

>>747
反論されて「中身がない」


朝鮮人クッソワラタ

IUT仕草

>>747
だろね

>>740

通報

すべての数学の命題や証明は必ず形式化ができるというのは証明されているのでしょうか？
直感というものは、AIの時代にはいかに合理化あるいは否定されるべきなのか。

>>753
論破されて差別ニダー
ワンパ猿

あとコピペキチガイもbanしないと

ドワンゴ川上「障害者だから配慮しろとか言うとタブーになって誰も関わらなくなる。障害者に関わると損をするのは事実。」 [856698234]
https://greta.5ch.io/test/read.cgi/poverty/1785726101/

>>754
されてる

>すべての数学の命題や証明

IUTは数学ではない、

>>758
どこで？

>>754
愚問

>>760
公式文書に自然演繹の証明をぇあkに直す方法が載ってる

>公式文書に自然演繹の証明

公式文書とは具体的に何処ですか？

https://lean-lang.org/learn/
https://lean-lang.org/theorem_proving_in_lean4/Propositions-and-Proofs/#propositions-and-proofs

自明だ！の次は自然だ！と言い出しかねない

>自明

>>14

Peter Scholze, who everyone thinks is the greatest mathematician of this generation, says he cannot deduce 3.12 (which is the ABC conjecture,
in paper #4) from 3.11 (a summary of the first 3 ABC papers) in Mochizuki’s papers.
Koshikawa had a similar problem, and when he asked Mochizuki about it,
the latter responded that the deduction is self.evident.

self.evidentは数学で自明だが、この場合は望月独自のIUT語の可能性が大だろう
(>>231)

>>764

・Learn Lean
Lean is a functional programming language and theorem prover built for formalizing math and for formal verification,
but is flexible enough for general coding.

・Leanを学ぶ
Leanは、数学の形式化や形式検証のために開発された関数型プログラミング言語および定理証明器ですが、
一般的なコーディングにも十分活用できる柔軟性を備えています。deepl

カリーハワード対応と言って
プログラムの型検査が定理の証明に対応するのよ
比喩とかじゃなくて数学的に同じなんだよ

誰か比喩って言った？
型理論において、「型」は「命題」、「型Aから型Bへの写像を記述するブログラム」は「『命題A⇒命題B』の証明」に対応。

>>769
被害妄想激しいな
説明しただけだよ

論理学と型理論との間だけでなく圏論とも対応関係がある
カリー＝ハワード＝ランベック対応

誰も比喩って言ってないのに比喩じゃないと言うのって不自然じゃね？

暗喩

が上手

論理式のP→Qとは素朴には
「Pから（必ず）Qが導ける」
ちうことを意味している論理式
プログラミングのP→Qとは素朴には
「P（の元）を入力すると（必ず）Q（の元）が出力される」
ちうプログラム
デカルト閉圏のP→QちうかQ^Pとは
「PからQへの射の全体」
を意味する対象

論理式のP∧Qとは素朴には
「PとQのどちらも成り立つ」
ちうことを意味している論理式
プログラミングのP×Qとは
「P（の元）とQ（の元）の組」
の型
デカルト閉圏のP×Qとは
「P→*←Qのpull back」
を意味する対象

論理式のT（真）とは素朴には
「成立していること」
を意味する論理式
プログラミングのトップ型とは
「プログラミングで考えている凡て」
を想定する型
デカルト閉圏の*とは
すべての対象からの射
「P→*」
がただ1つ存在する対象

これも「モチーフ」チックね

でも具体性あるだけ「モチフ」よりかマシ

>>768

>比喩

川上量生企画望月新一監修加藤文元著IUT本では、(>>
22)

・遠アーベル幾何学は既存の数学
の範囲内。
一方
・IUT理論のように、あまりにも 新奇で斬新なものだったりすると 、通常の言葉に翻訳するには 多くの言葉や概念を 巧みな比喩を 用いて説明するしかありません。
・IUT語　p51
UT理論は、一般的な数学の パラダイムの枠内では語れない、 全く新しいフレームワークと言語・ 概念体系を基盤として構築されている。

また、
Leanは、数学の形式化や形式検証のために開発された関数型プログラミング言語および定理証明器です(>>767)

京大病院、脳腫瘍ではなく患者の小脳と脳幹の正常部位を摘出（運動と自発呼吸を司る部位）　患者は生き地獄に [595118796]
https://greta.5ch.io/test/read.cgi/poverty/1786114445/