Theorem proving is the sibling computation: Both share the representation of mathematical objects. But while computation aims at solving problems quickly and at large scale, theorem proving makes sure the solutions are correct.
Computation and theorem proving are critical for automating and scaling up STEM in the 21st century — but there are two problems. Firstly, computation and theorem proving are mostly done separately in different communities and using different approaches and systems. That’s because both problems are so hard by themselves already that solving them together is even harder. And secondly, both areas struggle to acquire funding for maintaining and developing their systems: most rewards are given to novel applications while the daily work of fixing bugs and making releases is often overlooked.
OpenDreamKit has generated a lot of attention because it managed to solve the second problem for computation (at least for 4 years). Now researchers in theorem proving have started similar efforts. This week Gilles Dowek hosted a meeting in Paris of leading European theorem proving researchers. Florian Rabe participated as a representative of the Erlangen-Nuremberg site (led by Michael Kohlhase) and of OpenDreamKit as a whole.
The goal is to launch Logipedia as a central system for integrating theorem prover libraries. An EU infrastructure project akin to OpenDreamKit may be started in the future.
Kohlhase and Rabe have collaborated with Dowek’s group for many years, including throughout OpenDreamKit. They have held multiple workshops together and have recently submitted a joint French (ANR)/German (DFG) grant proposal of verifying deduction system results.
Many ideas of Logipedia are related to or inspired by innovations of OpenDreamKit. In particular, the general Math-in-the-Middle approach developed OpenDreamKit and the use of alignments for aligning corresponding (logical) concepts has been adopted in Logipedia.
Future collaboration between these projects will be critical to make progress on the first problem mentioned above - an integration of OpenDreamKit’s Math-in-the-Middle infrastructure with Logipedia is an exciting way towards integrating theorem proving and computation systems.
Workshops and Conferences Blog WP6: Data/Knowledge/Software bases Math-in-the-Middle WP2: Dissemination Future funding