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

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

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

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

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

AIは神ではない

いまさらギャップがあるとか言ってんすかww

へぇ。。
この加藤さんって、望月さん側の人間かと思っていたけれど、そこから疑義が出ちゃうか。
上手く突破できればいいけれどね。

>作業はなお途中だが、加藤氏は「現時点で研究チームが解明できていないポイントがある」と話した。それはIUT理論の根幹を支える定理で、数学的なギャップの可能性もあるとみている。ただ、それが本当にギャップなのか、チームの理解不足なのかについては、まだ判断できないとしている。

証明されないとそれが新たな重要未解決問題になるわけか

>>5
Leanで形式的証明を与えるつもりだったろうにね

別の宇宙作って云々かんぬんだったっけ
相当無理筋な気が……

ABC ABC は～～～ん E気持ち～

AI使って検証するとか言ってなかった？

>>2
記事の国際研究チームがまさにそれ

>>6のポイントと
ショルツェの指摘した系3.12は近いのか遠いのか
弱いABC予想との関係はどうなのか

今は人間だけでなくコンピュータ（AI)も参加して証明が正しいか検証するのね。
理想的な共同ワーク。

京大の望月派が加わっての議論でも解消されず、公式発表となったのだから、証明の見直しが必要な可能性は結構あると思う。

加藤先生やZEN内部から動きが出てきたのは良いことやね

ABC包囲網が形成されたか。１.４億円の賞金欲しさに名うての賞金稼ぎが集結か。

数学者って重要な発見するのだいたい20前後からせいぜい30半ばだからなあ

SFでしょ

もっと分かりやすい論文書いてね。
でいいじゃん。

ギャップがあるってつまり

検証チーム「『 〇ならば△』ってなぜそうなるのか？飛躍してない？」
望月教授「いや自明でしょ」

みたいなことだろうか

zfcじゃねーからなw
zfcuかつ失敗してんのがIUT

>>9
涅槃で待つ

検証チーム「数学におけるフロベニオイドを平手友理奈、外部ガロア作用を秋元康に置き換えてますよね。これは何ですか？そもそもどこの別宇宙です？」
望月教授「自明だろ」

リーマン予想のリーマンゼータ関数の零点が負の偶数と実部が1/2の複素数に限られる
なんでそうなるかというと宇宙がそうなるように演算しているってnoteで読んだ
複素数や虚数が生まれるとタキオン粒子とか存在してはいけないものが創発されるだってさ

数学と将棋は似ているのかな？
若い盛りを過ぎると急に脳力が落ちる

フィールズ賞受賞者に論理の飛躍を指摘されてまともに反論できなかった時点でもう詰みだろ

チョンカスドワンゴはleanのギャップを人力で解いちゃってもいいんすよw

理解者なんだろワラヒw

確かに、「始めました」とか「解き明かしました」ならわかるが
「始めて１年半経ちました」って変な発表だな
そんなんわざわざ発表する意味ある？

主人がオオアリクイになんだろ

理解者誰もいませんでしたってオチ？w

ハッタリかまして抜いてきた税金どうすんの？

オマエラ

>>28
この朝日の記事にはなぜか書いてないんだけど
理解せずに書いているからだろうけど
日経の記事によるとショルツのLeanプロジェクトチームにいた

>ZEN大学やオランダのユトレヒト大学などは31日、コンピューターを使って数学の難問の検証を目指す国際共同研究を始めたと発表した。
>Leanは13年に登場したプログラミング言語で、数学の定理を証明するのに使われている。22年にはLeanを使って現代数学の高度な議論を検証するプロジェクトが完了した。この研究計画の開始を呼びかけたのはショルツ氏だ。
>今回のLANAプロジェクトには、ショルツ氏のプロジェクトで中心的な役割を果たしたユトレヒト大のヨハン・コメリン助教や、カナダのアルバータ大学のアダム・トパーズ准教授が参加する。加藤所長は「世界一のメンバーを集めたと自負している」と意気込む。

も参加するようだ

ショルツのプロジェクトはLiquid Tensor Experimentって奴で
自身の液体ベクトル空間理論の定理9.1の形式的証明
自分でも正しいか自信が持てなかったが形式的に証明した
もう4年近く前の話

特定の立場に偏らずと断ってるのはショルツの仲間が参加しているためだろう
参加者が増えた新プロジェクトの目的そのものだから
加藤文元所長がギャップがあると思っている事に自身が持てなかったから始めた、というところだろうか

>>12
7月に発表だって
中間報告と言っても
加藤文元プロジェクト的には最終発表なのではないか
望月との対話はギャップをどう埋めるかなのではないか

>ZEN大学ZEN数学センター（ZMC）の加藤文元所長らは23年にIUT理論を研究するプロジェクトを立ち上げ、24年から本格的に研究をはじめた。加藤所長は「（IUT理論について）議論に不備の可能性があるポイントは押さえた。望月氏との対話も続けたい」と話す。7月17日に中間報告会を開き、研究成果などを公表する考えだ。

>>33
元所長かよ

同じ国のノーベル賞もエプスタイン汚染されてたなw
アーベル賞柏なんとか大丈夫か？
ドワンゴw

　
ありまぁ〜す

望月氏の証明法への疑義は続くがABC予想自体はおそらく真だというのが大方の見方なのだろうか

>>37
だからそういう微妙な所狙って素人騙してたんでしょ

>>12
まさに系3.12らしい

星裕一郎：京都大学数理解析研究所
>しかし同時に、残念ながら、私はまだ自分の役割を完全には果たせていないとも考えています。特に、先に述べた定理3.11から系3.12を導く論理について、LANAプロジェクトのメンバーの多くが、その中に何か超えられない壁があると感じていること、その事実を私は重く受け止めなければいけません。そして、そのような状況に対して、自分自身の至らなさも強く感じています。
https://zen.ac.jp/zmc/topics/jwz-o8xr3v6f

これLANAプロジェクトで理論の欠陥が明確になったら100万ドル（だっけ？）getじゃん？

>>40
審査プロセス非公開の循環取引かw

あん？うん？という状態になってるのか

というか当時も、そして今も
Scholze–Stixが正しくてギャップがあるということだね
ギャップがあるという指摘に対して答えられてない
https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture.pdf は2018年の事なのに(問題提起は2017年の事で、京大に赴いたが議論を諦めた結果がこの論文だ)
8年間何をしていたのだ
いや望月が直接返事した
https://www.kurims.kyoto-u.ac.jp/~motizuki/Cmt2018-05.pdf
と言うかもしれないが納得はされてない

https://arxiv.org/abs/2210.16488 2022年
https://zbmath.org/1465.14002 2021年
の批判もある

カス論文認めちゃったクソ研究所の柏なんとかサンはどこに逃げてるの？

>>13
AIじゃない
AIなんか馬鹿すぎてこの人達の議論にはついていけない

んでカス川上はなんつってんのw

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

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派が心を入れ替えて誠実になるってことありうるんだろうか
もはやこの話に集約される