Towards automatically categorizing mathematical knowledge

Clearly, there is no definitive standard for categorizing information contained in mathematical papers. Even if AMS Mathematics Subject Classification was important for mathematicians for years, nowadays we can observe growing popularity of other schemes, e.g. arXiv categories. On the other hand, in the era of digital information storing one can expect from the process of classification to be more or less automatic. Furthermore, generic categorization can be done inside the search engine. At different level, the distinction between such classical tagging items as lemma, proposition, theorem etc. had the aim of showing importance of proven facts. Here the automatization is much harder, or, to be more precise, the results obtained can be far from the original tagging given by the author. In the paper we point out some problems and thoughts concerned with the categorization of mathematical knowledge, illustrating some of them by examples taken from the Mizar Mathematical Library, large machine-checked repository of mathematical facts.