FormalConjectures.OEIS.«64313»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Integer part of area of a regular polygon with $n$ sides each of length 1

The area of a regular $n$-gon with side length 1 is given by $\frac{n}{4} \cot(\pi / n) = \frac{n}{4 \tan(\pi / n)}$.

References:

A064313

namespace OeisA64313

The exact area of a regular $n$-gon with side length 1.

noncomputable def area (n : ℕ) : ℝ :=
  (n : ℝ) / (4 * Real.tan (Real.pi / (n : ℝ)))

Integer part of area of a regular polygon with $n$ sides each of length 1.

noncomputable def a (n : ℕ) : ℕ :=
  (Int.floor (area n)).toNat



@[category test, AMS 51]
theorem a_1 : a 1 = 0 := by⊢ a 1 = 0
  dsimp [a, area]⊢ ⌊↑1 / (4 * Real.tan (Real.pi / ↑1))⌋.toNat = 0
  have h : Real.pi / ((1 : ℕ) : ℝ) = Real.pi := by⊢ a 1 = 0h:Real.pi / ↑1 = Real.pi⊢ ⌊↑1 / (4 * Real.tan (Real.pi / ↑1))⌋.toNat = 0 norm_numh:Real.pi / ↑1 = Real.pi⊢ ⌊↑1 / (4 * Real.tan (Real.pi / ↑1))⌋.toNat = 0h:Real.pi / ↑1 = Real.pi⊢ ⌊↑1 / (4 * Real.tan (Real.pi / ↑1))⌋.toNat = 0
  rw [h,h:Real.pi / ↑1 = Real.pi⊢ ⌊↑1 / (4 * Real.tan Real.pi)⌋.toNat = 0h:Real.pi / ↑1 = Real.pi⊢ ⌊↑1 / (4 * 0)⌋.toNat = 0 Real.tan_pih:Real.pi / ↑1 = Real.pi⊢ ⌊↑1 / (4 * 0)⌋.toNat = 0h:Real.pi / ↑1 = Real.pi⊢ ⌊↑1 / (4 * 0)⌋.toNat = 0]h:Real.pi / ↑1 = Real.pi⊢ ⌊↑1 / (4 * 0)⌋.toNat = 0
  norm_numAll goals completed! 🐙



@[category test, AMS 51]
theorem a_2 : a 2 = 0 := by⊢ a 2 = 0
  dsimp [a, area]⊢ ⌊2 / (4 * Real.tan (Real.pi / 2))⌋.toNat = 0
  rw [Real.tan_pi_div_two⊢ ⌊2 / (4 * 0)⌋.toNat = 0⊢ ⌊2 / (4 * 0)⌋.toNat = 0]⊢ ⌊2 / (4 * 0)⌋.toNat = 0
  norm_numAll goals completed! 🐙



@[category test, AMS 51]
theorem a_3 : a 3 = 0 := by⊢ a 3 = 0
  dsimp [a, area]⊢ ⌊3 / (4 * Real.tan (Real.pi / 3))⌋.toNat = 0
  rw [Real.tan_pi_div_three⊢ ⌊3 / (4 * √3)⌋.toNat = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0]⊢ ⌊3 / (4 * √3)⌋.toNat = 0
  have hf : Int.floor ((3 : ℝ) / (4 * Real.sqrt 3)) = 0 := by⊢ a 3 = 0hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0
    rw [Int.floor_eq_iff⊢ ↑0 ≤ 3 / (4 * √3) ∧ 3 / (4 * √3) < ↑0 + 1⊢ ↑0 ≤ 3 / (4 * √3) ∧ 3 / (4 * √3) < ↑0 + 1hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0]⊢ ↑0 ≤ 3 / (4 * √3) ∧ 3 / (4 * √3) < ↑0 + 1hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0
    norm_num⊢ 0 ≤ 3 / (4 * √3) ∧ 3 / (4 * √3) < 1hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0
    have h_sqrt : (1 : ℝ) < Real.sqrt 3 := Real.lt_sqrt_of_sq_lt (by⊢ 1 ^ 2 < 3h_sqrt:1 < √3⊢ 0 ≤ 3 / (4 * √3) ∧ 3 / (4 * √3) < 1hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0 norm_numAll goals completed! 🐙h_sqrt:1 < √3⊢ 0 ≤ 3 / (4 * √3) ∧ 3 / (4 * √3) < 1hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0)h_sqrt:1 < √3⊢ 0 ≤ 3 / (4 * √3) ∧ 3 / (4 * √3) < 1hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0
    constructorlefth_sqrt:1 < √3⊢ 0 ≤ 3 / (4 * √3)righth_sqrt:1 < √3⊢ 3 / (4 * √3) < 1hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0
    ·lefth_sqrt:1 < √3⊢ 0 ≤ 3 / (4 * √3)hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0 positivityAll goals completed! 🐙hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0
    ·righth_sqrt:1 < √3⊢ 3 / (4 * √3) < 1hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0 have : (3 : ℝ) < 4 * Real.sqrt 3 := by⊢ a 3 = 0righth_sqrt:1 < √3this:3 < 4 * √3⊢ 3 / (4 * √3) < 1hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0 linarithrighth_sqrt:1 < √3this:3 < 4 * √3⊢ 3 / (4 * √3) < 1hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0righth_sqrt:1 < √3this:3 < 4 * √3⊢ 3 / (4 * √3) < 1hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0
      exact (div_lt_one (byh_sqrt:1 < √3this:3 < 4 * √3⊢ 0 < 4 * √3hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0 positivityAll goals completed! 🐙hf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0)).mpr thishf:⌊3 / (4 * √3)⌋ = 0⊢ ⌊3 / (4 * √3)⌋.toNat = 0
  rw [hfhf:⌊3 / (4 * √3)⌋ = 0⊢ Int.toNat 0 = 0hf:⌊3 / (4 * √3)⌋ = 0⊢ Int.toNat 0 = 0]hf:⌊3 / (4 * √3)⌋ = 0⊢ Int.toNat 0 = 0
  rflAll goals completed! 🐙



