コンピュータサイエンスは数学の「問い」を変えた
素数は無限にある。ユークリッドが証明した。それで終わりだ。
だが2002年、別の問いが立てられた。素数かどうかを、入力の桁数に対して多項式時間で判定できるか。AKSアルゴリズムが答えを出した。命題は何も覆っていない。同じ対象が、別の解像度で管理されるようになっただけだ。
コンピュータサイエンスが数学に何をしたかと問われると、「証明がAIに置き換わる」とか「数学が計算になる」という答えが返ってくる。どちらも正確でない。というより、問いのたて方が粗い。起きているのは全体の革命ではなく、数学の三つの層それぞれへの介入だ。問題の形、証明の検証装置、知識を生産する制度。入口が違えば、作用の仕方も違う。
存在証明が得られれば、数学の仕事はひとまず終わる。そういう領域は多い。だが計算可能性の問いはそこで始まる。解けることと、まともな時間で解けることは違う。コンピュータサイエンスはその「後者」を、しつこく理論に持ち込んだ。
ただし、これが有効なのは離散的で符号化でき、入力として与えられる範囲においてだ。数学全体をこの言葉で覆い始めると、それはたいてい宣伝になる。
証明の話も同じ構図で読める。proof assistantが変えたのは、証明の書き方ではない。証明の存在形態だ。人間への説得の文章が、機械の検査可能な対象へと移されつつある。
ここで混同しやすいのは、厳密性と理解可能性が別物だという点だ。形式化は推論の局所的な正しさを強く保証する。どこで何を使ったかを細かく追える。だが、なぜその発想が重要かは自動的に与えてくれない。証明が正しいことと、証明がわかることは、別の問題だ。
Feit–Thompson定理もKepler予想も機械検証された。それでも信頼は無条件ではない。カーネル、基礎理論、実装、コンパイラ——形式化にも信頼の根拠はある。形式化とは無謬性の到来ではなく、誤りの居場所を変える技術だ。曖昧さに拡散していた誤差を、より局所的で監査可能な場所へ押し込む。消すのではなく、見つけやすい棚に並べ替える。
機械学習は反例探索や候補命題の選別に有効だ。だが観測されたパターンがそのまま定理になるわけではない。機械学習が与えるのは証明ではなく、探索のバイアスだ。どの表現の上でパターンが見えているかを明示しなければ、発見は理論にならず、面白い可視化で終わる。
三つ目の層は急に人間くさくなる。形式化基盤、計算資源、共同開発の作法——そうしたものへのアクセスは均等ではない。数学は純粋精神の営みだと言われる。だが実際には、サーバ代も人件費も教育コストも効いてくる。
技術は中立な道具としてだけ存在するのではない。形式化しやすい主題、データ化しやすい対象が前に出る。使いやすいものが標準になり、標準が評価を呼び、評価が人を集める。この循環が、数学の風景を少しずつ変える。
コンピュータサイエンスは数学を外から置き換えるのではない。計算に露出した部分で、問題の粒度が刻み直され、証明の検証様式が作り替えられ、知識を運ぶインフラが再設計される。派手な革命ではなく、接続面の作り替えだ。だが大きな変化は、たいてい全体の名前を変える前に、こうした地味な接続面から始まる。