I think we should consider having a table somewhere listing all important definitions and theorems, together with a latex identifier (or issue) and a link to a formalization, if it exists.
One advantage should be, that definitions and usages are easy to find then, using the latex-identifier. On the other hand, those have to be longer then.
Another thing is, that if we start to point to formalization (which I think should always be done by pointing to a part of a file in a specific commit), we might be able to build something which is update-able in a not-so-painful way.
I think we should consider having a table somewhere listing all important definitions and theorems, together with a latex identifier (or issue) and a link to a formalization, if it exists. One advantage should be, that definitions and usages are easy to find then, using the latex-identifier. On the other hand, those have to be longer then. Another thing is, that if we start to point to formalization (which I think should always be done by pointing to a part of a file in a specific commit), we might be able to build something which is update-able in a not-so-painful way.