import Mathlib import FormalConjectures.ErdosProblems.«70» import TaskSupport namespace Bounty theorem target : fcTypeOfName% "Erdos70.erdos_70" := by sorry end Bounty