ハルだよ。今回は数学の歴史の話なんだけど、AIを仕事で使うときのお手本としてすごく参考になるから持ってきた。20世紀を代表する論理学者のひとり、Kurt Gödel（クルト・ゲーデル）が80年以上前に速記で書きためたノートを研究者が Claude に読ませたら、2日ほどで約650ページの解説が返ってきた、とThe Guardian が報じているんだよ。しかも抜き出された定理候補663件のうち、約400件はコンピュータによる証明チェックをそのまま通った。でもこの話のキモは「AIすごい」じゃないと思った。人が下ごしらえをして、人が点検して、機械で確かめて、そこまでやってやっと成果と呼べる。その順番のほうが大事なんだよね🤔
日本の会社にとって：大半の会社には直接の関係はないよ。関係するのは、古い手書きの設計ノートや帳簿、社史の資料をAIで読み解こうとしているメーカーや老舗企業。計画を立てる段階で、AIに渡す前の文字起こしをだれがやるかと、出てきた結果をだれが1件ずつ点検するかを決めておこう。
10年近く手で書き起こしてきたノートを、AIに渡してみた
主役はヘルシンキ大学の論理学者 Jan von Plato さん。ゲーデルが1940年代初めに書いたノートは16冊、全部で約1,009ページあって、その大半が「ガーベルスベルガー式」っていうドイツ語圏の古い速記で書かれてる。速記は、記号みたいな省略文字で話す速さに追いつくようにメモする書き方のこと。von Plato さんによると、これを読める人は世界に6人しかいないんだって👀
ヘルシンキ大学には「Gödel Enigma」という研究グループがあって、公式の計画説明では、この16冊の速記ノートを書き起こして中身を読み解くことが研究の対象になっている。Guardian によると、von Plato さんはこの計画を2017年に始め、欧州研究会議（ERC、EUの研究費を出す機関）から250万ユーロの助成を受けている。ちなみに公式ページには、Claude を使ったことは載っていないよ。
人の手だとどのくらいのペースかというと、年に約50ページ、週に1ページくらいだと報じられている。1,009ページあるから、単純に割ると20年コースだよね。そこで9月、von Plato さんは自分で書き起こした原稿と、自分の著書6冊などをまとめて Claude に渡した。すると2日ほどで約650ページの解説が返ってきて、663件の定理が抜き出された。Guardian が伝えている流れはこんな感じ。
ここで大事なのは、Claude が速記の原本を直接読んだわけじゃないってこと。von Plato さんが何年もかけて普通の文字に起こした原稿があったから、AIに渡せたんだよ。世界に6人しか読めない速記を先に人が読んでいなかったら、この話は始まってすらいない。AIが速くなったのは2つ目の工程からで、いちばん地味で重い1つ目の工程は、まるごと人がやっていたんだよね。
663件を「証明チェック機」にかけたら、どうなった？
次の段階がおもしろい。抜き出した663件を Coq（コック）という道具にかけた、とMLQ.ai がまとめている。Coq は「定理証明支援系」と呼ばれる道具で、数学の証明が本当に正しいかをコンピュータが1ステップずつ厳しく確かめてくれる。人間の「たぶん合ってる」を一切許さない、超きびしい採点係だと思えばいいよ💡
結果はこう報じられている。
- そのまま正しいと確認された：約400件
- 前提を足したり、言い方を締めたりする修正が必要：約200件
- 誤り：約50件
つまり、そのまま通ったのは約6割。3割強は手を入れないと成り立たないか、そもそも間違いだった。ただ、約50件の誤りは von Plato さんにとって驚きではなかったそう。ゲーデル本人も読み返したときに、ノートの余白に「falsch!」（ドイツ語で「間違い！」）や「schlecht!」（「ダメ！」）と書き込むことがあったからだ。本人も途中で気づいてバツをつけてた、ってことだね。天才のメモにもちゃんとボツ案があるのは、ちょっと親近感😊
それと「663の定理」という数字には注意が要る。中身はゲーデルが証明しきったものだけじゃなくて、証明の筋道を書いていたもの、着想だけ書いていたものも合わせた数なんだよ。引用している記事の中には「ゲーデルが663の定理を証明した」と大きく書くものもあるけど、それは言いすぎ。そのうえで MLQ.ai によると、1970〜80年代まで世に出なかった結果を「数十件」先取りしていたほか、いまもだれも追いかけていない論理の主題が14件見つかったとされている。
いちばんの目玉、ゲーデルが「持っていた」と語った証明
報道の中心になっているのは「選択公理の独立性」の証明。ちょっと噛み砕くね。選択公理は、「どんなにたくさん箱があっても、それぞれの箱から1個ずつ中身を選び出せる」と認める、数学の基本ルールのひとつ。そして「独立性」は、このルールがほかの基本ルールからは、正しいとも間違いとも証明できないってこと。つまり、入れても入れなくても数学が矛盾しない、自由に選べるルールだと示すことなんだよ。
この証明を完成させて世に出したのは、1963年に発表した数学者の Paul Cohen だとされている。ところがゲーデルは、1966年に「自分はそれを持っていた」と語っていた。MLQ.ai によると、ノートの上ではその証明がほぼ完成していて、定義が1か所だけ違っていた。しかも正しい定義は、2年前のノートに書かれていたそう。Claude はその2つをつないで証明を組み直し、それが Coq の検証を通った、と報じられている🛠️
ノートの山の中から、別の年のページにある正しい部品を見つけてきて組み立てる。これを人間がやったら何年かかるか分からない作業だよね。大量の資料を一度に見渡してつながりを探すのはAIの得意分野で、それがよく分かる例だと思った。
でも冷静な声もある。ノートルダム大学の数学者・論理学者 Joel David Hamkins さんは、組み直された証明そのものはまだ見ていないと断ったうえで、「本当なら歴史的に面白いが、どこまでが Claude でどこまでがゲーデルかは歴史家が決めること」と話したと報じられている。さらに「Cohen の証明に似ているからといって、ゲーデルが証明を持っていたことにはならない。誰にも言わなかった仕事に功績は認められない」とも。確かに、AIが部品を拾ってつないだ時点で、それはもう「ゲーデルひとりの証明」とは言い切れないんだよね。
2日で650ページ。それでもまだ「成果」と呼べない理由
ここまで読むと「AIで20年分の仕事が2日に！」って言いたくなるけど、ハル的にはそこがいちばん危ないところだと思ってる。von Plato さん本人も「1ページずつ管理しなければならなかった」と話していて、650ページの解説は彼が1ページずつ点検したと Guardian は伝えている。2日で出てきたのは下書きの山であって、人の目を通るまでは使えないんだよ。
まだ確かめられていないことも、ここにまとめておくね。explainx.ai の Yash Thakker さんが指摘しているのは、まず論文もデータも公開されたとは報じられていないので、外の研究者が同じことをやり直して確かめられないこと。使った Claude のモデルの版も、かかった費用も明かされていない。外部の専門家による詳しい検証もまだ。そして Coq を通ったことで分かるのは「組み直された証明が正しい」ということだけで、ゲーデルが頭の中でその証明を持っていたかどうかの決着にはならない、とも書いている。この記事の数字もすべて報道にもとづくもので、ハル自身が確かめたものではないよ。
それでもこの話は、仕事でAIを使う人にとってすごくいい手本になると思った。順番を整理するとこうなる。
- 人が下ごしらえする（速記を普通の文字に起こす。年に約50ページのペース）
- AIに一気に読ませて候補をたくさん出させる（2日で650ページ、663件）
- 人が1件ずつ点検する
- 機械できびしく確かめる（Coq で約400件が合格、約250件はそのままでは使えない）
AIは、量をこなすこととつながりを探すことはめちゃくちゃ速い。でも出てきたものの3割強は、そのままじゃ使えなかった。会社の資料整理でも、AIの答えをだれが何で確かめるかを先に決めておかないと、速さがそのまま間違いの量になっちゃう。ゲーデルのノートは、そのことをすごくきれいに見せてくれた例だと思うんだよね🚀
