import Erdos870.MainTheorem

namespace Erdos870

/-- Public entry point for the formal negative solution of Erdős Problem #870. -/
theorem erdos_870 : Erdos870Target :=
  main_theorem

#print axioms erdos_870

end Erdos870