-
ABC予想証明の正否、コンピューターで決着か 望月氏が打開策示す
数学の超難問「ABC予想」をめぐる論争に、決着がつくかもしれない。
コンピューターの力を借りて、証明の正否を検証する動きが出てきた。
京都大の望月新一教授（56）も、この試みに肯定的だ。
証明が正しいかどうかの決断を、数学者ではなく、コンピューターが下すことになるのか。（以下略、続きはソースでご確認ください）
朝日新聞DIGITAL 2025年12月6日 10時00分
https://www.asahi.com/articles/ASTCY1BZVTCYDIFI00XM.html
- おどろいたね
- とりあえずこの人は天才なんだからここで止まらせずに新しいところに進ませようぜ
と思ったけどもう50も半ばすぎたのか… - >数学界の大半は認めていない
一部のアンチが騒いでるだけでしょ - そもそもABC予想はリーマン予想やP≠NPと違って
数学者なら誰でも知っているというレベルの問題ではなかっただろう - 宇宙際タイヒミュラー理論
- マイクロソフト社のLeanを使って
- 望月氏は16歳でプリンストン大。当時、プリンストンには神童がたくさんいたが、その中でも望月氏は突出していたという。
- そんな無駄なことは院生などに作業させて、
もっといくつも大理論を作ったり難問を提出する
作業に集中してほしい。 - 四色定理の頃のエレファントな証明とはまた違うんだろうが、宇宙際タイヒミュラー理論が証明ツールに肯定されても否定されても、面倒なことになりそうだなぁ
- >>10
エレファント？
象？エレガントの間違い？
でも四色問題だとエレガントな要素ないし - >>20
うん、当時コンピュータの力任せ（と思えた）パターン分け・総当たりの証明は、エレガントじゃないからってエレファントって揶揄されたの - リーマン予想やれば？
- リーマン予想はまだ誰も証明や反証を成し遂げてないよ
なので正否を判定できない - 人間は感情的に判断することを避けられないしな
機械にやらせるのが公平だろう - 望月氏によれば、新型のパワーアップしたバージョンのIUTを使ってセクション予想、ジーゲルゼロの非存在、更に強力なeffective ABC、の詰め合わせを一気に証明するぞ、だと。
- 予想の証明じゃなくて、まだ誰も予想すらしていない何かが出てきたりしないのかな？
- Grokに判断させてみようずｗ
- 出てきた結果が理解不可能とかならんかね
- 証明チェッカーに通す形式的証明より
数学者相手の説明の方が遥かに楽だろうに - 人間には感情があるからね
望月先生が間違いを認められないのかもしれないし、ショルツェ先生がそうなのかもしれない
ツールに形式的に落とし込み検証される過程で、感情を廃した判断に至ることもあるだろう - これ、コンピューターで四色問題が解かれたときにも言われたんだけど、
「コンピューターＡとコンピューターＢが違った結論を出したらどうするのか？」だよ。
四色問題のときは「プログラムを精査すればよい」で決着したけれど、今やソフトウェアはブラックボックスばかりだからな。
- 4色問題は有名なので
プログラムの実装は複数あるし
プログラムの正当性の形式的証明すらある - 生きてりゃ時々「＊＊予想」なる物が一般人に届くが、予想した奴が責任持って証明しろよ！と思うぞ、お父さんは
あと「宇宙Aがありまして、こっちに宇宙Bがありまして」って、先生一旦落ち着こう。早く食べないとご飯冷めちゃうよ
- テーマは掛け算と足し算の関連性なんだろ、それ自体aiで解析すれば
- 数学なんだからAIというか機械処理でええのよ
これとは無関係だが、ガリレオみたいな悲劇はもう起こらないようにしたい - ブルーノだろ
【数学】ABC予想証明の正否、コンピューターで決着か 望月氏が打開策示す
科学ニュース＋
コメント