ABC予想証明の正否、コンピューターで決着か 望月氏が打開策示す：朝日新聞

数学の超難問「ABC予想」をめぐる論争に、決着がつくかもしれない。コンピューターの力を借りて、証明の正否を検証する動きが出てきた。京都大の望月新一教授（56）も、この試みに肯定的だ。証明が正しいかど…

[megumin1]

"形式化の際に「飛躍してる」と言われるだけのような。" <= 形式化手法を理解していないコメントばかり。Leanが「正しい」という結論をだす形式化がひとつでも見つかればそれはABC予想の証明であり数学史上の快挙です。

[hom_functor]

Leanは膨大で見きれないような証明のチェックには有益だが、具体的にここが飛躍だと言われて合意取れないところに入れてもなぁ。証明の飛躍がLeanの飛躍した"公理"にマッピングされて、その正しさで揉めるだけ

[sophizm]

"「ケプラー予想」は（略）12人の数学者が4年かけて検証したが「証明の正しさは99%」としか確信が持てなかった。そこで証明チェッカーの検証が始まった。論文は約10年かけコードに形式化（略）数十人で10年かかった"

[hobo_king]

IUTが正しかろうが間違っていようが、一部の数学はもう人類の脳力の限界を超えつつある気がする。今後そういう分野増えるんだろうなあ。AIが予想を立ててAIが証明し、人間はよくわからないままそれを使う、みたいな。

[brain-box]

そんな一般化したツールで入力、証明できるのであれば、そもそもこんな事態になっていないのでは。形式化の際に「飛躍してる」と言われるだけのような。

[outalaw]

その前に他の研究者に指摘されたことを真摯に答えたほうが良いと思います　相手を馬鹿にする回答しかしないから呆れられてなかったことにされてしまっている

[flont]

形式化の過程に飛躍があるという話にすり替わるだけじゃないかという正しい指摘より「形式化のなんたるかが分かってない」と言ってる本当に分かってない形式化エアプ側に星付くの、やっぱりはてブは科学ダメだな

[greenbow]

まあそうですよね “IUT理論を記述したコードが、望月教授の意図した主張と正確に対応しているかを確認することは非常に難しいこともある”

[igni3]

定理証明支援ソフトってCoqとか？一般には馴染みないけど、おかしなことにはならんよ。情報系ならカリーハワードとかどこかで聞いてるやろ。

[petite_blue]

うまくいけば証明支援ソフトで未解決問題を証明した最初の事例になるのかも。ぜひ頑張ってほしい

[call_me_nots]

“Leanは米マイクロソフトリサーチが開発した。証明を構成する定義や概念、論理の流れをすべてプログラムのコードとして記述し、コンピューターがその整合性を1行ずつ検証していく仕組み”

[agrisearch]

京都大の望月新一教授、定理証明支援ソフト「Lean（リーン）」

[mimizukuma]

まだやってる

[siles]

「日本でのみ真とされる数学証明の奇妙な物語」（2025年6月5日、New Scientist の翻訳） https://4bungi.jp/blog/250816-new-scientist-jun-5th/

[mkusaka]

ABC予想とIUT理論を、Leanで形式化し20人規模の理解者論争を決着させる試みを解説

[Cru]

有料部分読めてないが。こりゃ少なくともDNNではないな。既存の形式論理に落とし込めるのなら、そりゃ正しいってことになる…

[kamei_rio]

ケプラー予想や四色問題のように反証を総当たりで潰せるならともかく、この問題で使えるんだろうか。論理に飛躍があるのでは？説明不足では？は既に指摘されているわけだし、意味があるんだろうか

[Wafer]

数学者は性格悪くてナンボ

[ttysumi]

タイトルだけで【あほか】と思う。数学の自殺行為では？タイトルおかしい。コンピューターではなく、プログラム、アルゴリズム、他の何かだろう。証明の前にこの人の数学の世界が数学であると認めさせるしかない。

[azzr]

証明部分に飛躍があればチェッカーを通せないんだから「形式化の過程に飛躍がある」なんて話にはならないよ。ABC予想のステートメント部分だけ表現できていれば、証明部分は元々の証明を映し取っている必要はないし。

[simila]

megumin1 とかいう定番的外れコメ師の的外れコメにスター集まってるのが正にハテブだなぁ。この人はただの底辺IT屋だと思うよ。

[xsde]

ABC予想のような巨大な証明を定理証明系で書き下ろすのは、ブラウザをすべてアセンブラで書くくらいの苦行。何人月かかるのだろう。。

[kamiokando]

マイクロソフト、そんなこともやってたのか。天才過ぎてよく理解できないけど面白い。

[hgaragght]

アプローチは色々あった方が良いよね。もしも証明されれば凄い奴みたいだし、査読者増やす切っ掛けは大事。

[hetarechiraura]

とんでもねえ頭脳であることは間違いないと思うから本件は計算機と他人に任せてなんか他のことやってほしい。言われんでもしとるんやろうけど。

[samu_i]

おれはそんなことに時間を使ってらんないね

[t-tanaka]

形式化できるんだ。意外。私たちが使っている論理学で形式化できる数学と，別の論理で構成された数学の「宇宙」をつなぐ理論かと思ってた。そこまでは飛躍してないのか。

[tomymot]

“HPで公開”HPって呼ぶタイプね

[mutinomuti]

“見かねた実業家が「間違いの証明」に100万ドルの賞金をかけ”たのに間違いを証明できてないのか

[georgew]

いずれにせよまたとてつもない労力と時間を要しそうではある。望月さんがご存命中に決着つくのかどうかっていう懸念も拭えない。

[pekee-nuee-nuee]

なんかあのメタな話をLeanで表現できるのかどうかって感じだな

[camellow]

理論が難解で専門家でも理解できないというのはどういう事なのだろう。自分のようなモノには永遠にわからないお話なんだろうなあ。

[yamazakicker]

Lean使うのか！最近Leanをちらほら耳にする気がする