There have been many contributions to mathlib from Aristotle already, it’s a major use case for our users