【数学】ABC予想、証明に暗雲？　国際チーム検証中、望月氏と議論へ [すらいむ★]

数学・ABC予想、証明に暗雲？　国際チーム検証中、望月氏と議論へ

　数学の超難問「ABC予想」の証明について、ZEN大学などの国際研究チームが31日、「1年半前から証明の検証を進めていた」と発表した。
　検証は途中だが、京都大の望月新一教授（57）の証明には「現時点で解明できていないポイントがある」「ギャップ（論理的な飛躍）の可能性もある」として、望月氏らと議論を続けているという。

（以下略、続きはソースでご確認ください）

朝日新聞　3/31(火) 13:00
https://news.yahoo.co.jp/articles/7305051a1b2b85772362b2d0ca5de447430d71e1

ショルツからの批判に皮肉で返した時点で望月新一の信用は地に落ちた

10進法だと(10+1)/2=11/2で訳分からんくなるから
5進法で考えればいいような気がする
(5+1)=6（5進法表記で10）

https://www.youtube.com/watch?v=hRJRaIP6VGk
こんな感じで

>>46
AIは形式証明に使われてるし
数学上の幾つかの未解決問題解いてるよ

生成AIが答えてる訳じゃないけどね

オレオレ数学使い出すしかないかもな
まあ最初だからだけどw

オレオレ数学使い出すしかないかもな
まあ最初からだけどなw

いやいやもう反例挙げてる論文出てるから
もうとっくに否定済みだよバカども

フィールズ賞受賞者で
望月が論文をちゃんと権威あるところへ提出したらレフェリーやるようなクラスの数学者が
もうとっくに否定論文出してる
何引き分けみたいにしてんだか
チョンかよ

>>54
ドワンゴ麻生っつったらもうあれよwww

明々後日に本人が話すじゃん
https://aitpm.github.io/
April 9th 2026
Shinichi Mochizuki: On the Formalization of IUT: a preliminary progress report
In this talk, we survey preliminary work conducted by my research group at RIMS, Kyoto University, since the fall of 2025 on the long-term project of formalizing IUT (inter-universal Teichmüller theory).
略
Finally, we discuss in detail, as a sort of case study, the reorganization into suitable blackboxes, from a Lean formalization-oriented point of view, of the logic of the final portion “3.11⇒3.12” of the third paper on IUT, since it is this portion of IUT that has received the most public attention. The skeletal Lean code that we wrote for this portion of IUT constituted a remarkably successful case of the use of Lean as a communication tool.

LEANがZFCのクソなので改造します的なこと言い出したら爆笑する

だいたいショルツに批判されて８年間、この人も何とか改良できなかったのかな
フェルマー定理は発表時に指摘された欠陥を修正できたのに

仮に3.12スルーしたところでまだ先は見てもらってもいない状態なんだよなこれ

後ろ盾が消えてケツに火がついたか

大英笹川財団議長 ロバート・マクスウェル

こういう時こそ得意の宇宙際タイヒミュラー理論だろ
3.11系から3.12系が成立する宇宙に持って行ってそこで証明してその結果をこの宇宙に持ってくればいい

>>59
なことはない

>>57
実際一階述語論理に基づいたZFCがLeanライブラリにないのでうまく証明が構成できないということは1年前から言ってる
ただそういう問題でもなさそうだとも分かってきたから今回の弱気な発言とショルツェ側の新メンバー招集なんだと思う

わからないこと

>>62
ワラタ
お前らのオレオレ査読の話してねーんだけど

>>65
いやSSも系3.12の導出しか問題にしてない

>>66
前提だからなw
他見てるわけじゃないw

ABCも知らないような高校生にも判るような易しい証明をお願いします。

XみたらもうIUTTとmathjinくらいしかいなくて
どっちもキチガイ扱いされてんの笑う

>>32
朝日の記事はずっと追ってる記者が書いていて数学科出身らしい
望月に肩入れしてるようなので混乱してるのではないか

>>70
あいつずっとIUT擁護の偏向記事出してるからなw
まー明日とアエラの科学記事はゴミだよ
ひやっしー持ち上げてたし

ABCも知らないような高校生にも判るような易しい証明（？）
かは、分からりませんが…というか証明ですらありまんが

16進法の0xABC=2748=(28-1)*10^2+24*2
Python記述:0xABC=2748=(24+6-6/2)*10**2+24*2

注釈:(24+4-1)→24+6（6は10進数と16進数分の差）に更に-6/2
今回はN=16進法で考えてみた…

信じるか否かはアナタ次第！！（たっ、多分。合っている筈…？？？）

