import Mathlib import FormalConjectures.ErdosProblems.«60» import TaskSupport namespace Bounty theorem target : fcTypeOfName% "Erdos60.erdos_60" := by sorry end Bounty