alt Hacker NewsYes, but thing is, for a lot of basic stuff there are myriad ways in which it is formulated, so humans have to decide which of them goes in the library. Of course you can include two or five or ten equivalent formulations (like textbooks sometimes do) but still, not everything under the sun.
Probably this will be done in some form in the coming months.
> Of course you can include two or five or ten equivalent formulations (like textbooks sometimes do) but still, not everything under the sun.
Note that mathlib currently includes duplicates of many theorems; I believe deduplication is an active goal (if not one seeing much labor right now).