I suspect that set theory can serve as a universal language.
While I believe that proposition is true in a technical sense, I think
it is false in a more important logistical sense. I believe that a
substantial percentage, maybe even a majority, of the people who are
interested in mechanical proof checking are of a rather constructivist
bent, with marginal interest in a set theory based results. Consider,
for example, the large group of proof checkers that are based upon the
de Bruijn and Martin-Lof style of logics. I think I can count at
least six major, on going, multi-person-year efforts with such a
footing. I suspect that this may be larger than the number of on
going set theory based projects. The decision to study these logics
is often not a decision taken likely, but rather is often based upon
philosophical convictions, including doubts about set theory. So I
think a decision to use set theory as the foundation to be a poor
logistical decision because it leaves so many likely participants
"out".
I believe that that a very high percentage of practically important
mathematics, including essentially all that is need for proof theory
(metamathematics Hilbert-Bernays style) and practical computer
science, can be checked in a system or systems much weaker than set
theory. One does not need set theory, for example, to support
McCarthy's mathematical theory of computation, ("A Basis for a
Mathematical Theory of Computation", in Computer Programming and
Formal Systems, eds. P. Braffort and D. Hershberg, North-Holland,
1963). And I hope that we may be able to agree on some weaker systems
whose proof-checked results almost the whole community is willing to
depend upon. In fact, I have read, the work in "reverse mathematics"
of the last several decades suggests that almost all of the
mathematics used in engineering can be done in logics much weaker than
set theory.
Certainly, a set theory checker will be an important component of a
mechanically proof-checked encyclopedia of mathematics because set
theory is the universal carrier of the bulk of modern mathematics, a
vehicle gladly, if informally, used by almost all practicing
mathematicians. It may even be that almost all of the entries in such
an encyclopedia will be set theory based, in the absence of any other
framework for the whole of contemporary mathematics. But that doesn't
mean that set theory should be the foundation.
Apologies to those to whom I am repeating myself,
Bob