I think you may be confusing specification of the problem and the formalization ...

		dooglius 5 days ago \| parent \| context \| favorite \| on: “Erdos problem #728 was solved more or less autono... I think you may be confusing specification of the problem and the formalization of the proof.