Problem

erdos:888

(fun n => ↑(Nat.findGreatest (Erdos888.p n) n)) =Θ[Filter.atTop] fun n => ↑n * Real.log (Real.log ↑n) / Real.log ↑n

Open Current State

Declared status: solved
Formalization: formalized
Subjects: number theorysquares
OEIS: A387584
Sources: source:erdos-ai-contributions-wikisource:erdos-problemssource:formal-conjecturessource:gpt-erdossource:vibemathed
Statement: www.erdosproblems.com

Matching claims

0

No direct claims

This problem has no directly related claim record.

Browse this Repository’s Claims