[maxwells-daemon]

Thank you! It depends on the topic. Some fields (algebra, number theory) are covered well by Lean's math library, and so I think we are already there; I recommend trying Aristotle for yourself to see how reliably it can formalize these theorems!

In other fields (topology, probability, linear algebra), many key definitions are not in Mathlib yet, so you will struggle to write down the theorem itself. (But in some cases, Aristotle can define the structure you are talking about on the fly!)

This is not an intrinsic limitations of Lean, it's just that nobody has taken the time to formalize much of those fields yet. We hope to dramatically accelerate this process by making it trivial to prove lemmas, which make up much of the work. For now, I still think humans should write the key definitions and statements of "central theorems" in a field, to ensure they are compatible with the rest of the library.

[zozbot234]

> ... But in some cases, Aristotle can define the structure you are talking about on the fly! ...

Do you have any plans to characterize these cases more fully, and perhaps propose your own contributions to mathlib itself on that basis?

[tachim]

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