import FormalConjectures.ErdosProblems.«172» import TaskSupport namespace Bounty theorem target : ¬ (fcTypeOfName% "Erdos172.erdos_172") := by sorry end Bounty