import Mathlib import FormalConjectures.ErdosProblems.«13» import TaskSupport namespace Bounty theorem target : fcTypeOfName% "Erdos13.erdos_13.variants.general" := by sorry end Bounty