Formal target: Corpus.WikipediaLemoine.lemoine_conjecture

For all odd integers $n ≥ 7$ there are prime numbers $p,q$ such that $n = p+2q$.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 6 n →
    Odd.{0} n →
      Exists.{1} fun p =>
        Exists.{1} fun q =>
          And (Nat.Prime p) (And (Nat.Prime q) (Eq.{1} (HAdd.hAdd.{0, 0, 0} p (HMul.hMul.{0, 0, 0} 2 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