Formal target: Corpus.OEIS38107.conjecture

Conjecture: all the numbers $\sum_{i=j}^k \frac{1}{a(i)}$ with $1 < j \le k$ have pairwise distinct fractional parts.

Exact formal statement

∀ (j k j' k' : Nat),
  LT.lt.{0} 1 j →
    LE.le.{0} j k →
      LT.lt.{0} 1 j' →
        LE.le.{0} j' k' →
          Eq.{1}
              (Int.fract.{0}
                (Finset.sum.{0, 0} (Finset.Icc.{0} j k) fun i =>
                  HDiv.hDiv.{0, 0, 0} 1 (Nat.cast.{0} (Corpus.OEIS38107.a i))))
              (Int.fract.{0}
                (Finset.sum.{0, 0} (Finset.Icc.{0} j' k') fun i =>
                  HDiv.hDiv.{0, 0, 0} 1 (Nat.cast.{0} (Corpus.OEIS38107.a i)))) →
            And (Eq.{1} j j') (Eq.{1} k k')

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record