【数学】ABC予想証明の正否、コンピューターで決着か　望月氏が打開策示す [すらいむ★]

**すらいむ ★** · 2025/12/07(日) 20:13:00.86

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

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

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

朝日新聞DIGITAL 2025年12月6日 10時00分
https://www.asahi.com/articles/ASTCY1BZVTCYDIFI00XM.html

**名無しのひみつ** · 2025/12/07(日) 20:19:01.09

おどろいたね

**名無しのひみつ** · 2025/12/07(日) 20:28:35.81

とりあえずこの人は天才なんだからここで止まらせずに新しいところに進ませようぜ
と思ったけどもう50も半ばすぎたのか…

**名無しのひみつ** · 2025/12/07(日) 20:43:02.28

>数学界の大半は認めていない
一部のアンチが騒いでるだけでしょ

**名無しのひみつ** · 2025/12/07(日) 20:58:10.66

そもそもABC予想はリーマン予想やP≠NPと違って
数学者なら誰でも知っているというレベルの問題ではなかっただろう

**名無しのひみつ** · 2025/12/07(日) 21:18:19.99

宇宙際タイヒミュラー理論

**名無しのひみつ** · 2025/12/08(月) 00:27:38.43

マイクロソフト社のLeanを使って

**名無しのひみつ** · 2025/12/08(月) 00:31:38.31

望月氏は16歳でプリンストン大。当時、プリンストンには神童がたくさんいたが、その中でも望月氏は突出していたという。

**名無しのひみつ** · 2025/12/08(月) 01:09:55.84

そんな無駄なことは院生などに作業させて、
もっといくつも大理論を作ったり難問を提出する
作業に集中してほしい。

**名無しのひみつ** · 2025/12/08(月) 01:26:28.10

四色定理の頃のエレファントな証明とはまた違うんだろうが、宇宙際タイヒミュラー理論が証明ツールに肯定されても否定されても、面倒なことになりそうだなぁ

**名無しのひみつ** · 2025/12/08(月) 04:45:00.28

リーマン予想やれば？

**名無しのひみつ** · 2025/12/08(月) 04:56:17.41

リーマン予想はまだ誰も証明や反証を成し遂げてないよ
なので正否を判定できない

**名無しのひみつ** · 2025/12/08(月) 06:07:29.95

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

**名無しのひみつ** · 2025/12/08(月) 06:23:36.86

人間は感情的に判断することを避けられないしな
機械にやらせるのが公平だろう

**名無しのひみつ** · 2025/12/08(月) 07:13:25.55

望月氏によれば、新型のパワーアップしたバージョンのIUTを使ってセクション予想、ジーゲルゼロの非存在、更に強力なeffective ABC、の詰め合わせを一気に証明するぞ、だと。

**名無しのひみつ** · 2025/12/08(月) 13:40:04.75

予想の証明じゃなくて、まだ誰も予想すらしていない何かが出てきたりしないのかな？

**名無しのひみつ** · 2025/12/08(月) 13:41:03.86

Grokに判断させてみようずｗ

**名無しのひみつ** · 2025/12/08(月) 14:05:29.90

>>10

**名無しのひみつ** · 2025/12/08(月) 14:07:58.66

有料記事、それも朝日でスレ立てるな
時間の無駄だ

**名無しのひみつ** · 2025/12/08(月) 14:27:30.77

>>10
エレファント？
象？

エレガントの間違い？
でも四色問題だとエレガントな要素ないし

**名無しのひみつ** · 2025/12/08(月) 15:18:04.60

>>20
うん、当時コンピュータの力任せ（と思えた）パターン分け・総当たりの証明は、エレガントじゃないからってエレファントって揶揄されたの

**名無しのひみつ** · 2025/12/08(月) 15:41:53.80

出てきた結果が理解不可能とかならんかね

**名無しのひみつ** · 2025/12/08(月) 16:04:31.69

証明チェッカーに通す形式的証明より
数学者相手の説明の方が遥かに楽だろうに

**名無しのひみつ** · 2025/12/08(月) 16:15:26.66

人間には感情があるからね
望月先生が間違いを認められないのかもしれないし、ショルツェ先生がそうなのかもしれない
ツールに形式的に落とし込み検証される過程で、感情を廃した判断に至ることもあるだろう

**名無しのひみつ** · 2025/12/08(月) 18:24:25.42

これ、コンピューターで四色問題が解かれたときにも言われたんだけど、

「コンピューターＡとコンピューターＢが違った結論を出したらどうするのか？」だよ。

四色問題のときは「プログラムを精査すればよい」で決着したけれど、今やソフトウェアはブラックボックスばかりだからな。

**名無しのひみつ** · 2025/12/08(月) 18:28:40.85

4色問題は有名なので
プログラムの実装は複数あるし
プログラムの正当性の形式的証明すらある

**名無しのひみつ** · 2025/12/08(月) 18:52:22.67

生きてりゃ時々「＊＊予想」なる物が一般人に届くが、予想した奴が責任持って証明しろよ！と思うぞ、お父さんは

あと「宇宙Aがありまして、こっちに宇宙Bがありまして」って、先生一旦落ち着こう。早く食べないとご飯冷めちゃうよ

**名無しのひみつ** · 2025/12/08(月) 18:55:42.72

テーマは掛け算と足し算の関連性なんだろ、それ自体aiで解析すれば

**名無しのひみつ** · 2025/12/08(月) 19:06:59.76

数学なんだからAIというか機械処理でええのよ
これとは無関係だが、ガリレオみたいな悲劇はもう起こらないようにしたい

