Conjectures.io

Number theory

Erdős 950 - part i

Is it true that lim inf⁡f(n)=1\liminf f(n)=1?

References

  • [Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72.

No one has attempted this yet.

Formal statement

Lean type

True ↔ Filter.liminf (fun n => ↑(Erdos950.f n)) Filter.atTop = 1

What you must prove

import FormalConjectures.ErdosProblems.«950»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos950.erdos_950.parts.i" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/950.lean

Source type SHA-256
sha256:7e1118bf0c5700f2f1dd307c13776deb823bf13036d54f86c4baa8350ffbf1bf
Task id
fc-379fc029-parts-i-9926d95809-formalized-v1
Task commitment
sha256:3b92b5ae606c79cd01ce3b5d43ebbdd8b39e67a18899daa79c68bdd252d383d0

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.