On Duplication in Mathematical Repositories

TL;DR

This paper argues that duplicating knowledge in mathematical repositories can be justified, analyzing various scenarios and providing examples to support the idea that duplication may be beneficial or necessary.

Contribution

It challenges the common assumption that mathematical repositories should avoid duplication, offering a nuanced analysis and examples supporting intentional duplication.

Findings

Duplication can facilitate easier access and cross-referencing.

In some cases, duplication helps maintain consistency across different formalizations.

Examples demonstrate situations where duplication improves repository usability.

Abstract

Building a repository of proof-checked mathematical knowledge is without any doubt a lot of work, and besides the actual formalization process there also is the task of maintaining the repository. Thus it seems obvious to keep a repsoitory as small as possible, in particular each piece of mathematical knowledge should be formalized only once. In this paper, however, we claim that it might be reasonable or even necessary to duplicate knowledge in a mathematical repository. We analyze different situations and reasons for doing so and provide a number of examples supporting our thesis.