import Mathlib import FormalConjectures.ErdosProblems.«86» import TaskSupport namespace Bounty theorem target : fcTypeOfName% "Erdos86.erdos_86" := by sorry end Bounty