Squarefree numbers in short intervals: explicit and formalized

数直線という、地平線へと続く果てしなく輝くハイウェイを想像してみてください。この道の上には、「平方自由（squarefree）」と呼ばれる数字が存在します。これらは、決して重複することのないユニークな構成要素から作られています。例えば、同じ色のパーツが二度と現れないレゴブロックのようなものです。それらを使って、完璧な正方形のタワーを建てることはできません。数学者たちは、このハイウェイの非常に長い区間を見渡せば、これらの特別な数字が予測可能なリズム、つまりおよそ10カ所につき6カ所の割合で現れることを古くから知っています。しかし、ズームインして、非常に短く小さな区間を見たとしたらどうなるでしょうか？平方自由数は依然としてそのリズムを保っているのでしょうか、それとも混沌として予測不能になるのでしょうか？これが「短い区間における平方自由数」という問題です。これは、整数の背後に隠されたパターンを研究する数学の一分野である、数論におけるパズルです。この問題を解くことは、一つのレンガが巨大な壁にどのように組み込まれているかを理解することのように、数学の根本的な構造を理解することに繋がります。

本論文において、マヤンク・パンデー（Mayank Pandey）は、既知の数学的結果を取り上げ、それを「明示的（explicit）」かつ「形式化（formalized）」することで、このパズルに取り組んでいます。以前は、これらの数字が短い区間においても良好に振る舞うことを証明する結果が存在していましたが、それは「ニルシーケンス（nilsequences）」やグリーンとタオの研究を含む、強力で複雑なツール（いわばブラックボックス）に依存していました。そのブラックボックスは、「答えが存在すること」は教えてくれますが、「計算に必要な具体的な数値」までは与えてくれなかったのです。パンデーの研究は、そのブラックボックスを分解し、すべての歯車やバネを測定し、その正確な寸法を書き記すような作業です。彼は、もし出発点 $X$ を少なくとも $e^{1027/\varepsilon^2}$ （驚異的に大きな数）以上とし、長さ $H = X^{1/5 - 2/90935 + \varepsilon}$ の区間を見るならば、見つかる平方自由数の数は、期待される量に非常に近くなることを証明しています。具体的には、実際のカウントと期待されるカウントの差は、必ず $10450 \varepsilon H X^{-\varepsilon/1025}$ 以下であることが保証されます。これは、区間が短すぎず、かつ出発する数字が十分に大きい場合に限り、具体的かつ計算可能な約束となります。

これを達成するために、パンデーは「誤差項（error terms）」という、カウントにおける小さな揺らぎが支配する困難な景観をナビゲートしなければなりませんでした。彼は問題を異なるゾーンに分解しました。あるゾーンでは、差分を繰り返し引き算して凹凸を滑らかにするという標準的な手法を用いて、揺らぎを容易に制御できます。しかし、より困難な別のゾーンでは、揺らぎは頑固です。元の論文では、これらの頑固なゾーンは前述の「ブラックボックス」ツールによって処理されていました。しかし、パンデーは自ら泥臭い作業を行うことを決意しました。彼は数学的な式を、絡まった紐の結び目のように扱いました。魔法のトリックを使って結び目を解く代わりに、彼は特定の糸を慎重に引くこと（「ヴァン・デル・コルペン（van der Corput）の差分法」と呼ばれる手法）で、結び目を緩めていったのです。彼は、たとえ紐が乱雑に見えたとしても、パターンを台無しにするような形で引っかかることはないと示しました。問題をより小さなケースに分割し、一つずつ検証することで、彼は「揺らぎ」が自身の設定した範囲内において無視できるほど小さいことを証明しました。

また、本論文は明快さを期すために、説明を簡略化するという意図的な選択を行っています。コンピュータコード（Lean 4によって形式化されたもの）には、より最適化され精密な数学的表現が含まれていますが、記述されたノートは、より理解しやすい「大まかな」バージョンを提示しています。これは、学生に街のすべての路地まで記された衛星写真を与えるのではなく、主要なルートを教えるために簡略化された地図を見せるようなものです。著者は、この簡略化によって最終的な指数がわずかに弱まるものの、核心となる発見は揺るぎないものであると述べています。すなわち、平方自由数のパターンは、非常に短い区間においても成立しており、今や私たちはそれを証明するための正確な数値を手に入れたということです。この研究は、単なる推測やシミュレーションではなく、厳密な証明であり、私たちが望んだ通り、数学的構造が顕微鏡で覗き込んでも秩序あるものであることを裏付けています。