Mathematical Libraries as Proof Assistant Environments

Abstract. In this paper we analyse the modifications on logical operations-- as proof checking, type inference, reduction and convertibility-- that are required for the identification of a proof assistant environment with a distributed mathematical library, focusing on proof assistants based on the Curry-Howard isomorphism. This identification is aimed at the integration of Mathematical Knowledge Management tools with interactive theorem provers: once the distinction between the proof assistant environment and a mathematical library is blurred, it is possible to exploit Mathematical Knowledge Management rendering, indexing and searching services inside an interactive theorem prover, a first step towards effective loosely-coupled collaborative mathematical environments