State of the Art

素数計算OSのための
厳密数値計算と
アルゴリズムの現在地

2010年代までの到達点を基準に、2020–2025年の重要論文を精査。
理論上のブレイクスルーよりも、「検証付き計算の実用化」と「既存手法の極限最適化」が進行した5年間であったことを報告する。

$\pi(10^{29})$

素数計数記録更新

$\tilde{O}(\sqrt{N})$

計算量の理論的下限

Coq/Why3

形式検証の統合

Verified

NN制御・ODEソルバ

B 分野別到達点と課題

※概念的な進展度合いを示すイメージ

以上の先行研究群は、以下の通り各分野において強力な到達点を与えてきた。

(i) Verified Numerics 個別問題ごとの
高精度検証

(ii) ODE/PDE 局所的な
安定性保証

(iii) Formal Verification 浮動小数点・制御器の
形式検証

(iv) Prime Algorithms $\pi(x)$ を高速評価する
素数カウンタ

しかし、解析的な素数公式を有限個の演算＋$\Sigma_1$型台帳で一括して閉じる「素数計算OS」は、いまだ構成されていない。

本研究は、この空白を埋める OS構造と finite-closure の枠組みを与え、素数計算を verified numerics および形式検証の文脈に直接接続する点に突破口がある。