what is in a name
CSC remarks:
technical lemmas. The names are typically approximation of the statement, like
\texttt{mult\_minus} that could distributivity of multiplication over subtraction
for example. It could be useful to extract keywords from the name, e.g. automatically
trying to split names into words/symbols. The obtained names would be weak keywords,
so maybe they are already covered by Dublin Core?
MW:
see also David Aspinall, Cezary Kaliszyk: What's in a Theorem Name? ITP 2016.