Comment by fdupress

The theorem doesn't exist in a vacuum. It talks about objects that must be formally defined. And if that formal definition (which is part of the API) is not immediately compatible with those others use, and every single theorem comes with its own definitions of the objects they're working on, you're going to be reinventing the wheel over and over again.

Replacing thought and curation with repeated automation is tech debt, pushed down to fundamental knowledge and understanding.