import Mathlib import FormalConjectures.ErdosProblems.«59» import TaskSupport namespace Bounty theorem target : fcTypeOfName% "Erdos59.erdos_59.variants.big_o" := by sorry end Bounty