@[category test, AMS 51]
theorem a_4 : a 4 = 1 := by⊢ a 4 = 1
  dsimp [a, area]⊢ ⌊4 / (4 * Real.tan (Real.pi / 4))⌋.toNat = 1
  have h : (4 : ℝ) / (4 * Real.tan (Real.pi / 4)) = 1 := by⊢ a 4 = 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ⌊4 / (4 * Real.tan (Real.pi / 4))⌋.toNat = 1
    rw [Real.tan_pi_div_four⊢ 4 / (4 * 1) = 1⊢ 4 / (4 * 1) = 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ⌊4 / (4 * Real.tan (Real.pi / 4))⌋.toNat = 1]⊢ 4 / (4 * 1) = 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ⌊4 / (4 * Real.tan (Real.pi / 4))⌋.toNat = 1
    ringh:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ⌊4 / (4 * Real.tan (Real.pi / 4))⌋.toNat = 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ⌊4 / (4 * Real.tan (Real.pi / 4))⌋.toNat = 1
  rw [hh:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ⌊1⌋.toNat = 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ⌊1⌋.toNat = 1]h:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ⌊1⌋.toNat = 1
  have hf : Int.floor (1 : ℝ) = 1 := by⊢ a 4 = 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1hf:⌊1⌋ = 1⊢ ⌊1⌋.toNat = 1
    rw [Int.floor_eq_iffh:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ↑1 ≤ 1 ∧ 1 < ↑1 + 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ↑1 ≤ 1 ∧ 1 < ↑1 + 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1hf:⌊1⌋ = 1⊢ ⌊1⌋.toNat = 1]h:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ↑1 ≤ 1 ∧ 1 < ↑1 + 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1hf:⌊1⌋ = 1⊢ ⌊1⌋.toNat = 1
    constructorlefth:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ↑1 ≤ 1righth:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ 1 < ↑1 + 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1hf:⌊1⌋ = 1⊢ ⌊1⌋.toNat = 1 <;>lefth:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ ↑1 ≤ 1righth:4 / (4 * Real.tan (Real.pi / 4)) = 1⊢ 1 < ↑1 + 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1hf:⌊1⌋ = 1⊢ ⌊1⌋.toNat = 1 norm_numh:4 / (4 * Real.tan (Real.pi / 4)) = 1hf:⌊1⌋ = 1⊢ ⌊1⌋.toNat = 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1hf:⌊1⌋ = 1⊢ ⌊1⌋.toNat = 1
  rw [hfh:4 / (4 * Real.tan (Real.pi / 4)) = 1hf:⌊1⌋ = 1⊢ Int.toNat 1 = 1h:4 / (4 * Real.tan (Real.pi / 4)) = 1hf:⌊1⌋ = 1⊢ Int.toNat 1 = 1]h:4 / (4 * Real.tan (Real.pi / 4)) = 1hf:⌊1⌋ = 1⊢ Int.toNat 1 = 1
  rflAll goals completed! 🐙