論文載せた身内誌の編集委員7人のうち分かると言うのは1人だった。
新しい理論出すのは自由だが従来理論との違いは説明いりそう。望月はまず批判者は理解してないと切り捨てその後わが理論を数年学びに来いと吹いた。
信者20人対数学界でも少数が正しいことはありうるがもはや理論や理解でなく信仰するかしないかになってるようにみえる。

ブラックボックスおじさん

>>56
イングランドの大学らしいから
日本時間の今日中には終わるな
日本時間の0時が向こうの15時だから

>>56
skeletalってどういう意味で使ってるのかな
まだ出来てないけど俺の理論を形式化するために凄いライブラリを開発できそうだぜ
ってことなんですかね

>>56
https://www.kurims.kyoto-u.ac.jp/~motizuki/Formalization%20of%20IUT%20(2026-04).pdf

https://plaza.rakuten.co.jp/shinichi0329/diary/202601010001/ とほぼ同じかね

>>63
MathLibに登録されてないだけで見つかってるんだって
ただどうモデル化してるかによって
IUTで使いやすいかどうか違うからなあ
数学屋さんにはこの辺は理解しにくいだろうけど
理論は理論だろって思っているだろうから
極めてプログラミング的なゲーデルの第二不完全性定理の面倒臭さ考えれば自明なんだけど

>>77
学会で発表したPDFの方は流石にRCSとは書いてないのね

>>77
差別的とかどの口が言ってんだよ半ユダって感じだなw

>>32
この日経の記事で

>数学の超難問の「ABC予想」に関連する「宇宙際タイヒミューラー（IUT）理論」や「遠アーベル幾何学」の主要な定理をプログラミング言語の「Lean」で記述できるようにする。超難問の証明過程をLeanで正確に記述できれば、証明の真偽を確かめられる。

とあるのだけどこれは誤解
・上手く形式化できて証明出来る
・上手く形式化できない
・形式化が下手なのか
・証明に問題があるから形式化が不可能なのか
の後者は簡単に決着付かない
証明できる人間がまだ出てない問題は偽であると言えないのと同じ
その過程で何処に問題があるのかははっきりしてくる
しかしそれがSS論文の結論に近いというのが現在の状況

>>77
この内容じゃあ反応ないはずだわな
7月まで無風かな
あるいは外部の人も参加してるから少しずつ漏れてくるかな

全てが発覚した後
「日本のおお数学界を救うためにいい仕方なくううう」
とか言いそうだよなw

ああ…
>>77で形式的証明を与えることが重要なんではなく
これまでも主張しているように
数学的常識を疑う思考ができない人がIUTを理解できないのだから
その障壁を取り除くのにLeanはコミュニケーションツールとして有益という謎の主張をしてるのは
>>32
単に形式的証明を与えるだけだとショルツェの二番煎じになっちゃうからか
対抗意識が強いんだね

この発表聞いた人は頭抱えただろうな
数学の発表じゃないし
形式的証明与えたらもうコミュニケーションする必要もないんだが
一方的に宣言すればいい
勝利したと

>>84
しかもさ
指摘されてる内容が3.12と同じなのに
3.12は合ってる！3.11がおかしい！とか言ってんには
ショルツのアドバイスを受け入れたくないからだよね

ゴミを他の場所に移動しただけ
ほんとマジカス

コミュニケーションしたんですうう
完

IUT関係者「Lean4は忖度がないから困る」

ブラックボックスにされちゃったLEANくんの行く末
京都版LEAN改造人間にされてしまったりして

>>63
> 一階述語論理に基づいたZFCがLeanライブラリにないのでうまく証明が構成できないということは1年前から言ってる

>>77
>species/mutationの理論において本質的な役割を果たす「不定元のような論理式」（＝特定されていない、「とある論理式Φ」のようなもの）を扱うには、一階述語理論としてのZFCが必要であり

論理式が特定されてないなら必要なのは二階なのでは？
二階述語論理も必ずあると思いますが
ゲーデルの第二不完全性定理で必要なので
違うの？

ちなみに人間が扱うときは面倒なんで
公理の数を無限個にして一階のままやるパターンがあります
全ての論理式ごとに公理を無限個付け加えれば二階にする必要はないので
こういう無限個の公理を扱うプログラムがCoqやLeanにあるのかどうかは知りません

>>89
>論理式が特定されてないなら必要なのは二階なのでは？

だよな、このレベルで間違えるとか、信じ難いけど

キリスト教・ユダヤ教に基く欧米の神格化・選民思想と理性の弾圧
https://plaza.rakuten.co.jp/shinichi0329/diary/202401020000/
新一さんって大丈夫なの？

>>6
いやならない
論理的にギャップがあるから
それを認めると無根拠に色々と証明できてしまう
系3.12を証明に使うということは
証明にギャップを持ち込むのと同じことだから
だからグループの人が色々と証明出来てる
ちょっと工夫して系3.12を上手くはめ込むだけ

