Interuniversal geometry とABC 予想61 



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

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

「間違いですらない（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/

ショートスリーパー信者ボコボコにしたら
遠吠えがIUTと同じだったw

https://youtu.be/lWp7QiS3DlI?si=6G6SblPowatbsdTw

abc予想的なものを説明してるのかと思ったらAIに作らせた間違ってる画像をこれは気にしないでくださいとか言ってる死にそうなリハッククオリティ

701 名無しさん＠恐縮です 2026/08/15(土) 13:41:31.61 ID:3cD2kfkc0
「自分が言ってることを信用してない人たちに向けて別に証明するつもりもない」みたいなことをよく言うけど、
まさに超能力者（笑）とかがよく言うセリフだなぁと思って見てる
https://hayabusa9.5ch.io/test/read.cgi/mnewsplus/1786497408/701

2014年12月
IUT論文査読中

IUTTの検証.進捗情報の報告
京大数理解析研究所教授.望月新一
・P5
>ABC予想には本質的に異なる 手法による「別証明」が果たして存在 し得るか、疑問を抱かざるを得ないと いう意味においても「正しい理論」で ある。

・P6
>IUTの場合「絶対遠アーベル幾何」や 「エタール.テ-タ関数の剛性性質」 「Hode.Arakelov理論」といったテーマについて既に深い理解とそれなりの研究業績を有する研究者なら、そのような 「つまみ食い」だけでIUTをかなり 本格的に理解することが可能かもしれませんが、
幸か不幸かは別としてそれらのテーマに精通している研究者は(私自身を除けば)この世に存在しないのが実情です。

・P7
「既にIUTの検証活動に関わっている 数名の研究者(サイディ.山下剛.星)を除けば、世界の 全ての数論幾何の研究者(=連続論文が公開された時点.2012年8月での山下剛氏も含めて)はIUTの周辺にある数学に関しては「全くの素人」であり、
これまでの研究業績の上に成り立っている「深い理解」を活用してIUTの成否に関する決定的な(=数学的に意味がある」)判定を下す資格が本質的にありません。
(>>7)

狂人の香りがぷんぷん

ショルツェだけでなくファルティングス、カレガリ、タオらもIUTに対して非・肯定的なコメントをしている
彼らのような一流でも理解できないのであればそれ以下の凡人には理解できるはずもないので、関わるだけ時間の無駄でしょう

証明というのは的を射たアイデアがあるとスパッと解けるもの
逆に無いと何をどうこねくり回しても解けないもの
IUTには何もアイデアが無いことをショルツェは見抜いていたんだね

相談者が加藤じゃなければもっと早い段階で問題の指摘を受けて、こんなことにはならなかったかもね

日本財団朝鮮人とドワンゴ朝鮮人が税金抜きつつ日本の科学を腐らせようとした方策がIUT

