数学市場

うちの工場でそんな良い定理ができるわけないじゃないですか。

週に何個か懸賞問題を解かせてようやくぎりぎり黒字です。

最先端の花形論文は全部大手企業製、うちみたいな弱小はゴミ定理かマイニングで食いつなぐしかありません。

うちも数年前までは上手くいってたんですよ。

一応GPUを二千台持ってますからそこそこのスペックのAIが動きますし、院で数学やってたような子も雇って工場で数学させていました。

別にうちの工場がしょぼいとか、そういうことじゃないんです。

2055年頃にはAIが人間よりも偉くなって、人間が数学をやるより人工知能に証明を探索させるほうがはやくなりました。

昔は手も足も出なかったミレニアム問題みたいな難問も、大手の証明AIが数年探索すれば解けてしまいます。

証明AIに記号的・形式的な証明を探索させて、コンピュータにその証明が正しいか検証させて、AIを使いつつ専門家が形式的証明を人間の言葉に翻訳する。

この体制が確立されると、数学の論文は指数関数的に増え始めました。

その後10年くらいは大手IT企業が数兆円規模のAIサーバーセンターを作って、各分野の専門家を集めて数学をやってたんです。

しかし、2063年にあのProofCoinが発行されたんですね。

ProofCoinは仮想通貨です。

他の仮想通貨と同じように、ブロックチェーンで改ざんを防いでいます。

このコインがすごいのは、ある数学の定理の証明を持っていることをゼロ知識証明できる点です。

例えば、あなたがある定理を形式的に証明したら、登録料を払ってその定理と、暗号化した証明をブロックチェーン上に登録します。

すると、検証者、つまり他のユーザーから証明を持っているかのゼロ知識証明を求められます。

検査をクリアすると定理の所有権が1000枚発行され、1000枚ともあなたのものになります。

実際にはサブチェーンで検証が行われるんですけど、ここでは割愛させてください。

さて、他の誰かが、あなたの定理を使えば別の定理を証明できることを発見したとしましょう。

しかし、その人はあなたの定理の証明を知りません。

そこで、ブロックチェーン上に登録されたあなたの定理を引用して証明を書きます。

この新しい定理がブロックチェーン上に登録されると、あなたは引用料のProofCoinをゲットします。

引用料は定額ではなく、価値のある定理はより多くの引用料がもらえます。

これによって、市場の参加する個々人が自身の利益を最大化することで数学が発展するように設計されているわけです。

場合によっては、引用の引用とかでも引用料がもらえます。

つまり、定理が不動産のような不労所得になったわけです。

引用料を稼ぐのは年単位の時間がかかるという問題があります。

特に、うちみたいに証明に莫大な電気代を使っている工場では、さっさと元をとらないと倒産してしまいます。

そこで、所有権の一部を投資家に売るんです。

1000枚のうち500枚を売れば、将来の引用料の半分は投資家に持っていかれてしまいますが、その代わりに目先のお金が手に入ります。

価値のある定理は将来の引用料が高いですから、市場で高く売れるんです。

あるいは、有名な定理を持っていることはステータスになるので価格が高騰することもあります。

つい先日、とある代数幾何の定理が話題になって価格が高騰してましたね、すぐにおさまってましたけど。

そもそもこのコインの仕組みの上手い所は、価値のある定理かどうかを市場に判断させるところなんですよ。

例えば、定理Aの証明が登録されたら、それを少し変形した同値命題を大量に登録して引用料を横取りしようとする人もいたんですけど、そういう定理は大体市場に良い定理だと判断されず、値段が上がりません。

すると、登録料はそこそこしますから、元が取れない仕組みになっているんです。

そういうイカサマをすべてアルゴリズムで検知するのは不可能ですが、市場はすべての情報を加味して判断する社会装置ですから、定理の社会背景まで考慮して価格を決定してくれます。

ちなみに、最近は定理の値段をAIに判断させてます。

始まったばかりのころは数学者の判断や下馬評がかなり力を持っていましたが、それもすべてAIに学習されてしまいました。

これはProofCoinの開発メンバーも想定していたことです。

市場で取引される定理の数は指数関数的に増えていきますから、その価格をすべて人間が決めるのは無理なことでした。

