The Space of Mathematical Software Systems -- A Survey of Paradigmatic
Systems
Journal Articles
Overview
Research
View All
Overview
abstract
Mathematical software systems are becoming more and more important in pure
and applied mathematics in order to deal with the complexity and scalability
issues inherent in mathematics. In the last decades we have seen a cambric
explosion of increasingly powerful but also diverging systems. To give
researchers a guide to this space of systems, we devise a novel
conceptualization of mathematical software that focuses on five aspects:
inference covers formal logic and reasoning about mathematical statements via
proofs and models, typically with strong emphasis on correctness; computation
covers algorithms and software libraries for representing and manipulating
mathematical objects, typically with strong emphasis on efficiency;
concretization covers generating and maintaining collections of mathematical
objects conforming to a certain pattern, typically with strong emphasis on
complete enumeration; narration covers describing mathematical contexts and
relations, typically with strong emphasis on human readability; finally,
organization covers representing mathematical contexts and objects in
machine-actionable formal languages, typically with strong emphasis on
expressivity and system interoperability. Despite broad agreement that an ideal
system would seamlessly integrate all these aspects, research has diversified
into families of highly specialized systems focusing on a single aspect and
possibly partially integrating others, each with their own communities,
challenges, and successes. In this survey, we focus on the commonalities and
differences of these systems from the perspective of a future multi-aspect
system.
