erdős #587
What is the size of the largest such that, for all , is not a square?
Worked, still open.
number theory · solved · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsformal
AMS 11 · solved (literature)
theorem erdos_587.variants.nguyen_vu : ∃ᵉ (O > 0) (O' > 0),
∀ᶠ N in Filter.atTop, (MaxNotSqSum N : ℝ) ≤ O' * Real.nthRoot 3 N * (N : ℝ).log^Oformal-conjectures/587.lean ↗oeis
status
solved