嫌な言い方をすれば、初期の市場価格を決定していた数学者たちは、AIが定理の価格を決める時代の下準備をさせられていたわけです。

もちろん現実世界に接地するのは人間の特権ですから、大局的な価格決定には人間社会が大きな役割を果たしていますが、

日々のデイトレードとか定理が登録された直後の価格の推移は全部AIがやっています。

最近は定理の価格推移をテクニカル分析して一儲けしようとする輩もいるようです。

ProofCoinの機能として、特定の定理の証明に懸賞金をかけることもできます。

例えば、ある企業が自社のプロダクトにバグが無いかを形式的に検証してほしい時や、巨大な証明を書いているチームがその一部を外注したい時に使います。

懸賞金問題は証明しても引用されることが少ないので利益が少ないですが、市場価格が変動するリスクなく利益が出るんです。

昔は個人で定理を探索している人がやっている印象でしたが、今はどこの工場も懸賞金問題を狙うのでレッドオーシャンです。

ProofCoinは基礎研究を金融商品にしました。

web3フォロワーたちが「市場の原理は計算資源を適切に分配する」という指導原理を掲げ、ProofCoinの整備に励んだ結果、数学の高等教育を受けていなくても、先進国の生まれでなくても、コンピュータか数学の才能さえあれば理論上誰でも最先端の研究に参加できる時代になりました。

ProofCoinの仕組みは先行者利益がとても大きいですから、一旦そういう流れができてしまうと誰も止めることはできません。

初期にはドイツのスタートアップがヴォイタ予想の証明に成功して、引用料で莫大な富を築いて世界屈指の大企業になりました。

つまり、他国に証明を明け渡すことは機会損失ですから、国はある種の国防の一環としてProofCoinに参加せざるを得ません。

各国はデータセンターを新設し、ありとあらゆる分野の専門家を招集してポートフォリオを作成し、各分野の定理の取得に乗り出しました。

ProofCoinが活性化するのは、数学の研究費が増額するのとほぼ同義です。

世界中の数学やそれに関連する分野で事実上予算が増えたことで、数学の発展のスピードは歴史上類を見ないものになりました。

最近では専門家の先生でも数学の発展のスピードに追い付くのが大変で、気を抜くと最先端の分野の定理をごっそり他国に持っていかれるので現場は大変だそうです。

うちみたいな民間も証明探索の工場を建てるようになりました。

証明探索のよいところは、既存のマイニング用の設備をほとんどそのまま流用できる点です。

独特なノウハウなんてほとんどいらず、AIを運用できる技術者と資産があればほとんど自動でできちゃいます。

基礎的な定理の証明をまとめたライブラリが無料で公開されたことで参入障壁が下がったという背景もあります。

投資家向けに計算資源を貸し出す人もいますね。

まあ国も補助金を出してくれますから、くいっぱぐれることはないと思ってました。

証明探索の挙動がおかしいという噂が流れだしたのは2年ほど前です。

どこの工場も年当たりの証明数が3%ほど落ちているんじゃないかと話題になり始めたんです。

急いで確認してみると、たしかにうちのAIも昨年比2~3%ほどスピードが落ちている。

探索アルゴリズムは各社が独自のものを使っていますから、みんな3%落ちているというのは奇妙な話です。

ドライバが更新したわけでもない、ネットワークが不安定なわけでもない、ハードウェア側の不調でも報酬スキームが変わったわけでもありません。

もしかしてウイルスが流通しているんじゃないかという話もありましたが、それらしい痕跡もありません。

知り合いが国立大学のサーバーで働いていたので聞いてみると、どうにも大学のAIでも同じようなことが起きていて原因を探していると教えてくれました。

この段階でようやく大事になりそうだと気づかされました。

四か月後、証明のスピードがさらに1%落ちていました。

同業者の間ではこの話題でもちきりになりました。

何か得体のしれないことが起きている。

原因を探せど探せど見つからない。

誰かがこれを「数学の危機の再来」と言い出しました。

うちの工場でも自社が持っている定理の証明をAIで自然言語に翻訳して傾向を調べたり、評価関数や探索アルゴリズムなどのパーツをあえて昔のものに戻したり、さまざまな実験をしましたが改善の兆しはありません。

