Number theory

Erdős 1203

Prove that

F(n)\to \infty

n\to \infty

References

erdosproblems.com/1203

No one has attempted this yet.

Formal statement

Lean type

True ↔ Filter.Tendsto Erdos1203.F Filter.atTop Filter.atTop

What you must prove

import FormalConjectures.ErdosProblems.«1203»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1203.erdos_1203" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1203.lean

Source type SHA-256: sha256:45fa62117f124f409a76e766632db59989b0fa75a7e0c329d86c5db39ae72e72
Task id: fc-379fc029-erdos1203-erdos-1203-3813980b2c-formalized-v1
Task commitment: sha256:5a94909f12fb52258642ea8a183aaa13ddc4b9b212b3860f3bd8b412ad07034c

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.