学生の頃は、いいプリンターがあったからいつも印刷してたな。今は画面で読む方が楽になっちゃったから、ちょっと懐かしい。

その通りだね。紙で何かを読むと、少なくとも10ポイントはIQが上がった気がする。これは本のドラフトを編集する時にも使ってる戦略なんだ。印刷したドラフトをいい場所（例えば、カフェや公園）に持って行って、じっくり読んでから、修正を.texのソースに戻すんだ。これを何度も繰り返して、テキストと説明がしっかりしたと感じるまでやる。画面で読むのとは全然違うよね…

AIの文章作成と似てるね。無駄が多い。

テレンス・タオがAIの数学的証明について言ったことは、純粋な数学だけじゃなくて共感できるよね。「文章はしばしば些細なことに長々と触れ、最も興味深く新しい議論の部分をあっさり通り過ぎるか、あるいは積極的に隠してしまうことが多い。」前から気づいてたけど、オンラインで誰かに反論する時に、誤字みたいな些細なことにこだわる人ほど、元の主張が強力だってこと。要するに、バイクシェッディングってやつだね。元の主張の説得力を示す最も明白な証拠は、最もアップボートされた返信がジョークやミームの時だよ。それが本当に、反応している人たちが他に言うことがないってことを示してる。白旗を掲げているようなもんだし、犬がひっくり返ってお腹を見せている感じ。

普通の数学の証明についても同じことが言えるよね。証明がなぜ成立するのかについては誰も話さないけど、どうやって成立するのかを何千ページもかけて説明するのは大好きだよね。

何日か前に誰かがこのポイントを持ち出してきたんだけど、AIの文章が読むのがすごくイライラする理由の一つ（もしかしたら一番の理由かも？）だとますます確信してる。AIは、重要なことも些細なことも同じように物語の重要性やドラマチックなトーンを与えちゃうから、真の理解を伝えることがほとんどできないんだよね。

彼の四色定理に対する見解が気になるな。コンピュータがいくつかのケースをチェックして、すべての地図がこれらのケースの一つに還元されるって説明できるけど、専門家じゃなくても言えることだよね。「適切に説明する」っていうのは、すごく曖昧な領域だと思う。近い将来、Leanで検証された結果の証明がすごく長くて、誰も「適切に説明」できなくなると思うけど、それを捨てるべきじゃないと思う。特異点の解決は、平中の有名な定理だよね。アビャンカールは、この定理の証明を本当に理解している人はいないと言ってた。彼とザリスキーは、完全に理解することなく論文を読み終えられなかったらしい。でもみんなこの定理が正しいって認めてるよ。

これに対する反論はチェスから来る。高レベルのエンジンは特定の手を「証明」するけど（数学的な意味ではない）、その「エンジンの手」は人間に説明するのがすごく難しいんだ。GM（グランドマスター）でさえ、何が良い手かは説明できても、その理由は説明できない。エンジンはGMを圧倒して、何が起こっているか誰も本当に理解していなくても、真実と見なされる。もし数学も同じだったら悪夢になるかも、どうだろう。特に反例に関しては、LLM（大規模言語モデル）の解決策は良さそうだ。無駄なことに人間が時間を浪費するのを防いでくれるから。証明に関してはもっと厄介だけど、形式的に検証されていれば証明は証明だと思う。帰属の問題もあるね（LLMから答えを引き出した人がクレジットをもらうべきか、そうだと思う）。これは非自明な認識論と科学理論の問題だと思う。

この経験則は失敗すると思う。今後のAIモデルにおける超人的な数学的推論と合成の組み合わせ、そしてスケーラブルな形式的検証インフラの急速な構築は、数学の指数的な進展を爆発的に引き起こすだろうし、まだ何も見ていないと思う。数学は人間の能力をかなり早く超えていくと思う（私たちの生きている間に、もっと急激にかもしれない）。多くの作業はAIにしか即座にアクセスできないように思えるし、すべてを人間に説明しようとするよりも、人間が特に理解することで利益を得られる部分に焦点を当てることになると思う。