Main goals
Large formal and semiformal mathematics libraries are needed to support mathematics research, mathematics education, rigorous software development, and formal proof development. This workshop explored methods for designing, constructing, and maintaining large mathematics libraries as well as for finding, comparing, and applying the knowledge residing in these libraries.
OpenDreamKit implication
The workshop was co-organised by Dennis M"uller (FAU). Florian Rabe (FAU) was a member of the programme committee. Michael Kohlhase (FAU) gave a talk presenting OpenDreamKit results.
Event summary
The workshop featured two invited talks by Makarius Wenzel and Claudio Sacerdoti Coen on making large libraries (Isabelle resp. Coq) available for system integration. It also included contributed talks on Logipedia by the Dedukti group, which closely collaborates with OpenDreamKit members, and mathematical datasets.
Results and impact
The main result of the workshop was to strengthen the awareness of and to support the community for managing large formal libraries. This has been a central topic in WP 6 of OpenDreamKit, and the discussions allowed presenting OpenDreamKit results.
In particular, the talks be Wenzel and Sacerdoti Coen presented results that were developed in collaboration with OpenDreamKit members in WP 6.