OAF: An Open Archive of Formalizations

数学知识是科学和工程的核心，也是发达国家创新的主要因素。它的数量目前的增长速度超过了我们组织和利用它的能力。通过符号(软件)系统的机器支持将极大地增强数学知识的潜力，但前提是存在形式化的背景知识库。因此，形式化的成本阻碍了机器支持。更糟糕的是，符号系统及其库是不可互操作的，因为它们基于不同的基础，而且许多工作都花在基本库的重新开发上，这些库可以更有成效地投资于涵盖新的领域。此外，随之而来的多种多样的库格式迫使实现者将时间花在库组织功能上，而不是完善其系统的核心功能。拟议的oaf项目通过开发用于形式化的开放档案、用于管理和共享形式化的数学知识(如理论、定义和证明)的通用和开放的基础设施来解决这些互操作性和多样性问题。在知识库的规模和逻辑基础的多样性方面，oaf基础设施都是可扩展的。特别是，OAF系统将基于统一的独立于基础的图书馆表示格式，该格式允许将逻辑基础与图书馆一起形式化，从而作为调整图书馆的框架。这将解决当前技术状态中的两个主要瓶颈。它将提供一个永久存档解决方案，并非所有系统和用户社区都能负担得起单独维护。它将建立一种标准化和开放的图书馆格式，作为比较和系统演变的催化剂。符号系统开发人员将能够通过将他们的库输出到OAF来委托图书馆管理，数学知识管理(MKM)系统的开发人员将能够在其上开发高级服务。与当前技术状态相反，这允许分离关注点：符号系统的开发人员可以专注于其系统的逻辑核心，而通用MKM服务的开发人员可以访问相关大小的库。最后，我们档案库的统一表示语言首次实现了对以不同形式编写的大型库集成的系统大规模调查。从长远来看，这使得图书馆能够无缝地组合和合并成一个通用的大规模知识空间。

Mathematical knowledge is at the core of science and engineering and a major factor in innovation in developed societies. Its quantity is currently growing faster than our ability to organize and utilize it. Machine support via symbolic (software) systems would greatly enhance the potential of mathematical knowledge, but is predicated on the existence of libraries of formalized background knowledge. Thus, machine support is hampered by the costliness of formalization. Even worse, symbolic systems and their libraries are non-interoperable because they are based on differing foundations, and much work is spent on re-development of basic libraries that could be more productively invested in covering new areas. Moreover, the ensuing plurality of library formats forces implementors to spend time on library organization features instead of perfecting the core functionality of their systems. The proposed OAF project tackles these interoperability and plurality problems by developing an open archive for formalizations, a common and open infrastructure for managing and sharing formalized mathematical knowledge such as theories, definitions, and proofs. The OAF infrastructure is designed to be scalable with respect to both the size of the knowledge base and the diversity of logical foundations. In particular, the OAF system will be based on a uniform foundation-independent representation format for libraries, which allows formalizing the logical foundations alongside the library and thus acts as framework for aligning libraries.This will resolve two major bottlenecks in the current state of the art. It will provide a permanent archiving solution that not all systems and user communities can afford to maintain separately. And it will establish a standardized and open library format that serves as a catalyst for comparison and thus evolution of systems.Symbolic system developers will be able to delegate library management by exporting their libraries into the OAF and developers of mathematical knowledge management (MKM) systems will be able to develop high-level services on top of it. Contrary to the current state of the art, this permits separating the concerns: developers of symbolic systems could focus on the logical core of their system and developers of generic MKM services gain access to relevant-size libraries.Finally, our archive's uniform representation language for libraries enables -- for the first time -- systematic large scale investigations into the integration of large libraries written in different formalisms. In the long run, this enables the seamless combining and merging of libraries into a universal large-scale knowledge space.