There have been many contributions to mathlib from Aristotle already, it’s a maj...

		tachim 68 days ago \| parent \| context \| favorite \| on: “Erdos problem #728 was solved more or less autono... There have been many contributions to mathlib from Aristotle already, it’s a major use case for our users