感慨 -- 思えば遠くに来たもんだ

【感慨 -- 思えば遠くに来たもんだ】

昨日、不思議な感動的な体験をしました。

月末のセミナーに向けて、数学者が証明問題を解くのに、コンピュータを利用し始めていることを紹介しようとしているのですが、どうしても取り上げたいトピックがありました。

一年ほど前、連続体仮説の独立性をコンピュータ上で証明できたという論文が出ていました。彼らは、その証明を GitHubで公開していました。「証明」はコンピュータで実行可能な「プログラム」の形をしているのです。

昨日、それを実行してみたのです。

僕のくたびれた非力なMacは、証明の準備にとりかかりました。メッセージをみると、証明に必要な情報をたくさん集めているのがわかります。一時間ほどかかって、ようやく準備ができましたようです。「証明して」とコマンドを打ち込んだら、15分ほどで、証明が終わりました！

不思議な気持ちになりました。

確かに、僕が命令して僕のマシンが働いたのですが、僕は「連続体仮説の独立性」を証明したのでしょうか？

「連続体仮説」というのは、数直線上の 0と1 の間に、何個の点があるのかという問題です。カントールはこの個数についてある仮説を立てたのですが、ついには狂気にいたるまでそれを証明することができませんでした。ヒルベルトは、この問題を 20世紀の数学が解くべき問題の筆頭に掲げました。

ゲーデルは、この仮説が集合論の他の公理とは矛盾しないことを示すことができました。この問題が最終的に解いたのは、コーエンです。彼は、連続体仮説がなりたつ集合論もあれば、それが成り立たない集合論もあることを示すことに成功します。それが「連続体仮説の独立性」証明です。

arXivもGitHubもない時代でした。僕がコーヘンの論文とその準備をしたゲーデルの無矛盾性証明のレクチャーノートを手に入れるのに、田舎にいたせいもあって、3ヶ月かかりました。PCもタブレットもないので、プリンストンの真っ赤な表紙のレクチャーノートをいつも持ち歩いて、ボロボロになりました。

カントール、ヒルベルト、ゲーデル、コーエンが苦闘した問題を、こたつの上の古いMacが、一時間ちょっとで解いたのです！　かつて「連続体仮説」フェチだった僕にとっては、Open-AI の「人工知能」が、数 I レベルの「数学オリンピック」の問題のいくつかをといたことなんかより、はるかに大事件です。

もっとも、こうしたことは理論的には、頭では分かっていました。「コンピュータは、推論・証明する能力を持っている」でも、実感したのは初めてです。

ショートムービー「証明へのコンピュータの利用-- 連続体仮説をコンピュータで解く」を公開しました。

多分、たいした意味はないのですが、証明のLogも公開しました。

過去・現在・未来