The Chinese Remainder Theorem, its Proofs and its Generalizations in Mathematical Repositories
Christoph Schwarzweller · Studies in Logic Grammar and Rhetoric · 2009
In the spirit of mathematical knowledge management theorems are proven with computer assistance to be included into mathematical repositories. In the mathematical literature one often finds not only differ- ent proofs for theorems, but also different versions or generalizations with a different background. In mathematical repositories, for obvious reasons, there is usually one version of a theorem with one proof only - the authors choose a version and a proof which can be formalized most easily. In this paper we argue that there are other issues to decide which proof of a theo- rem or which version of a theorem should be included in a repository. These basically depend on the intended further use of the theorem and the proof. We illustrate these issues in detail with the Chinese Remainder Theorem as an example.