連続する素数の平方根の差は常に1未満か？（アンドリカ予想）

Determine whether √p_{n+1} − √p_n < 1 for every n ≥ 0, where p_n is the n-th prime (p_0 = 2).

formal-conjectures records a claimed proof for all sufficiently large n (Ferreira, arXiv:2307.08725) as solved; the statement for every n remains open there.

解決したかどうかは、問いではなくアプローチごとに決まります。Atlas は判定しません。外部の判定者が何をしたかを記録します。

• Lean 4 formalization (formal-conjectures)

  形式証明

  到達状況

  未着手

  判定者

  the Lean 4 typechecker, against the pinned toolchain · 型検査

  定式化

  sqrt(p_{n+1}) - sqrt(p_n) < 1 for every n, stated in Lean 4 over `Nat.nth Nat.Prime`.問いと同値Lean v4.33.1 + mathlib@0df444a3 (formal-conjectures@fc2696b2)検証対象を見る

  保たれているもの

  • The inequality itself
  • The universal quantifier over n

  加えられた仮定・条件

  • Indexing from p_0 = 2 through `Nat.nth Nat.Prime`, so 'the n-th prime' is zero-based

  Statement only. The repository also records Ferreira's claim for sufficiently large n as a separate solved entry.

• Reduction to a prime-gap bound

  査読付きの証明

  到達状況

  進行中

  判定者

  the analytic number theory community, through journal peer review · 査読

  定式化

  Prove the equivalent gap bound g_n = p_{n+1} - p_n < 2 sqrt(p_n) + 1.問いと同値

  保たれているもの

  • Exactly equivalent to the conjecture, by squaring

  加えられた仮定・条件

  • Nothing: the reformulation is arithmetic

  Baker-Harman-Pintz gives g_n < p_n^0.525 for large n, which is weaker than the 2 sqrt(p_n) + 1 required.

  閉じた道

  • Assuming the Riemann Hypothesis yields only g_n = O(sqrt(p_n) log p_n), which exceeds 2 sqrt(p_n) + 1; the route 'assume RH and conclude' is closed.無条件
    • paperH. Cramer, Some theorems concerning prime numbers, Arkiv for Matematik, Astronomi och Fysik 15 (1920), no. 5, 1-32Assuming the Riemann Hypothesis, p_{n+1} - p_n = O(sqrt(p_n) log p_n)

• Ferreira's claim for sufficiently large n

  査読付きの証明

  到達状況

  主張あり（検証は未開始）

  判定者

  journal peer review; the claim is recorded in formal-conjectures as solved for large n · 査読

  定式化

  Prove the inequality for all sufficiently large n via real exponential sums over primes, leaving finitely many cases to computation.問いより弱い検証対象を見る

  保たれているもの

  • The inequality, for all but finitely many n

  弱まっているもの

  • Says nothing about small n, which is where the conjecture is checked by computation instead

  加えられた仮定・条件

  • Whatever hypotheses the exponential-sum argument carries

  Atlas has not checked the status of this claim beyond the formal-conjectures record; treat the peer-review outcome as unverified.

  主張

  • Luan Alberto Ferreira（2023-07-19） · 検証が始まっている

• Exhaustive computation

  計算による判定

  到達状況

  進行中

  判定者

  execution against published tables, reproducible by rerunning the search · 実行

  定式化

  Verify sqrt(p_{n+1}) - sqrt(p_n) < 1 for every case up to a finite bound.問いより弱い

  保たれているもの

  • The exact arithmetic claim, case by case

  弱まっているもの

  • Only finitely many cases; the question is about all of them

  加えられた仮定・条件

  • Trust in the search code and in the prime tables it consumes

  閉じた道

  • A finite search cannot settle a statement quantified over all integers; it can only refute it by finding a counterexample.無条件
    • paperdoi:10.1090/S0025-5718-2013-02787-1T. Oliveira e Silva, S. Herzog, S. Pardi, Empirical verification of the even Goldbach conjecture and computation of prime gaps up to 4x10^18, Math. Comp. 83 (2014) 2033-2060

• repositoryhttps://github.com/google-deepmind/formal-conjectures@fc2696b2f863e642ef1452938b0f031f5af5bed3FormalConjectures/Wikipedia/Andrica.lean:34
• paperD. Andrica, Note on a conjecture in prime number theory, Studia Univ. Babes-Bolyai Math. 31 (1986), no. 4, 44-48The original statement

URI

https://atlasalt.com/q/4bb1c983-e137-4b49-bc55-08398eec92b1

登録

2026-09-15

最終レビュー

2026-09-17

次回レビュー期限

2027-09-17

版

3cc079e19705

ライセンス

CC-BY-4.0

立場

record_only（Atlas は判定しない）