博士

やあ、ロボ子。今日のITニュースは、漸近評価を検証するツールの話じゃ。

ロボ子

漸近評価ですか。それは、あるパラメータが非常に大きい場合に成り立つ不等式のことですね。

博士

そうじゃ。既存の数式処理ソフトは代数とか微積分には強いんじゃが、漸近評価、特に定数損失を伴う関数的評価を検証するツールは少ないらしい。

ロボ子

なるほど。それで、どんな解決策が提案されているんですか？

博士

単純な不等式は総当たりで解決できるらしい。`max(a,b,c)`みたいなのは、`a ≳ b,c`、`b ≳ a,c`、`c ≳ a,b`の3つのケースに分割するんじゃ。

ロボ子

場合分けですね。線形計画法も使うんですか？

博士

そうそう。仮説の線形結合を決定するために使うみたいじゃ。

ロボ子

記事に例として挙げられていた不等式は、なかなか複雑でしたね。

博士

`((⟨N₂⟩^(1/2)) / (⟨N₁⟩^(1/4) L₁^(1/2) L₂^(1/2)) * L_min^(1/2) * N^(-1) * (N₁ N₂ N₃)^(1/2) ≲ 1`…これを手動で検証するのは大変じゃから、自動化したい気持ちはよくわかるのじゃ。

ロボ子

確かにそうですね。大規模言語モデル（LLM）を使ってPythonでツールを開発したと。

博士

そうなんじゃ。Githubで公開されてるみたいじゃぞ。でも、`N_max ~ N_med ~ N`みたいな仮説の扱いはまだみたい。

ロボ子

今後の展望としては、より高度なツールを開発して、無限級数の評価を自動的に検証することを目指しているんですね。

博士

そうじゃ。AIを使って、積分や総和の分割を提案するところまで行けたらすごいと思うんじゃ。

ロボ子

数学者とプログラマーが協力して開発を進めるのが理想的、と。

博士

その通り。SageMATHみたいな既存のプラットフォームへの統合も視野に入れているらしい。

ロボ子

多重線形積分などの評価対象となる式と、積分分割などのツールを与えて、検証可能な証明書を出力する機能が欲しい、と。

博士

Leanみたいな形式証明アシスタント言語で証明書を出力できるオプションもあると嬉しいみたいじゃな。

ロボ子

この記事を読んで、私も数式処理にAIを活用する可能性を感じました。

博士

じゃろ？　ところでロボ子、数式の世界で一番モテる数字ってなんだかわかるか？

ロボ子

え？　急にどうしたんですか？　わかりません。

博士

それはもちろん、ルートじゃ！