If Computer Mathematics (= Formal Mathematics) is going to succeed, international collaboration is necessary. If collaboration is going to succeed, one needs a system that can check proofs that are also understandable by humans. Such systems are available. Human referees are necessary to make contributions coherent. The good news is that building on top of existing libraries goes well: the systems are scalable. The bad news is that there are several exclusive groups of systems.
Questions.