erdős #728
Let and be sufficiently small. Are there infinitely many integers with and such thatand ?
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_728 :
answer(True) ↔
∀ᶠ ε : ℝ in 𝓝[>] 0, ∀ C > (0 : ℝ), ∀ C' > C,
∃ a b n : ℕ,
0 < n ∧
ε * n < a ∧
ε * n < b ∧
a ! * b ! ∣ n ! * (a + b - n)! ∧
a + b > n + C * log n ∧
a + b < n + C' * log nformal-conjectures/728.lean ↗status
solved