AIでConwayの予想を証明した話
I Vibed a Proof of Conway's Conjecture
数学に詳しくない筆者が、ClaudeとChatGPTを駆使して、50年前にJohn Conwayが提起した超現実数の「omnific integers」に関する未解決予想のLean証明を試みた。1ヶ月と大量のトークンを費やし、独立検証はまだだが、Palomar registryの機械的チェックを通過し、専門家からも声明が正しいとの意見を得ている。AIとの対話から生まれた証明の舞台裏を綴る。
私は、数学の内容を理解せずに問題を「解く」というアイデアはかなり不条理だと思った。だからこそ、なおさら魅力的に感じられた。
HNでの議論
290- gbjcantab
どういうわけか、このアプローチを見ていると、ファンタジーの魔法体系における「ウィザードリー」と「ソーサリー」の違いを思い出す。
「ウィザード」の魔法は、根本的に秘術的なものに対する深い研究と理解に基づいており、おそらくは（必要か、あるいは役立つ）強力な道具に助けられている。「ソーサラー」は超自然的存在を召喚し、彼らを操り、なだめすかし、自分や他者を彼らから守ることができる（成功の度合いはさまざまだが）……しかし、実際に望む魔法の効果を実行するのは、それらの存在なのだ。
コンピューティングは歴史的にウィザードリーの分野だった。これほど多くの人々がソーサリーの方向へと強く押し進め、しかもそのソーサリーを、自分たち自身ではその呪文が効いたかどうかを十分に検証できない他の分野に適用しているのを見るのは……興味深い（？）ことだ。
- pretzellogician
（背景：訓練を受け、論文も発表しているが、まだアマチュアの数学者。）
これはクールなブログ記事だし、君は正しい方向に進んでいて、読み進めるうちに証明を理解し始めていると思う。
自分自身で証明を追えるようになるまで、単純化と理解の道を続けることを勧める。私も似たようなことをしたので、いくつか提案を：
1. 証明の個々の部分が他の場所で見つからないか（あるいはAIに尋ねてみる）。つまり、ある議論が単に他の何かのコピーではないか？もしそうなら、それを帰属させることは重要だが、通常はこれによって単純化できる（「定理Xにより」など）。
2. 冗長なパターンを探し、それらを統合してみる。
3. AIに、あるジャーナルの批判的な査読者になってもらい、その批判を修正してみる。
4. 単純化を続ける！最終結果は実際には比較的短いかもしれないと想定して。
幸運を祈る！
- bwfan123
> いずれにせよ、AIを最も活用できるのは数学者自身だと思う
数学の純粋な生産量は増え、数学者には今、これを解き明かし、役立つものにするための仕事が増えている。AIは無限の猿定理[1]における猿の役割を果たす。今必要なのはLLMの系、つまりこんな感じだ：有限数のLLMエージェントは、無限のトークン予算が与えられれば、ほとんど確実にすべての定理を見つけ出すだろう。
- rlue
> これまでに得たすべての数を取る。次に、すでにある数の間のすべての隙間に新しい数を「生成」する（重要なのは、「すべての左」と「すべての右」も「隙間」に数えられることだ）。このステップを永遠に適用し続けると、超現実数が得られる。
私は数学者ではない。このアプローチがどうやって有理数を超えるのか、誰か説明してくれないか？
あと、これは引用ブロックとしてフォーマットされていたが、私が見る限り、この定式化がオンラインで見られるのはこのブログ記事だけだ。
- unholiness
超現実数とその周辺のゲーム理論的概念への素晴らしく作られた入門は、3Blue1BrownのSummer of Mathコンペティションで優勝したHackenbushに関するこの動画[0]だ。
[0]https://www.google.com/search?q=video+introduction+to+surrea...
- sigmar
> 何人かの数学者にいくつかのタイポ修正案をメールで送り、少なくともいくつかは本物の修正のようだと確認をもらった。しかし、Leanで裏付けられていない問題の中には、誤解だったものもあった。
このプロジェクトは本当に素晴らしいと思うが、自分を「アマチュア」以上と表現できるほどの時間を費やす前に、専門家に突然メールするのは適切だろうか？OPのメールは役に立ったかもしれないが、何十億人もの人がこれらのLLMを使って新しい分野に足を踏み入れており、メールはすでに低いシグナル対ノイズ比だ。
- howunfortunate
> 2日目には、2つの隙間がある：「何もないものとゼロの間」と「ゼロと何もないものの間」。この2つの隙間に2つの数が生成される。それらを-1と1と呼ぶ。
ここで迷った。私は公式に数学には頭が悪すぎるようだ。
- bonoboTP
私の主な考えは、彼はここで何か一般的なことを行っており、それは実際に価値があり、人類の大部分にとって難しいということだ。それは、Google検索が難しいことだった時代や、PCのトラブルシューティングのようなものだ。彼がここでできることは、実際には知能と呼ばれる稀なスキルであり、彼はそれを何でもないと思うかもしれないが、ほとんどの人にとっては実際に稀で難しい。深い専門知識なしに出力を判断し解釈する能力は、実際には非常に稀な能力だ。