https://b.hatena.ne.jp/entry/s/www.asahi.com/articles/ASTCY1BZVTCYDIFI00XM.html 数学の超難問「ABC予想」をめぐる論争に、決着がつくかもしれない。コンピューターの力を借りて、証明の正否を検証する動きが出てきた。京都大の望月新一教授（56）も、この試みに肯定的だ。証明が正しいかど… https://b.hatena.ne.jp/TakayukiN627/20260104#bookmark-4779930834351478753 2026-01-04T05:46:07Z 数学 https://b.hatena.ne.jp/koto7638/20251214#bookmark-4779930834351478753 2025-12-14T08:23:55Z https://b.hatena.ne.jp/call_me_nots/20251208#bookmark-4779930834351478753 “Leanは米マイクロソフトリサーチが開発した。証明を構成する定義や概念、論理の流れをすべてプログラムのコードとして記述し、コンピューターがその整合性を1行ずつ検証していく仕組み” 2025-12-08T05:24:12Z https://b.hatena.ne.jp/harumanachika/20251208#bookmark-4779930834351478753 2025-12-07T22:13:39Z mass_media math https://b.hatena.ne.jp/funaki_naoto/20251208#bookmark-4779930834351478753 2025-12-07T16:29:39Z math https://b.hatena.ne.jp/togusa5/20251208#bookmark-4779930834351478753 2025-12-07T16:13:29Z あとで読む https://b.hatena.ne.jp/agrisearch/20251207#bookmark-4779930834351478753 京都大の望月新一教授、定理証明支援ソフト「Lean（リーン）」 2025-12-07T14:53:10Z 科学 AI https://b.hatena.ne.jp/omega314/20251207#bookmark-4779930834351478753 2025-12-07T14:29:37Z https://b.hatena.ne.jp/xiangze/20251207#bookmark-4779930834351478753 2025-12-07T14:22:09Z https://b.hatena.ne.jp/yamori0408/20251207#bookmark-4779930834351478753 2025-12-07T14:02:07Z あとで読む https://b.hatena.ne.jp/mimizukuma/20251207#bookmark-4779974444936781921 まだやってる 2025-12-07T08:56:34Z https://b.hatena.ne.jp/siles/20251207#bookmark-4779930834351478753 「日本でのみ真とされる数学証明の奇妙な物語」（2025年6月5日、New Scientist の翻訳） https://4bungi.jp/blog/250816-new-scientist-jun-5th/ 2025-12-07T08:23:57Z 数学 https://b.hatena.ne.jp/petite_blue/20251207#bookmark-4779930834351478753 うまくいけば証明支援ソフトで未解決問題を証明した最初の事例になるのかも。ぜひ頑張ってほしい 2025-12-07T06:55:09Z math 証明支援 https://b.hatena.ne.jp/mkusaka/20251207#bookmark-4779930834351478753 ABC予想とIUT理論を、Leanで形式化し20人規模の理解者論争を決着させる試みを解説 2025-12-07T06:26:09Z AI要約 ABC予想 望月新一 Lean 形式化 定理証明支援系 https://b.hatena.ne.jp/andsoatlast/20251207#bookmark-4779930834351478753 2025-12-07T03:21:50Z https://b.hatena.ne.jp/OKU_s62/20251207#bookmark-4779930834351478753 2025-12-07T02:29:02Z 数学 lean prover https://b.hatena.ne.jp/Cru/20251207#bookmark-4779930834351478753 有料部分読めてないが。こりゃ少なくともDNNではないな。既存の形式論理に落とし込めるのなら、そりゃ正しいってことになる… 2025-12-07T01:53:11Z 興味深い 数学 機械学習 https://b.hatena.ne.jp/parakeetfish/20251207#bookmark-4779930834351478753 2025-12-06T23:03:40Z https://b.hatena.ne.jp/kamei_rio/20251207#bookmark-4779930834351478753 ケプラー予想や四色問題のように反証を総当たりで潰せるならともかく、この問題で使えるんだろうか。論理に飛躍があるのでは？説明不足では？は既に指摘されているわけだし、意味があるんだろうか 2025-12-06T22:23:32Z https://b.hatena.ne.jp/takeishi/20251207#bookmark-4779930834351478753 2025-12-06T16:45:41Z 数学 https://b.hatena.ne.jp/keint/20251207#bookmark-4779930834351478753 2025-12-06T16:28:45Z https://b.hatena.ne.jp/ttysumi/20251207#bookmark-4779930834351478753 タイトルだけで【あほか】と思う。数学の自殺行為では？タイトルおかしい。コンピューターではなく、プログラム、アルゴリズム、他の何かだろう。証明の前にこの人の数学の世界が数学であると認めさせるしかない。 2025-12-06T16:25:55Z https://b.hatena.ne.jp/akiu-ksg/20251207#bookmark-4779930834351478753 2025-12-06T16:25:28Z https://b.hatena.ne.jp/akinonika/20251207#bookmark-4779930834351478753 2025-12-06T15:47:13Z https://b.hatena.ne.jp/azzr/20251207#bookmark-4779930834351478753 証明部分に飛躍があればチェッカーを通せないんだから「形式化の過程に飛躍がある」なんて話にはならないよ。ABC予想のステートメント部分だけ表現できていれば、証明部分は元々の証明を映し取っている必要はないし。 2025-12-06T15:04:27Z https://b.hatena.ne.jp/simila/20251206#bookmark-4779930834351478753 megumin1 とかいう定番的外れコメ師の的外れコメにスター集まってるのが正にハテブだなぁ。この人はただの底辺IT屋だと思うよ。 2025-12-06T14:33:14Z https://b.hatena.ne.jp/outalaw/20251206#bookmark-4779930834351478753 その前に他の研究者に指摘されたことを真摯に答えたほうが良いと思います　相手を馬鹿にする回答しかしないから呆れられてなかったことにされてしまっている 2025-12-06T14:05:54Z https://b.hatena.ne.jp/htnma108/20251206#bookmark-4779930834351478753 2025-12-06T14:05:17Z https://b.hatena.ne.jp/greenmold/20251206#bookmark-4779930834351478753 2025-12-06T13:47:15Z あとで読む https://b.hatena.ne.jp/fuzitahoushirou/20251206#bookmark-4779930834351478753 2025-12-06T13:19:52Z https://b.hatena.ne.jp/vitamin41/20251206#bookmark-4779930834351478753 2025-12-06T13:08:55Z https://b.hatena.ne.jp/ma__ko__to/20251206#bookmark-4779930834351478753 2025-12-06T13:02:07Z あとで読む https://b.hatena.ne.jp/yukatti/20251206#bookmark-4779930834351478753 2025-12-06T12:58:29Z science news https://b.hatena.ne.jp/yasuhiro1212/20251206#bookmark-4779930834351478753 2025-12-06T12:51:54Z あとで読む https://b.hatena.ne.jp/asianwind/20251206#bookmark-4779930834351478753 2025-12-06T12:46:46Z 数学 科学 https://b.hatena.ne.jp/igni3/20251206#bookmark-4779930834351478753 定理証明支援ソフトってCoqとか？一般には馴染みないけど、おかしなことにはならんよ。情報系ならカリーハワードとかどこかで聞いてるやろ。 2025-12-06T12:31:09Z https://b.hatena.ne.jp/xsde/20251206#bookmark-4779930834351478753 ABC予想のような巨大な証明を定理証明系で書き下ろすのは、ブラウザをすべてアセンブラで書くくらいの苦行。何人月かかるのだろう。。 2025-12-06T12:24:39Z https://b.hatena.ne.jp/penguin_dane/20251206#bookmark-4779930834351478753 2025-12-06T12:21:16Z 2025 新聞社 数学 https://b.hatena.ne.jp/kazuya030/20251206#bookmark-4779930834351478753 2025-12-06T12:18:09Z https://b.hatena.ne.jp/a842/20251206#bookmark-4779930834351478753 2025-12-06T12:12:35Z https://b.hatena.ne.jp/kamiokando/20251206#bookmark-4779930834351478753 マイクロソフト、そんなこともやってたのか。天才過ぎてよく理解できないけど面白い。 2025-12-06T12:05:28Z https://b.hatena.ne.jp/inomoy/20251206#bookmark-4779930834351478753 2025-12-06T12:00:34Z https://b.hatena.ne.jp/txmx5/20251206#bookmark-4779930834351478753 2025-12-06T11:54:44Z あとで読む https://b.hatena.ne.jp/hgaragght/20251206#bookmark-4779930834351478753 アプローチは色々あった方が良いよね。もしも証明されれば凄い奴みたいだし、査読者増やす切っ掛けは大事。 2025-12-06T11:47:33Z https://b.hatena.ne.jp/hetarechiraura/20251206#bookmark-4779930834351478753 とんでもねえ頭脳であることは間違いないと思うから本件は計算機と他人に任せてなんか他のことやってほしい。言われんでもしとるんやろうけど。 2025-12-06T11:39:13Z https://b.hatena.ne.jp/fjch/20251206#bookmark-4779930834351478753 2025-12-06T11:38:13Z あとで読む https://b.hatena.ne.jp/ozean-schloss/20251206#bookmark-4779930834351478753 2025-12-06T11:29:42Z あとで読む https://b.hatena.ne.jp/yada2003/20251206#bookmark-4779930834351478753 2025-12-06T11:18:46Z あとで読む https://b.hatena.ne.jp/yada20031025/20251206#bookmark-4779930834351478753 2025-12-06T11:15:24Z あとで読む https://b.hatena.ne.jp/repunit/20251206#bookmark-4779930834351478753 2025-12-06T10:57:14Z https://b.hatena.ne.jp/tabloid/20251206#bookmark-4779930834351478753 2025-12-06T10:55:11Z https://b.hatena.ne.jp/ET777/20251206#bookmark-4779930834351478753 2025-12-06T10:37:12Z あとで読む https://b.hatena.ne.jp/yamamototarou46542/20251206#bookmark-4779930834351478753 2025-12-06T10:07:24Z oooooo https://b.hatena.ne.jp/flont/20251206#bookmark-4779930834351478753 形式化の過程に飛躍があるという話にすり替わるだけじゃないかという正しい指摘より「形式化のなんたるかが分かってない」と言ってる本当に分かってない形式化エアプ側に星付くの、やっぱりはてブは科学ダメだな 2025-12-06T10:06:06Z https://b.hatena.ne.jp/demandosigno/20251206#bookmark-4779930834351478753 2025-12-06T09:59:25Z https://b.hatena.ne.jp/samu_i/20251206#bookmark-4779930834351478753 おれはそんなことに時間を使ってらんないね 2025-12-06T09:48:40Z https://b.hatena.ne.jp/tt_w54s/20251206#bookmark-4779930834351478753 2025-12-06T09:44:18Z https://b.hatena.ne.jp/t-tanaka/20251206#bookmark-4779930834351478753 形式化できるんだ。意外。私たちが使っている論理学で形式化できる数学と，別の論理で構成された数学の「宇宙」をつなぐ理論かと思ってた。そこまでは飛躍してないのか。 2025-12-06T09:04:21Z 数学 https://b.hatena.ne.jp/tomymot/20251206#bookmark-4779930834351478753 “HPで公開”HPって呼ぶタイプね 2025-12-06T08:36:44Z https://b.hatena.ne.jp/momonga_dash/20251206#bookmark-4779930834351478753 2025-12-06T08:27:24Z https://b.hatena.ne.jp/R2M/20251206#bookmark-4779930834351478753 2025-12-06T08:05:59Z 数学 https://b.hatena.ne.jp/greenbow/20251206#bookmark-4779930834351478753 まあそうですよね “IUT理論を記述したコードが、望月教授の意図した主張と正確に対応しているかを確認することは非常に難しいこともある” 2025-12-06T07:54:19Z 数学 https://b.hatena.ne.jp/hobo_king/20251206#bookmark-4779930834351478753 IUTが正しかろうが間違っていようが、一部の数学はもう人類の脳力の限界を超えつつある気がする。今後そういう分野増えるんだろうなあ。AIが予想を立ててAIが証明し、人間はよくわからないままそれを使う、みたいな。 2025-12-06T07:51:51Z 数学 https://b.hatena.ne.jp/dreamyou/20251206#bookmark-4779930834351478753 2025-12-06T07:39:36Z https://b.hatena.ne.jp/single_wing/20251206#bookmark-4779930834351478753 2025-12-06T07:27:12Z https://b.hatena.ne.jp/shoutinginabucket/20251206#bookmark-4779930834351478753 2025-12-06T07:25:08Z https://b.hatena.ne.jp/Unimmo/20251206#bookmark-4779930834351478753 2025-12-06T07:04:52Z https://b.hatena.ne.jp/hom_functor/20251206#bookmark-4779930834351478753 Leanは膨大で見きれないような証明のチェックには有益だが、具体的にここが飛躍だと言われて合意取れないところに入れてもなぁ。証明の飛躍がLeanの飛躍した"公理"にマッピングされて、その正しさで揉めるだけ 2025-12-06T07:01:13Z https://b.hatena.ne.jp/yonigex/20251206#bookmark-4779930834351478753 2025-12-06T07:01:07Z あとで読む https://b.hatena.ne.jp/S0R5/20251206#bookmark-4779930834351478753 2025-12-06T06:53:33Z 数学 https://b.hatena.ne.jp/mutinomuti/20251206#bookmark-4779930834351478753 “見かねた実業家が「間違いの証明」に100万ドルの賞金をかけ”たのに間違いを証明できてないのか 2025-12-06T06:47:40Z https://b.hatena.ne.jp/georgew/20251206#bookmark-4779930834351478753 いずれにせよまたとてつもない労力と時間を要しそうではある。望月さんがご存命中に決着つくのかどうかっていう懸念も拭えない。 2025-12-06T06:37:56Z https://b.hatena.ne.jp/mesotaro/20251206#bookmark-4779930834351478753 2025-12-06T06:37:17Z https://b.hatena.ne.jp/pekee-nuee-nuee/20251206#bookmark-4779930834351478753 なんかあのメタな話をLeanで表現できるのかどうかって感じだな 2025-12-06T06:29:50Z https://b.hatena.ne.jp/camellow/20251206#bookmark-4779930834351478753 理論が難解で専門家でも理解できないというのはどういう事なのだろう。自分のようなモノには永遠にわからないお話なんだろうなあ。 2025-12-06T06:12:04Z https://b.hatena.ne.jp/hazardprofile/20251206#bookmark-4779930834351478753 2025-12-06T06:06:48Z https://b.hatena.ne.jp/nodat/20251206#bookmark-4779930834351478753 2025-12-06T06:02:30Z https://b.hatena.ne.jp/laislanopira/20251206#bookmark-4779930834351478753 2025-12-06T05:58:53Z 科学 https://b.hatena.ne.jp/yamazakicker/20251206#bookmark-4779930834351478753 Lean使うのか！最近Leanをちらほら耳にする気がする 2025-12-06T05:40:17Z https://b.hatena.ne.jp/obsv/20251206#bookmark-4779930834351478753 2025-12-06T05:37:04Z あとで読む https://b.hatena.ne.jp/byaa0001/20251206#bookmark-4779930834351478753 ヒルベルトプログラム的なあれやんね 2025-12-06T05:37:03Z https://b.hatena.ne.jp/theatrical/20251206#bookmark-4779930834351478753 望月氏の批判に対する態度はお前らが理解してないだけだ、俺が正しい。と言ったかなり独善的に見えるので、懐疑的に思ってしまうが、そう言う感覚とは別に白黒つくなら良いとはもちろん思う 2025-12-06T05:33:40Z https://b.hatena.ne.jp/roorenzo/20251206#bookmark-4779930834351478753 2025-12-06T05:33:34Z https://b.hatena.ne.jp/nakex1/20251206#bookmark-4779930834351478753 2025-12-06T05:27:33Z 数学 https://b.hatena.ne.jp/NikugaTabetainoyo/20251206#bookmark-4779930834351478753 2025-12-06T05:23:59Z https://b.hatena.ne.jp/megumin1/20251206#bookmark-4779930834351478753 "形式化の際に「飛躍してる」と言われるだけのような。" <= 形式化手法を理解していないコメントばかり。Leanが「正しい」という結論をだす形式化がひとつでも見つかればそれはABC予想の証明であり数学史上の快挙です。 2025-12-06T05:13:35Z https://b.hatena.ne.jp/hasiduki/20251206#bookmark-4779930834351478753 そんなことしたら欠陥が明らかになるのでは？？？？！！？ 2025-12-06T05:07:34Z https://b.hatena.ne.jp/Itisango/20251206#bookmark-4779930834351478753 lean 2025-12-06T05:05:43Z https://b.hatena.ne.jp/peketamin/20251206#bookmark-4779930834351478753 2025-12-06T04:57:53Z https://b.hatena.ne.jp/ROYGB/20251206#bookmark-4779930834351478753 四色問題では考えられうるパターンを総当たりで証明した。 2025-12-06T04:52:47Z https://b.hatena.ne.jp/fuji_haruka/20251206#bookmark-4779930834351478753 Leanきたこれ 2025-12-06T04:38:55Z https://b.hatena.ne.jp/roanapua/20251206#bookmark-4779930834351478753 2025-12-06T04:27:45Z https://b.hatena.ne.jp/kaos2009/20251206#bookmark-4779930834351478753 2025-12-06T04:22:17Z https://b.hatena.ne.jp/TakamoriTarou/20251206#bookmark-4779930834351478753 なるほどわからん　　　さらに何十年もかかるかもなのか 2025-12-06T04:19:58Z https://b.hatena.ne.jp/sophizm/20251206#bookmark-4779930834351478753 "「ケプラー予想」は（略）12人の数学者が4年かけて検証したが「証明の正しさは99%」としか確信が持てなかった。そこで証明チェッカーの検証が始まった。論文は約10年かけコードに形式化（略）数十人で10年かかった" 2025-12-06T04:19:19Z https://b.hatena.ne.jp/toaruR/20251206#bookmark-4779930834351478753 形式化って、ひょっとして屏風の虎を出すような話？(・ω・) 2025-12-06T04:16:59Z https://b.hatena.ne.jp/brain-box/20251206#bookmark-4779930834351478753 そんな一般化したツールで入力、証明できるのであれば、そもそもこんな事態になっていないのでは。形式化の際に「飛躍してる」と言われるだけのような。 2025-12-06T04:14:22Z https://b.hatena.ne.jp/en-en-ra/20251206#bookmark-4779930834351478753 2025-12-06T04:13:13Z あとで読む https://b.hatena.ne.jp/aont/20251206#bookmark-4779934915109484673 2025-12-06T04:13:11Z https://b.hatena.ne.jp/narwhal/20251206#bookmark-4779930834351478753 2025-12-06T04:11:44Z mathematics