Formal target: Corpus.PaperDubner.dubner_conjecture

Every even number greater than 4208 is the sum of two twin primes.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 4208 n →
    Even.{0} n →
      Exists.{1} fun p =>
        Exists.{1} fun q =>
          And (Corpus.PaperDubner.IsTwinPrime p)
            (And (Corpus.PaperDubner.IsTwinPrime q) (Eq.{1} (HAdd.hAdd.{0, 0, 0} p q) n))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record