@[category test, AMS 51]
theorem a_6 : a 6 = 2 := by⊢ a 6 = 2
  dsimp [a, area]⊢ ⌊6 / (4 * Real.tan (Real.pi / 6))⌋.toNat = 2
  rw [Real.tan_pi_div_six⊢ ⌊6 / (4 * (1 / √3))⌋.toNat = 2⊢ ⌊6 / (4 * (1 / √3))⌋.toNat = 2]⊢ ⌊6 / (4 * (1 / √3))⌋.toNat = 2
  have h_eq : (6 : ℝ) / (4 * (1 / Real.sqrt 3)) = 3 * Real.sqrt 3 / 2 := by⊢ a 6 = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ⌊6 / (4 * (1 / √3))⌋.toNat = 2
    have : 0 < Real.sqrt 3 := Real.sqrt_pos.mpr (by⊢ 0 < 3this:0 < √3⊢ 6 / (4 * (1 / √3)) = 3 * √3 / 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ⌊6 / (4 * (1 / √3))⌋.toNat = 2 norm_numAll goals completed! 🐙this:0 < √3⊢ 6 / (4 * (1 / √3)) = 3 * √3 / 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ⌊6 / (4 * (1 / √3))⌋.toNat = 2)this:0 < √3⊢ 6 / (4 * (1 / √3)) = 3 * √3 / 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ⌊6 / (4 * (1 / √3))⌋.toNat = 2
    field_simpthis:0 < √3⊢ 6 * 2 = 4 * 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ⌊6 / (4 * (1 / √3))⌋.toNat = 2
    ringh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ⌊6 / (4 * (1 / √3))⌋.toNat = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ⌊6 / (4 * (1 / √3))⌋.toNat = 2
  rw [h_eqh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ⌊3 * √3 / 2⌋.toNat = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ⌊3 * √3 / 2⌋.toNat = 2]h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ⌊3 * √3 / 2⌋.toNat = 2
  have hf : Int.floor (3 * Real.sqrt 3 / 2) = 2 := by⊢ a 6 = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2
    rw [Int.floor_eq_iffh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ↑2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < ↑2 + 1h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ↑2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < ↑2 + 1h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2]h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ ↑2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < ↑2 + 1h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2
    norm_numh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2
    have hle : (4 / 3 : ℝ) ≤ Real.sqrt 3 := by⊢ a 6 = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2
      have : (4 / 3 : ℝ) ^ 2 ≤ 3 := by⊢ a 6 = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2this:(4 / 3) ^ 2 ≤ 3⊢ 4 / 3 ≤ √3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2 norm_numh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2this:(4 / 3) ^ 2 ≤ 3⊢ 4 / 3 ≤ √3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2this:(4 / 3) ^ 2 ≤ 3⊢ 4 / 3 ≤ √3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2
      exact (Real.le_sqrt (byh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2this:(4 / 3) ^ 2 ≤ 3⊢ 0 ≤ 4 / 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2 norm_numAll goals completed! 🐙h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2) (byh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2this:(4 / 3) ^ 2 ≤ 3⊢ 0 ≤ 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2 norm_numAll goals completed! 🐙h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2)).mpr thish_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2
    have hlt : Real.sqrt 3 < 2 := by⊢ a 6 = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2
      have : (3 : ℝ) < 2 ^ 2 := by⊢ a 6 = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3this:3 < 2 ^ 2⊢ √3 < 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2 norm_numh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3this:3 < 2 ^ 2⊢ √3 < 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3this:3 < 2 ^ 2⊢ √3 < 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2
      exact (Real.sqrt_lt (byh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3this:3 < 2 ^ 2⊢ 0 ≤ 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2 norm_numAll goals completed! 🐙h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2) (byh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3this:3 < 2 ^ 2⊢ 0 ≤ 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2 norm_numAll goals completed! 🐙h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2)).mpr thish_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 2 ≤ 3 * √3 / 2 ∧ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2
    constructorlefth_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 2 ≤ 3 * √3 / 2righth_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2 <;>lefth_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 2 ≤ 3 * √3 / 2righth_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hle:4 / 3 ≤ √3hlt:√3 < 2⊢ 3 * √3 / 2 < 3h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2 linarithh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ ⌊3 * √3 / 2⌋.toNat = 2
  rw [hfh_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ Int.toNat 2 = 2h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ Int.toNat 2 = 2]h_eq:6 / (4 * (1 / √3)) = 3 * √3 / 2hf:⌊3 * √3 / 2⌋ = 2⊢ Int.toNat 2 = 2
  rflAll goals completed! 🐙

"Usually (perhaps always?) $\lfloor n^2 / (4\pi) - \pi / 12 \rfloor$ for a polygon of circumference $n$. Note that the area of a circle with circumference $C$ is $C^2 / (4\pi)$."

@[category research open, AMS 51]
theorem conjecture (n : ℕ) (hn : 3 ≤ n) :
    a n = (Int.floor ((n : ℝ) ^ 2 / (4 * Real.pi) - Real.pi / 12)).toNat := byn:ℕhn:3 ≤ n⊢ a n = ⌊↑n ^ 2 / (4 * Real.pi) - Real.pi / 12⌋.toNat
  sorryAll goals completed! 🐙

end OeisA64313