>>91
麻生太郎とかもなw

望月氏って苗字（姓）に月が二つ付いてるじゃん
論理和の一種「XOR」を翻訳したら差別的だと誤解されて論文を読んでもらえない説
んで、望月氏は月が二つっぽいので強く印象に残っていたのでは？

>>94
XORが使われている論文が読まれない説と、望月の名前に月が二つある話に、ギャップがあるぞ

LEAN自身の正しさはどう証明するの。それがC言語で書かれていたら、
そのプログラムの正しさをどうやって証明するのかな。
かりにC言語で書かれたプログラムが正しくても、それをコンパイル
して生成された機械語プログラムが正しいものになるためには、
コンパイラの正しさと、機械語をCPUや計算機のハードとOSが
正しく実行することが必要。I社のCPUはエラッタが多いぞ。
コンパイラも頻繁にバージョンアップがあるということは
バグも多いだろうし、バージョンが上がればバグが減ること
は保証されない。OSもWindowsなどバグだらけだろう。
Linuxだってカーネルやライブラリやデバイスドライバも
含めてバグはある。また長時間計算すると、電気ノイズや
宇宙線などの影響により正しく計算できる確率は時間と
ともに指数関数的に減少する。ECCも無いようなメモリを
使っている安物のPCによる計算結果は信用するに値しない。

>>96
あーあクッソ頭悪い低学歴が無限後退し始めたw





だせえww
IUT擁護のゴミマジだせええw

っていうか川上とかその辺りのレベルかもなw

このグループの人達の論文読むと
数学なのに例え話がよく出てくるよね
予備校の授業みたいに

ブラウアーの数学的直感は
全て排中律としてまとめる事が可能なことが分かった
みたいな事例もあるから
数学的直感は重要だけども

証明が可能になるようにLEANにパッチを当てればいいだけ。
信じるものは救われる。

パッチなんか当てる必要はなく系3.12を公理として加えればいい
RIMSでも公理として扱ってる

IUT派が心を入れ替えて誠実になるってことありうるんだろうか
もはやこの話に集約される

>>35
エスプタインは別にどうでもいいよ。

>>103
ドワンゴ
界隈にかなり近いぞ

>>6
加藤さんが解明できないんだったら、誰にもわからないぞおい

この世の中にたった一人の人間がいてあとはチンパンジーだけだったとするとき、
その人間が導いた証明はあとのチンパンジーには努力してもチンプンカンプンで、
決して理解されることはない。それよりもバナナが欲しいだろうし。

人間より圧倒的に頭のいいチンパンジーがいる状態
ただやっぱりチンパンジーは以下略

>>106
ゲラゲラ
ほんとIUT派はクソ頭悪い比喩多いよなあ



朝鮮人ww

>>105
ギャップがあると解明させてるけど
望月さんに強く言えない状態なのでは

偽右翼
顔面見たら
朝鮮人

望月新一の論文はもう具体的に反例が構成されて提出済み
議論なんかされてない
もう結論は出てる
否定済み

反例の論文が提出されて査読中ということ？
wktkして待ってる

ペーター・ショルツェは望月新一の理論には主要な定理に反例があり誤って居ることをすでに証明済み。当然査読済みの論文が出されている。
またアクシェイ・ヴェンカテシュも望月新一の論文は証明に飛躍があり、証明になってないとする見解を出している。
どちらもフィールズ賞受賞者であり、望月新一などより遥かに格上の数学者で、
望月新一が内々で勝手に証明したことにするインチキをやらずちゃんと世界的に名の知られた数学雜誌に論文を提出すればレフェリーをやるような数学者だ。
ウソつきがインチキをやって引き分けみたいに工作しているだけ。
望月新一の理論はすでに否定済み。



.

日本の京大関係者が必死になっているけど、世界は間違いで放置決定の話でしょ。

>>113
査読済みっての間違いだったな。
具体的な反例の提示だから、こういう議論は現物を指し示すだけで十分なので
普通は反例の提出だけで十分とされて、わざわざ論文を書いたりはしないものらしい。

望月氏の今までの論文は大丈夫なの？

>>116
否定済み。
少なくとも望月新一より遥かに格上のフィールズ賞受賞者の数学者が最低二人否定している。
レフェリーやるような数学者ね。

これがマズいのは
韓国がやりそうなことをよりによって京大がやらかしてるってことなのよね
日本はもうここまで劣化しちゃってるってゆうことを示す端的なデータ

Hard times create strong men,
strong men create good times,
good times create weak men, ←日本は今ココ
and weak men create hard times.←これからの日本
G. Michael Hopf

