proof assistants - Is there a known way to formalise notion that certain theorems are essential ones?

Although your question is vague in certain ways, one robust answer to it is provided by the subject known as Reverse Mathematics. The nature of this answer is different from what you had suggested or solicited, in that it is not based on any observed data of mathematical practice, but rather is based on the provable logical relations among the classical theorems of mathematics. Thus, it is a mathematical answer, rather than an engineering answer.

The project of Reverse Mathematics is to reverse the usual process of mathematics, by proving the axioms from the theorems, rather than the theorems from the axioms. Thus, one comes to know exactly which axioms are required for which theorems. These reversals have now been carried out for an enormous number of the classical theorems of mathematics, and a rich subject is developing. (Harvey Friedman and Steve Simpson among others are prominent researchers in this area.)

The main, perhaps surprising conclusion of the project of Reverse Mathematics is that it turns out that almost every theorem of classical mathematics is provably equivalent, over a very weak base theory, to one of five possibilities. That is, most of the theorems of classical mathematics turn out to be equivalent to each other in five large equivalence classes.

For example,

• Provable in and equivalent to the theory RCA₀ (and each other) are: basic properties of the natural/rational numbers, the Baire Cateogory theorem, the Intermediate Value theorem, the Banach-Steinhaus theorem, the existence of the algebraic closure of a countable field, etc. etc. etc.




• Equivalent to WKL₀ (and each other) are the Heine Borel theorem, the Brouer fixed-point theorem, the Hahn-Banach theorem, the Jordan curve theorem, the uniqueness of algebraic closures, etc. , etc. etc.




• Equivalent to ACA₀ (and each other) are the Bolzano-Weierstraus theorem, Ascoli's theorem, sequential completeness of the reals, existence of transcendental basis for countable fields, Konig's lemma, etc., etc.




• Equivalent to ATR₀ (and each other) are the comparability of countable well orderings, Ulm's theorem, Lusin's separation theorem, Determinacy for open sets, etc.




• Equivalent to Π¹₁ comprehension (and each other) are the Cantor-Bendixion theorem and the theorem that every Abelian group is the direct sum of a divisible group and a reduced group, etc.

The naturality and canonical nature of these five axiom systems is proved by the fact that they are equivalent to so many different classical theorems of mathematics. At the same time, these results prove that those theorems themselves are natural and essential in the sense of the title of your question.

The overall lesson of Reverse mathematics is the fact that there are not actually so many different theorems, in a strictly logical sense, since these theorems all turn out to be logically equivalent to each other in those five categories. In this sense, there are essentially only five theorems, and these are all essential. But their essential nature is mutable, in the sense that any of them could be replaced by any other within the same class.

I take this as a robust answer to the question that you asked (and perhaps it fulfills your remark that you thought ideally the answer would come from proof theory). The essential nature of those five classes of theorems is not proved by looking at their citation statistics in the google page-rank style, however, but by considering their logical structure and the fact that they are logically equivalent to each other over a very weak base theory.

Finally, let me say that of course, the Reverse Mathematicians have by now discovered various exceptions to the five classes, and it is now no longer fully true to say that ALL of the known reversals fit so neatly into those categories. The exceptional theorems are often very interesting cases which do not fit into the otherwise canonical categories.