連続する素数の平方の間には、素数が少なくとも4つあるか？（ブロカール予想）

Let pₙ be the n-th prime. Determine whether for every n ≥ 2 there are at least four primes strictly between pₙ² and pₙ₊₁².

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

• Lean 4 formalization (formal-conjectures)

  形式証明

  到達状況

  未着手

  判定者

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

  定式化

  For every n >= 2 there are at least four primes between p_n^2 and p_{n+1}^2, stated in Lean 4.問いと同値Lean v4.33.1 + mathlib@0df444a3 (formal-conjectures@fc2696b2)検証対象を見る

  保たれているもの

  • The count of at least four primes
  • Consecutive primes p_n, p_{n+1}

  加えられた仮定・条件

  • An explicit lower bound n >= 2

  Statement only.

• Derivation from a stronger prime-gap conjecture

  査読付きの証明

  到達状況

  未着手

  判定者

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

  定式化

  Derive the four-prime count from Oppermann's conjecture, from Cramer's conjecture, or from Legendre's conjecture applied twice.問いより弱い

  保たれているもの

  • The exact count of four primes follows once the stronger statement is available

  弱まっているもの

  • Settles nothing on its own: it moves the question onto an equally open one

  加えられた仮定・条件

  • Whichever stronger conjecture is assumed

  閉じた道

  • Every known derivation starts from a conjecture that is itself open (Oppermann, Cramer, or Legendre), so this route cannot close the question unaided.無条件
    • repositoryhttps://github.com/google-deepmind/formal-conjectures@fc2696b2f863e642ef1452938b0f031f5af5bed3FormalConjectures/Wikipedia/Oppermann.lean:61 — Oppermann implies Brocard, proved in Lean; the implying conjectures are themselves open

• Exhaustive computation

  計算による判定

  到達状況

  進行中

  判定者

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

  定式化

  Verify at least four primes between consecutive prime squares 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

• Sieve methods

  閉じた道（障壁）

  到達状況

  この道では到達できないと証明済み

  判定者

  none: the obstruction is a published theorem, not a decision procedure · 引用

  差分（このアプローチが問いの何を保ち、何を弱めるか）はまだ書かれていません。人類審査で書きます。

  閉じた道

  • A sieve alone cannot detect primes (Selberg's parity problem), so sieve methods reach almost-primes rather than a prescribed count of primes in a short interval.無条件
    • talkA. Selberg, On elementary methods in prime number theory and their limitations, Den 11te Skandinaviske Matematikerkongress, Trondheim (1949), 13-22The parity obstruction: a sieve cannot distinguish an odd from an even number of prime factors

• repositoryhttps://github.com/google-deepmind/formal-conjectures@fc2696b2f863e642ef1452938b0f031f5af5bed3FormalConjectures/Wikipedia/BrocardConjecture.lean:37
• paperH. Brocard, note in L'Intermediaire des Mathematiciens 11 (1904) 190Attribution of the conjecture; Atlas has not consulted the original note, so the page reference is unverified

URI

https://atlasalt.com/q/1a00019b-6d21-40bf-ab8c-7a7a9f95f61f

登録

2026-09-14

最終レビュー

2026-09-17

次回レビュー期限

2027-09-17

版

d1cadea8959f

ライセンス

CC-BY-4.0

立場

record_only（Atlas は判定しない）