Comment Comment by tachim There have been many contributions to mathlib from Aristotle already, it’s a major use case for our users parent tachim 9 months ago