お前らどうすんのおおぉぉぉぉぉォオぉぉぉぉぉぉぉぉおぉおおぉぉぉお(´;ω;`)>IUT関係者

形式化プロジェクト鋭意推進中
と言っとけばしばらくは飯食える

でもLANAなんか中間報告成果０でも相変わらずドアンゴの支援はずっと続いてるようにみえる。
おそらくこのまま何十年たっても成果でなくてもずっと永遠に支援され続けるんじゃないかな？
だったらもうなんもする必要もないと開き直ってるかもね。やってるふりしときゃいいと
なんかできるとも思わないけど

その間ずっと税金抜かれる

ZEN大学の目玉の一つが望月だったとしても
望月が落ちたからZEN大学も骨抜きで消滅とはならん
文科省はその辺クリアしてるかどうか見て設置を許可してる
ZEN数学センターも望月の属人的な組織運営にはなってない

>>796
私大の殆ど全ては私財が投入されて設置されてる

税金は入ってないとgeminiは言っとるな。しらんけど

税金はある程度はいってるの？

ZEN大学の運営や学費に「直接的な税金（国からの補助金）」は投入されていません。
ZEN大学（学校法人日本財団ドワンゴ学園）は、民間企業のドワンゴと、公益財団法人である「日本財団」の民間資金によって設立・運営されている私立の通信制大学です。税金との関わりや、学費が年間38万円と安く抑えられている理由は以下の通りです。

1. 税金（補助金）が入っていない理由通常の私立大学には、国から「私学助成金（経常費補助金）」という税金を原資とした補助金が交付されます。しかし、ZEN大学のような新設の通信制大学には、基本的にこの国からの経常費補助金は交付されません。そのため、運営費のベースに税金は入っていません。

2. なぜ税金なしで学費を安くできるのか？税金の補助がないにもかかわらず、一般的な私立大学（年約93万円）の半額以下である年間38万円という低学費を実現できている理由は、主に2つあります。日本財団による巨額の民間資金援助ボートレースの売上金などを原資に社会貢献活動を行う「日本財団」が全面的なバックアップをしています。税金ではなく、この潤沢な民間資金（財団資金）が投じられているため、設備投資やシステム開発のコストが抑えられています。オンライン特化によるコスト削減大規模な校舎、広大なキャンパス、維持費のかかる施設を持たないため、固定費が圧倒的に安く済みます。

3. 間接的に「国の税金（国の支援）」を使えるケース大学の運営自体に税金は入っていませんが、学生個人が受けるサポートには税金による制度を利用できます。国の「高等教育の修学支援新制度」の対象ZEN大学は文部科学省に認可された正規の大学であるため、国の「給付型奨学金（日本学生支援機構/JASSO）」や「授業料減免制度」の対象校となっています。世帯年収などの要件を満たせば、国からの税金（支援）によって実質的な負担がさらに安くなります。結論として、大学のビジネスモデルや運営基盤は「税金」ではなく「日本財団（民間資金）×ドワンゴのネット技術」で成り立っています。

>>797

>文科省はその辺クリアしてるかどうか見て設置を許可してる

文科省関連の方ですか？　

元々IUTにはIUT論文の査読中に文科省から補助金が出ていたね。
zen大学のIUGCはIUTの第2の拠点を
アピールしていた。
1番目が望月新一教授の京大数理研、

Leanのシステムの正しさはどうやって証明するの？　OSやCPUのバグも心配になる。

Leanが空気を読む賢さを学べば、忖度を覚えてしまうかもしれない。
早く芽を出せ柿の種、出さぬとハサミでちょん切るぞ、といって脅すと
言霊の力により、柿の種から芽が出てすくすくと育ち、柿の実ができて
それをみたサルが、。。。

>>801
LeanはAIじゃないから学ばないでしょ
人が忖度を入れ込むことは有り得る

>>799
私学助成金は憲法違反だっていう人もいるね
文科省の大学支配のための餌・ツールになってるから
廃止するべきと俺も思う

>>799
>日本財団による巨額の民間資金援助
これが凄まじそうだけど
日本財団の顔を建てて
国粋主義的な側面を見せていかねばならんのかもね
日本財団側ではZEN大学はどう位置づけてるんだろ
ボートレースのギャンブル的側面から来る
負の印象を払拭することも目的にしてるのかな？

LeanというはAIではなくプログラム言語の一種で、そのLeanコンパイラ自体は人間が読めるソースコードから作られてる古典的プログラム
つまりNNではないのでシステムにブラックボックスな部分は無い
オープンソースなので世界中の誰でも自分のPCでLeanでの証明プログラムの検証が出来る

>>798
エセ科学と一緒にすんなよw
朝鮮人w

>>805

>Leanでの証明プログラムの検証

証明は数学の定理の検証。

IUT理論は数学と異なる望月新一独特のIUT語による。(>>780)。
一方
Leanは、数学の形式化や形式検証のために開発された関数型プログラミング言語および定理証明器です(>>781)
よってIUT論文はleanの数学形式化の対象外。

zen大学ZMC所長のLANAプロジェクトのリーダー.加藤文元も副所長fesenkoも、

望月新一IUT語によるIUT理論と現行数学との違いを認めている。(>>231)

この違いを「完全に言語化する新しい数学の言語体系を早急に作らねばならない。by 加藤文元IUGC(現ZMC)所長