Formal target: Corpus.PaperCatchUpConjecture.value_of_even_mul_succ_self_div_two

Let $T_N = \sum_{k=1}^{N} k = \frac{N(N+1)}{2}$.

Exact formal statement

∀ (N : Nat),
  Even.{0} (HDiv.hDiv.{0, 0, 0} (HMul.hMul.{0, 0, 0} N (HAdd.hAdd.{0, 0, 0} N 1)) 2) →
    Eq.{1} (Corpus.PaperCatchUpConjecture.value (Finset.Icc.{0} 1 N)) Corpus.PaperCatchUpConjecture.Outcome.draw

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record