Erdős problem 152

Must `lim f n = ∞`?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

152.lean

Retained formal statement1 of 2

Must lim f n = ∞?

This was proved formally by the DeepMind prover agent [DM26a].

FormalConjectures/ErdosProblems/152.leanErdos152.erdos_1521 lineExact file

1True ↔ Filter.Tendsto Erdos152.f Filter.atTop Filter.atTop

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.