Erdős problem 152 · problems.science

Must lim f n = ∞?

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

152.lean

Retained formal statement2 of 2

Must f n ≫ n ^ 2?

This stronger quadratic variant was also proved formally by the DeepMind prover agent [DM26b].

FormalConjectures/ErdosProblems/152.leanErdos152.erdos_152.variants.square1 lineExact file

1True ↔ (fun n => ↑n ^ 2) =O[Filter.atTop] fun n => ↑(Erdos152.f n)

SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.