そもそもAIによる証明は難しいうえに長大なものになっていて、博士課程を修了したような従業員でも証明の全容を理解するのには年単位でかかるかもしれないと言っていたので、うちのような会社では答えが出せる問題ではなさそうだと判断して匙をなげました。

その後、いくつかのチームが有力な仮説を打ち出しました。

某大学の研究室が出した仮説は、ProofCoin上に築かれた数学の体系は間違った方向に進んでいるのではないかというものです。

証明AIと価格決定AIが意図しない相互作用を起こしていて、なにか局所最適のような良くない状態に陥っているのではないか。

あるいは、評価関数とA*探索をベースに証明を探す古典的な手法には罠が潜んでいるのではないか。

某大手IT企業が出した仮説は、ノイマン型コンピュータの証明AIの相性が悪いのではないかというものでした。

これを打破するために、全く新しいアーキテクチャのコンピュータ開発や、人間の脳細胞を培養して活用する研究に投資することを発表しました。

様々な仮説がありましたが、どの仮説もある程度妥当そうで、それを踏まえた解決策が提示されました。

我々は不安ながらも、もしかすると技術の進歩がこの問題を解決してくれるかもしれないと楽観視し始めました。

SNSでもしばしば話題になり、様々な人が自分なりの意見を言って楽しむ定番の話題になりつつありました。

同業者は薄々この状況のまずさには気づいていました。

ゼロ知識証明しているので、証明があるということしか確認できない。

誰もProofCoin上の数学の全体像を知らず、何が起きているのか把握できない。

確認するには他社の証明を見るしかないですが、見せてもらえるわけがないので身動きが取れません。

しかし、それを大々的に言えば定理の価格やProofCoinの価格が下がりかねないので、楽観的に振る舞いました。

それは功を奏し、しばらく定理の価格が上昇しました。

投資家は供給が減るので価格が上がるだろうと考えて買いに走り出したのです。

定理の生産スピードは5%落ちていましたが、定理の価格は最大で20%ほど上がりました。

数学の危機はわが社の危機かと慌てた時期もありましたが、その年度の収支は大幅黒字となりとても安心していました。

一年後、形式証明を自然言語の証明に翻訳するAIの挙動がおかしくなり始めました。

どこの会社でも翻訳AIの性能は安定していたのですが、数学的に間違った証明を出力するようになったのです。

計算ミスなどではなく、証明の方向性を理解できていないような翻訳ばかりで、使い物にならなくなりました。

一つの定理の証明は最低でも1TBありますから、これを人間が読むのは現実的に不可能で、もはや何が起きているのか把握するすべはありません。

我々は証明AIと価格決定AIが市場でやり取りするのを見ていることしかできなくなったのです。

証明AIは20%ほど速度を落としていましたが、まだ稼働できています。

市場の価格は落ち着き始めていて、なかなか採算がとれないのでやりくりが大変です。

Proof-Theoretic Complexity of Arithmetic Thermodynamic Theory

In recent years, arithmetic thermodynamic theory has emerged as a central topic of investigation, with applications ranging from combinatorial entropy analysis, proof-theoretic heat kernel methods, and bar-recursive encoding of path integral, to speculative frameworks such as categorical fluctuation calculus, modal Boltzmann hierarchies, and ultrafinitary entropy. Despite its apparent breadth, the theory remains notoriously intractable. In particular, the proof of its Main Theorem has resisted formalization even in strong systems.

In this paper we demonstrate, working over the weak base theory RCA₀, that assuming the Main Theorem of arithmetic thermodynamic theory one can establish the consistency of full second-order arithmetic. We further show that any verification of this theory within a mechanized proof assistant requires computational resources proportional to the 2.7th power of the proof length, a complexity barrier that holds uniformly across standard systems.

From the standpoint of information-geometric proof theory, our results suggest that attempting to discover proofs of theorems strictly stronger than second-order arithmetic via Transformer-based algorithms will incur overwhelming computational costs. We conclude by arguing that, should mathematical development continue along this trajectory, the necessity of such immense verification resources for both proof construction and type-checking may render further progress intractable.