I'm wondering about the 'searchability' or canonicalization of such a theorem library. How do you make sure there's no duplicate work? How do you index the thin

I'm wondering about the 'searchability' or canonicalization of such a theorem library. How do you make sure there's no duplicate work? How do you index the thing? Can you match and input / output proposition and look through the whole database and have it find all related theorems? I'm thinking 'automatic lemma matching' for software verification. e.g. In a SPARK proof you might need to use a lemma [0]. If you formal math education is lacking or maybe your theorem library is not encyclopedic, you might want suggestions from 'the hive'... [0] https://blog.adacore.com/gnatprove-tips-and-tricks-using-the-lemma-library https://blog.adacore.com/gnatprove-tips-and-tricks-using-the...