あと確かテレンス・タオも望月新一の論文は否定していたはず。この人もフィールズ賞受賞者。

昔、韓国人が悪さやって裁判になって
法廷に出たくないもんだから自分の体にうんこ塗りたくって抵抗したとかね
ああいう恥ずかしことをよりによって京大がやらかしてると言うね

CHATGPTに聞いてみよう。

誤ってることが証明済みなら何で今更Leanで検証なんて話になってるの？よくわからんな

やっぱ凡人が考える天才の真似
天才のハッタリって言ったら
形から入るよなあ
コジキのコスプレとか

>>123
IUTグループ自分らは誤りを認めてないんだよ
3.11から3.12のギャップの一部分だけ見て
他をブラックボックスにしときゃ
全体は間違ってても局所的に(とは言っても嘘になるが)正しいと言えるかもしれないからなあ

これさあ
みんな黙ってるけど
「IUTで他のやり方」したら別の不等式出てきちゃうだろw

>>123
ウソつき負け猿だからじゃ無いの？

.


Hard times create strong men,


strong men create good times,


good times create weak men, ←日本は今ココ


and weak men create hard times.←これからの日本


G. Michael Hopf


.

負けが確定したら
引き分けみたいに工作しだすのはチョンの常套手段
日本は最早チョンクオリティ

p進数とかN進法とか
分かりずらいから麻雀パイの絵文字を用いれば良いかも

>>125
加藤は認めてるに等しいという報道なんでは？

>>39
星のIUT入門論文読んだけど
理解するのはなかなか難しかった
用語が独自すぎるのと
うまく整理されてるようには思えなかった事で
それから「これは大雑把に言うと～するということである」が多すぎ

>>131
バカチョンアスペルガーか
なんでLEANに手を出したかその経緯の話だろ
ゴミかお前の脳は

エッシャー階段へのチート策は
視野を狭めて局所だけ正しいとか言っときゃいいだけだからな

AIに聞いてみただけだから確実ではなく個人的な予想に過ぎないけれど
LEANには排他的論理和に関す表す機能？が無いらしくMathLibに載っていないらしい
排他的論理和はc言語やPythonはハット記号「^」だけれども
Basicやネット上では乗数で用いられているので実装が難しいと予想
ＷHat？状態な予感

>>135
なわけない

>>136
失礼、表現の仕方が悪かった
ご指摘の通り、LEANは確かに排他的論理和を表せるのだけれども
https://www.youtube.com/watch?v=H4n1XIa2flI
を視聴したのだけれども
集合記号と¬の組み合わせで混乱して読めない…的なことを言いたかったんよ

数学者は数学的記号の統一的表記を決める気はなく
分野によって使い方が違うので
証明系では証明系研究者たちが自分たちで決め打ち的にやるしかない
適用分野ごとに使う記号を差し替えるライブラリを作れる証明系もあるが保守性が低くなる割にメリットはほとんどない

集合論の人は含意を⊃で表すのを好むが
計算論の人たちはそうではない
困った事にこの二つの分野はゲーテルの予言通りかなり接近してきている

多分こんな感じ？
Φ(ζ(-1))∈{2π,2π+(π/6)i}

笹川朝鮮財団の方から来た偽学者w

AIでええんとちゃう？

a+b=c、gcd(a,b)=1 のとき

素因数の積 rad(abc) は
→ cに対して「異常なスケール差」を作れない

正確には

任意の ε>0 に対して

rad(abc)≫c1/(1+ε)という制約がかかる

スーパーコンピューターで２０００通り試してその割合で大体あってるっていう統計学的な解決案で大体合ってるやろ
試行を止めずに２兆通り、2亥通りとかやれば９９．９９９９…％正しい答えが出るだろ

無限大と比較すれば2亥通りどころかグラハム数通りでさえ無視できる小ささ
99.9999…%じゃダメなんですか？
はい、ダメなんです

LEANの前にリファレンスになるIUTは実在すんの？
なんか昔は何年もかけて誤字脱字数式ミスの改訂繰り返してたけど
もう飽きてんだろ？

あんな状態でLEANの持ち込めるリファレンスがあるわけねーじゃんw
そもそもw

カドカワ金無くなってきたんか？
朝鮮麻生笹川ザマw

京大の研究所は２０２６年度からは紙に印刷された雑誌の製造と配付を辞めるらしい。
世界中からダウンロードされたりミラーリングして保存しておかないと、戦争や大災害
などあれば、学術研究の成果の記録はデジタルデータだけだと風と共に去りぬになって
しまうかもしれない。

これ読んだらもう人間の脳ミソじゃ無理みたいやね
ttps://note.com/cool_chives7783/n/n0b48a6daa3fe