import Mathlib import FormalConjectures.ErdosProblems.«111» import TaskSupport namespace Bounty theorem target : fcTypeOfName% "Erdos111.erdos_111" := by sorry end Bounty