Formal target: Corpus.OEIS64313.conjecture

"Usually (perhaps always?) $\lfloor n^2 / (4\pi) - \pi / 12 \rfloor$ for a polygon of circumference $n$.

Exact formal statement

∀ (n : Nat),
  LE.le.{0} 3 n →
    Eq.{1} (Corpus.OEIS64313.a n)
      (Int.floor.{0}
          (HSub.hSub.{0, 0, 0}
            (HDiv.hDiv.{0, 0, 0} (HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) 2) (HMul.hMul.{0, 0, 0} 4 Real.pi))
            (HDiv.hDiv.{0, 0, 0} Real.pi 12))).toNat

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record