The set of primes is supernatural: a Lean formalization of the statement of the conjecture
本論文は、恒等関数、定数、および有限個の点演算（加法、乗法、指数演算）から構成される非定数関数は、すべての正の整数を素数に写すことはないという予想の、完全かつ機械的に検証されたLean 4による形式化を提示するものであり、これにより、当該の予想を自動推論システムにとって精密かつカーネル検証可能な対象へと変貌させている。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
無限に続く広大な図書室を想像してみてください。そこにあるすべての本は「数」です。この図書室には、「素数」と呼ばれる非常に特別で排他的なクラブが存在します。これらは、より小さな数を掛け合わせることで作ることができない数であり、2、3、5、7のように、算術における「不可分な原子」なのです。何世紀もの間、数学者たちは、これらの特別なクラブ・メンバーだけを吐き出すことができる、単一のシンプルで洗練されたレシピ——基本的な数学の道具で作られた機械——を作り出そうと試みてきました。彼らは、どんな数を入力しても、常に素数を出力するような機械を求めていたのです。
使用できるレシピの道具は、私たちが知る最も基本的なものに限られています。数の足し算、掛け算、そして累乗（2乗や3乗など）です。これらの道具を好きなように組み合わせることはできますが、割り算や平方根のような「凝ったもの」を使うことはできません。大きな問いはこうです。これらの単純な道具だけを使って、決して間違いを犯さない機械を作ることができるのでしょうか？ その機械は、終わりのない素数のリストを生成できるのでしょうか、それとも、いつかは躓いて素数ではない数を出力してしまうのでしょうか？ これは単なるゲームではありません。それは、素数がどのように構造化されているかという、数学の核心に触れる問題なのです。もしそのような機械が存在するならば、それは素数が単純で予測可能なパターンに従っていることを意味します。もし存在しないならば、素数が単純な公式では捉えきれないほど、荒々しく混沌とした、「超自然的」なものであることを意味します。
この論文は、その問いに対するデジタルな探偵小説です。著者であるアルノー・マイユー（Arnaud Mayeux）は、ある大胆な推測（予想）を提示した特定の数学論文を、「Lean」と呼ばれるコンピュータ言語へと翻訳しました。Leanを、数学の証明のあらゆるステップを厳格にチェックし、人間のミスや「おそらくこうなるだろう」といった曖昧さを一切許さない、超厳格な審判だと考えてください。この論文は、素数を生成する機械が存在するかどうかという謎を解いたわけではありません。代わりに、そのゲームのルールの完璧で壊れることのないデジタル・モデルを構築したのです。
この研究の主な成果は、「素数マシン」の仮説に関する理論全体が、コンピュータの中に正しくコーディングされたことです。元の論文にあるすべての定義、すべての例、そしてすべての数値表が、今やこのデジタル・ファイルの中に生きています。著者は、これら「自然関数」（足し算、掛け算、累乗から作られる機械の洗練された名称）の89種類もの異なる例を検証しました。それぞれの関数について、コンピュータは計算を行い、それらが最終的に素数以外の数を出力して失敗することを確認しました。例えば、ある関数は最初の6つの数については完璧に機能しましたが、7番目の数で壊れてしまいました。コンピュータは、人間が手作業で行えば何年もかかるような巨大な数値を、高度なデジタル証明書を用いて検証することで、これらの失敗を絶対的な確信を持って証明したのです。
しかし、この論文は、自身が「やっていないこと」についても明確に述べています。この論文は、素数マシンが不可能であることを証明したわけではありません。究極の答えを見つけたわけでもありません。そのような機械は存在しないという中心的な推測は、依然として未解決の問題としてコンピュータ・コードの中に残されており、いつか人間や人工知能が最終的な証明を行うのを待っています。この論文は実質的に、「ここに正確なルールブックがあり、これまで試してきたすべての機械がいかに失敗したかの証拠がある。しかし、最終的な判決はまだ出ていない」と言っているのです。
著者はまた、ゲームを少し拡張しました。「もし、階乗（その数より下のすべての数を掛け合わせたもの）や、クヌースの矢印（巨大な累乗を表現する方法）のような、もう少し多くの道具を加えたらどうなるだろうか？」と問いかけたのです。彼らはこれらの追加ツールを用いた、より大きなクラスの機械を構築し、さらに困難なバージョンの予想を提示しました。つまり、これらの「スーパー・ツール」を使っても、なお素数だけを作る機械を作ることはできないという予想です。この新しい予想も未解決であり、証明されてはいませんが、誰かが最終的に証明を見つけたときにコンピュータがチェックできるように記述されています。
要するに、この論文は大規模な翻訳と検証の作業です。素数の混沌とした性質に関する複雑な数学的アイデアを取り上げ、すべてのルールが機械によってチェックされるデジタルな金庫の中に封じ込めたのです。それは、テストされたすべての具体的な例において「素数マシン」が失敗することを裏付けていますが、そのような機械が理論的に可能であるかという究極の問いについては、未来への挑戦として残しています。素数は、私たちがそれらを閉じ込めようとする単純な公式に対して、依然として「超自然的」であり続け、抵抗しているようです。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。