import Mathlib import FormalConjectures.ErdosProblems.«87» import TaskSupport namespace Bounty theorem target : fcTypeOfName% "Erdos87.erdos_87.parts.i" := by sorry end Bounty