Formal target: Corpus.WikipediaBrocardConjecture.brocard_conjecture

**Brocard's Conjecture** For every n ≥ 2, between the squares of the n-th and (n+1)-th primes, there are at least four prime numbers.

Exact formal statement

∀ (n : Nat),
  LE.le.{0} 1 n →
    LE.le.{0} 4
      (Finset.card.{0}
        (Finset.filter.{0} Nat.Prime
          (Finset.Ioo.{0} (HPow.hPow.{0, 0, 0} (Nat.nth Nat.Prime n) 2)
            (HPow.hPow.{0, 0, 0} (Nat.nth Nat.Prime (HAdd.hAdd.{0, 0, 0} n 1)) 2))))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record