HN201180
ついに解明？Conway予想を証明してみた件
I vibed a proof of Conway's conjecture
m-hodges・約15時間前
議論
10件Dan Abramovが公開しているリポジトリにて、Conway予想の証明に関する考察が展開されています。なぜ彼がこの証明が正しいと確信しているのか、その論理的なアプローチや詳細については以下のGitHubリンクから確認できます。興味のある方はぜひチェックしてみてください。詳細はこちら: https://github.com/gaearon/conway-refinement#why-i-think-its-correct
2日目には「無とゼロの間」と「ゼロと無の間」という2つの隙間ができる。その2つの隙間に2つの数字が生まれる。それを-1と1と呼ぶ。
ここで迷子になった。数学に関しては正式に「自分は頭が悪すぎる」という認定を受けたと思う。
いずれにせよ、AIを最も価値ある形で活用できるのは数学者自身だと私は信じている
数学の純粋なアウトプットは増えるだろうし、数学者はこれを解明して役立てるための新たな仕事が増えることになる。AIは「無限の猿定理[1]」における猿の役割を果たす。今や我々にはLLM版の補題が必要だ。例えば「十分なトークン予算さえあれば、有限のLLMエージェントがすべての定理をほぼ確実に発見する」といったようなものだ。
超現実数（surreal numbers）とその周辺のゲーム理論的コンセプトを解説した素晴らしい入門動画として、3Blue1BrownのSummer of Mathコンペで勝者となったHackenbush[0]のこの動画がある。
私は数人の数学者にタイポ修正案をいくつかメールで送ったところ、そのうちのいくつかは正当な修正であるとの確認を得られた。しかし、Lean（証明支援系）で裏付けられていない問題の中には、単なる誤解だったものもあった。
このプロジェクトはとても素晴らしいと思うけれど、自分が「アマチュア」以上だと名乗れるほどの時間をかけて努力する前に、専門家にいきなりメールを送るのは適切なのだろうか？投稿者のメールは役立ったかもしれないが、何十億もの人がLLMを使って新しい分野に足を踏み入れており、すでにメールのノイズは増大しているんだ。
（背景：数学のトレーニングを受けて論文発表もしているが、いまだアマチュアの数学者としての立場です）
これはクールなブログ投稿だし、正しい方向へ進んでいると思うよ。やりながら証明の理解を深め始めているね。
自分自身で証明を追えるようになるまで、簡略化と理解のステップを続けることをおすすめする。私が似たようなことをした経験からいくつかアドバイスを：
-
証明の個々のパートが他で見つからないか確認（またはAIに聞く）してみる。つまり、議論がどこかのコピーになっていないか？もしそうなら、出典を明記することが重要だし、通常はそれによって「定理Xにより〜」のように簡略化できる。
-
冗長なパターンを探して、それらを統合してみる。
-
AIにジャーナルの批判的査読者になってもらい、その批判を修正するように試みる。
-
簡略化を続ける！最終的な結果は、実は比較的短くまとめられるはずだと想定してみる。
幸運を祈る！
なぜかこのアプローチ、ファンタジーの魔法体系における「ウィザード（術師）」と「ソーサラー（魔術師）」の違いを連想させる。「ウィザード」の魔法は、偉大な力を持つ（必要あるいは有益な）道具に助けられることもあるが、根本的には難解な物事への深い学習と理解に基づくものだ。「ソーサラー」は超自然的な存在を召喚し、それを制御・懐柔し、自分自身や他者をその存在から守る（程度の差はあるが）...しかし、実際に目的の魔法的「効果」を発揮するのはその召喚された存在だ。
コンピューティングは歴史的にウィザードの領域だった。これほど多くの人々がこれほど強くソーサラーの方向に突き進み、しかも彼ら自身が魔法が成功したかどうかを検証できないような他の分野にまでそのソーサリーを適用しているのを見るのは、興味深い（？）ことだ。
著者がLLMとやり取りする様子が非常に興味深い。例えば：
しかし、私は単に何らかの結果が欲しいわけではなかった。私を惹きつけるものが欲しかったのだ。
最初、私はClaudeにこう尋ねた：
私：超現実数の研究プログラムにおいて、どの未解決問題が最もあなたを惹きつけますか？また、その理由は？
「私を惹きつける（pulls me）」から「あなたを惹きつける（pulls you）」への切り替えに注目してほしい。著者はここで、自身とLLMの関係性や境界線をどう捉えているんだろう？
-
LLMが興味深いとフラグを立てたものを探し、自分もそれを面白いと感じられることを期待している？
-
「興味深さ」を普遍的（観察者に依存しない）な性質だと見なしていて、興味深いものを探すためにLLMを利用している？
-
「興味深いものを探す」という欲求をLLMに委譲し、著者の感情に関係なく、AIが興味深いと判断するものを探させている？
-
LLMを思考プロセスの一部と見ていて、自分とAIを区別していない？
-
LLMを自分自身の一部と見なしていて、結合された存在を二人称で呼んでいる？
このあたり、ぜひ詳しく知りたいところだ。
私が一番思ったのは、彼がここで実行していた一般的な作業は、実は価値があって大多数の人には難しいことだということだ。かつてのGoogle検索が難しい作業だったことや、PCのトラブルシューティングと似ている。彼がここでできていることは、実は「知性」と呼ばれる希少なスキルなんだ。本人は大したことないと思っているかもしれないが、実際には非常に希少で、ほとんどの人には難しいことだよ。深い専門知識なしにアウトプットを判断・解釈する能力は、本当に稀な才能だ。
結果を査読中のVincenzo Mantova教授[1]からのディープリンク返信：https://news.ycombinator.com/item?id=49761718
[1] https://eps.leeds.ac.uk/maths/staff/4058/dr-vincenzo-l-mantova