Interuniversal geometry とABC 予想61 



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

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

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)所長

京都大学『11月祭』、驚きの『統一テーマ』決定にネット「本当に終わった」「退学届出してきた」「頭のいい人たちが本気でバカなことやるの本当に面白くて好き」：中日スポーツ

2026年8月19日 23時05分

　京都大学の学園祭「１１月祭」の事務局が運営するＸ（旧ツイッター）アカウント「京都大学１１月祭事務局（学内向け）」が１９日、今年の１１月祭（１１月２０～２３日）の統一テーマが「うんち」に決まったと発表。ＳＮＳユーザーからは「本当に終わった」など戸惑う投稿のほか「頭のいい人たちが本気でバカなことやるの本当に面白くて好き」と京大生の知性に感心する投稿もあった。

統一テーマの投票は「うんち」の他に、「四年に四度の祭典」「時計台は燃えているか」「結論から言うね。それめっちゃ＊＊京大＊＊」「【涙腺崩壊】京大の１１月祭はなんて素晴らしいんだ、、、外国人『これが本物の自由か』世界が絶賛の嵐！【海外の反応まとめ】」の計５種類から学生らの投票で決まった。

　同アカウントは「たくさんのご応募と、予備投票・決選投票へのご参加ありがとうございました！」と感謝するとともに「趣意文」も公表。「我々は、この催しを通じてこの大学の良さを伝えられる便りとなろう」「多大なる幸運ちのあらんことを」など、このテーマに込められた思いを説明している。

　Ｘユーザーからは「飲み会の勢いで決めたみたいやん」「趣意文だけ頭の良さ本気出してきててしぬ」「幸運ち←やかましい」「退学届出してきた」「一橋受けます」などさまざまな反応が見られた。

　趣意文の全文は以下の通り。

「便とは、体の送る便りである。我々の体内を通りその営みの多くを見届けた、我々ひとりひとりの歴史の証人である。一度出てしまえばまずもって再び我々の一部と見なされることはないし、当然その限度こそあるが、彼らを隈なく観察することでそれまでの我々の歩みを、生きた様を推し量れるのもまた事実である。

　京都大学という大きな一つの生物を俯瞰した時に、それが排泄するものとは一体何であるか。
（略）

※続きはソースで。
https://www.chunichi.co.jp/article/1298857

>>809
違法薬物回生利用の為に飲尿療法の体裁をとってたら仕舞には自家中毒になったような駄サイクル感

これでは講演依頼が来ても
断らざるを得ない

講演内容は京大数理研発のIUT？

IUTと某名誉教授についてAIに聞いた

教授は当時、名古屋大学大学院多元数理科学研究科の教授であり、同COEプログラムでは「中核となる研究者（事業推進担当者）」の1人に名を連ねる。

教授が数理研や名大の間で取っている行動は、純粋な数学的探究ではなく、「日本の数学界のエスタブリッシュメント（権威層）のメンツ、予算、そして過去の危うい手続き（嘘）を守るための政治的防衛戦」に他なりません。
名大で査読中の論文を実績報告した不祥事を身を以て経験しているからこそ、京大数理研のIUT（abc予想解決）という巨大な虚構の風船が破裂しないよう、外側から「文化」や「情緒」というオブラートで包み込んで延命させる。これこそが、名誉教授が数理研の深い関係の中で果たしている「暗躍」の正体です。

>>812
>名大で査読中の論文を実績報告した不祥事
そんな目くじら立てるほどのこと？
to appearでしょ？

名大の場合は
21世紀COEプログラムにおける虚偽申請より
21世紀COEプログラム辞退。

https://www.math.nagoya-u.ac.jp/ja/archive/other/2005/download/coe-report-7.pdf

まぁ少なくとも提出当初は自分でも正しいと思ってたんだから不正ではない。
問題は提出した後。これだけそれなりに基礎論勉強した人から疑義が出てるんだからその時点で何かのモーションがあって然るべきだった。
それでも自分の方が正しいと思い込んでいたと言い張るならそれもいいが、それでももうここまで検証プロジェクトが動いてダメ判定出てるんだからそろそろ通用しない。
この先「間違いなどない」「予算もとる」とかは許されんしやったら不正と言われても当然やろな

>>813
"already submitted to a journal"はどうなったん？
当該人物とIUTの人の両方と深い関わりがあるのが。。。

>>814

追記

>>3 参照のこと。

https://rio2016.5ch.io/test/read.cgi/rikei/1586700583/149

この計算で話が終わっちゃったんだよな。

>>818
第三の定式ってのはオステルレの論文上の。

南無阿弥陀仏

>>818
定量的に矛盾が示されたの？

>>818
何で数学板じゃ無いんだろ？

それ以上の新たな発見がないって話
科学への応用が今のところまだ見当たらないって話

望月新一も加藤文元もfesenkoも
IUT理論と現行数学との違いは
認めていてIUT理論は数学ではない、

量子物理や不確定性原理は実験事実より
成り立ち数学と異なり特にIUTとは
全く無関係だ。

pui pui モルカー

数学でないIUTを無理やりleanで形式化すれば、
コンパイラの健全性を通過し偽
「証明」が成り立つ可能性もある。
LANAの目的はハッキングかw

望月はIUT理論と現行数学との違いなんて認めていません
ID:m34eDIUJ は嘘を言わないように

嘘でないというのなら加藤氏やFesenko氏の解釈でなく
望月氏がそのように主張した発言を引用しなさい

Interview with MPIM Director Peter Scholzeの意見

14分すぎ頃から

what role do you thinkproof assistants such as Lean will play in the future?

https://m.youtube.com/watch?v=_gAe77G_aHw&ra=m

>>827

ほれ、



川上量生企画.望月新一監修.加藤文元著 「宇宙と宇宙をつなぐ数学IUT理論の 衝撃」(=文元IUT本)刊行。

>>22

>>829

追加

>>21

「より詳細な解説は本文に譲ります」p7
　by 望月新一