Comment by pfdietz

I'm thinking once we have much of the math literature formalized it's going to be possible to mine commonalities like that. Think of it as automated refactoring, applied to math.