The Flexiformalist Manifesto

In this manifesto, we develop the "Flexiformalist Program". This may be thought of as a modern extension of Hilbert\´s "Formalist Program", which solved the foundational crisis of mathematics but remained purely theoretical: Even though formal representations are a prerequisite for computer support in mathematics, formalization is a possibility that is usually unconsummated and thus does not have any practical influence on day-to-day mathematics.The Flexiformalist Program aims to change this and calls for1. The development of a regime of partially formalizinga. mathematical knowledge into a modular ontology of mathematical theories (content commons), andb. mathematical documents by semantic annotations and links into the content commons (semantic documents),2. The establishment of a software infrastructure witha. a distributed network of archives that manage the content commons and collections of semantic documents,b. semantic web services that perform tasks to support current and future mathematic practicesc. active document players that present semantic documents to readers and give access to respective3. the re-development of a comprehensive part of mathematical knowledge and the mathematical documents that carries it into a flexiformal digital library of mathematics (FDLM). We believe that such a flexiformal digital library will significantly empower mathematicians, scientists, and engineers in research, education, and application. Our experiences with early approximations of the FDLM show that the approach can be profitably transferred to other domains in science, technology, and engineering.