Conjectures.io

Number theory

Erdős 688 - part ii

In particular, is it true that ϵn=o(1)\epsilon_n = o(1)?

References

  • [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.

No one has attempted this yet.

Formal statement

Lean type

True ↔ Erdos688.epsilonFunction =o[Filter.atTop] fun n => 1

What you must prove

import FormalConjectures.ErdosProblems.«688»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos688.erdos_688.parts.ii" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/688.lean

Source type SHA-256
sha256:55896d56d50443407b4cb1e0e7992106639fe1beb10fe69832816d38a48ad0eb
Task id
fc-379fc029-parts-ii-cef3d6dae2-formalized-v1
Task commitment
sha256:58a91c90759cfa3036874d7a3899df184ace2cfc736bd546f5e9084e356271e7

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.