**名無しのひみつ** · 2025/12/08(月) 20:42:27.83

ブルーノだろ

**名無しのひみつ** · 2025/12/09(火) 03:50:26.99

246 １３２人目の素数さん 2025/12/06(土) 19:53:00.98 ID:63QplXU6
>> 232
＞望月氏が打開策示す
望月氏の主張は
証明になっていないと主張する側が打開しろ
と言っているに等しい内容ですから
到底打開策とは言えません

証明が理解不能という批判に開き直って
> (NwExp) entirely standard practice in professional
> mathematics for research papers to be written with
> a rather narrowly defined circle of experts in mind.
と言い放っているにもかかわらず
形式化が"narrowly defined circle of experts"によってではなく
外部の研究者によってなされるべきと言っているのですから
> (LnCom) the task of communicating the mathematical
> content of IUT to mathematicians (such as arithmetic
> geometers) with professional expertise in writing
> Lean code is one important area of currently on going
> efforts with regard to the goal of Lean-style
> formalization of IUT.

当初は歓待されたのにご存じの結果に終わった
Joshi氏やBoyd氏の顛末に鑑みて
望月氏に協力する研究者が現れるはずもありません
（標準的な遠アーベル幾何の形式化は別）

形式化できないのは外部の数学者がiutを
理解できないから・拒絶しているからだと
これまで通りに責任を転嫁して
自らを納得させることになるのではないでしょうか

**名無しのひみつ** · 2025/12/09(火) 03:51:34.79

別に本人が形式化を実行する必要はありませんが
本人が音頭を取って本人の責任の下に行われるのでなければ
事態は何も進展しません

証明責任は証明を主張する側にあります
途轍もない主張には途轍もなく固い証拠が必要です（カール・セーガン）

**名無しのひみつ** · 2025/12/09(火) 11:54:36.54

これはこれでやってみればいいんじゃないの
既存の概念で成り立ってるコンピュータ言語で記述できるのかわからないけど

**名無しのひみつ** · 2025/12/09(火) 12:04:35.32

証明の中に人類がまだ十分にその存在を意識していない
公理を暗黙に導入している可能性があるからな。
その公理がなければ証明不可能な命題だとすれば、。。。
そういう可能性もある。
証明チェッカーはそういう証明の穴が無いことを
示しうる。
しかし数学的に証明が可能な問題であっても、
それを具体的に書き下すことが事実上不可能な
問題はいくらでもある。たとえば将棋は千日手
を禁止すれば、先手必勝か先手必敗か引き分けか
に必ずなるはずだが、たとえば先手必勝である
というのが真実だとして、それを具体的に証明を
記述してみることは、おそらく誰にもできない。
証明が数学的に可能だとしても、その記述量は
現実的なものではないだろうからだ。宇宙の
すべての原子に0と1を割り当てて記述したと
しても、書き切れない程のビット長の記述文章
になるだろうから。

**名無しのひみつ** · 2025/12/09(火) 12:39:12.04

ちゃんとステップ毎に人間が検証できるならありかも

**名無しのひみつ** · 2025/12/09(火) 15:13:46.11

>>33
記述に使うのは結局は推論系と公理系ですよ
そこがしっかり厳密化できていれば
証明系の言語に乗せるのは時間が解決する問題
けど厳密化が結構難しい
数学家はそこまで厳密に考えてるわけではないので
証明されてない新定理を使った推論を結構重ねてる

**名無しのひみつ** · 2025/12/09(火) 15:15:38.25

>>34
厳密でなくてもいいけど
どんな証明も見つかってないものは
証明されてないのだから
証明系の言語で記述できないのは当たり前です
証明がないのだから記述しようがない
予想の段階ですから

**名無しのひみつ** · 2025/12/09(火) 20:37:11.78

ScholzeやTaoがLeanに貢献してるな
望月の証明はダメでしたってなったらまた嫉妬ガー

**名無しのひみつ** · 2025/12/10(水) 07:03:17.82

想像してみよう、仮にまだ人類が選択公理あるいは
それと同等の公理の必要性をまったく認知していなかった
とする。しかしなぜかリーンのような形式証明系は
作られていて、有限集合の場合には当然成り立つ性質だから
その延長で、形式論理にも選択公理が意識されずに密輸入
されていたとする。
　すると、選択公理がなければ証明できないはずの定理が
証明できてしまうのだ。つまり証明系の穴なんだが、
それを指摘するということは選択公理を認識して、
それが公理たりえるものである（仮定しない数学体系も
可能だ）ということが把握されなければありえない。

**名無しのひみつ** · 2025/12/10(水) 19:33:09.03

そのコンピュータのプログラムだかAIだかが正しい証明はどうやってするんだ？

**名無しのひみつ** · 2025/12/10(水) 21:26:27.74

>>40
グーグル検索で
「さてどん尻に控えしは」
を検索してみな

ＡＩ様が爆笑もの（歌舞伎好きにとっては）の要約を出すよ

**名無しのひみつ** · 2025/12/11(木) 04:54:55.58

2次元射影幾何の公理からはデザルグの定理は導けず、
公理とは独立である。つまり2次元射影幾何では
デザルグの定理はそれを使うためには定理ではなくて
公理にしなければならない。
しかし3次元以上の射影幾何の公理からはデザルグの定理は
導ける。
そのことが形式証明検証系で正しく出せるか？
（望ましくは半自動的に次元を分類してくれて）

【数学】ABC予想証明の正否、コンピューターで決着か 望月氏が打開策示す [すらいむ★]

【数学】ABC予想証明の正否、コンピューターで決着か　望月氏が打開策示す [すらいむ★]