import Mathlib import FormalConjectures.ErdosProblems.«7» import TaskSupport namespace Bounty theorem target : fcTypeOfName% "Erdos7.erdos_7" := by sorry end Bounty