Published: 30th October 2020
DOI: 10.4204/EPTCS.328
ISSN: 2075-2180


Proceedings 9th International Workshop on
Theorem Proving Components for Educational Software
Paris, France, 29th June 2020

Edited by: Pedro Quaresma, Walther Neuper and João Marcos

João Marcos, Walther Neuper and Pedro Quaresma
Teaching Interactive Proofs to Mathematicians
Mauricio Ayala-Rincón and Thaynara Arielly de Lima
Isabelle/HOL as a Meta-Language for Teaching Logic
Asta Halkjær From, Jørgen Villadsen and Patrick Blackburn
Formalizing IMO Problems and Solutions in Isabelle/HOL
Filip Marić and Sana Stojanović-Đurđević
Number Theory and Axiomatic Geometry in the Diproche System
Merlin Carl
Lucas-Interpretation on Isabelle's Functions
Walther Neuper


The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the power of theorem-proving technologies. What follows is a brief description of how the present volume contributes to this enterprise.

The 9th International Workshop on Theorem Proving Components for Educational Software, (ThEdu'20), was scheduled to happen on June 29 as a satellite event of the IJCAR-FSCD 2020 joint meeting, in Paris. The COVID-19 pandemic came by surprise, though, and the main conference was virtualised. Fearing that an online meeting would not allow our community to fully reproduce the usual face-to-face networking opportunities of the ThEdu initiative, the Steering Committee of ThEdu decided to cancel the workshop.

Given that many of us had already planned and worked for that moment, we decided that ThEdu'20 could still live in the form of an EPTCS volume. The EPTCS editors concurred with us, recognising this very singular situation, and accepted our proposal of organising a special issue with papers submitted to ThEdu'20. An open call for papers was then issued, and attracted five submissions, all of which have been accepted by our reviewers, who produced three careful reports on each of the contributions. The resulting revised papers are collected in the present volume.

With the contributions in this volume it became clear that: the automated reasoning tools are becoming mature enough for crossing the boundary from research to application; when education is concerned the interactive provers and some specifically chosen topics are preferred as application tools instead of the fully automatic tools and generic scenarios. We see in the paper by Mauricio Ayala-Rincón and Thaynara Arielly de Lima and in the paper by Asta Halkjær From, Jørgen Villadsen and Patrick Blackburn approaches that use interactive theorem provers to convince mathematicians to include them in their toolboxes, in the first and in the second as tools for teaching logic. In the paper by Filip Marić and Sana Stojanović-Đurđević preparatory steps are taken to envisage the goal to win the gold medal in the IMO Grand Challenge. The papers by Merlin Carl an by Walther Neuper describe systems to design interactive proving systems, in concrete scenarios in the first case, in a more generic setting, in the second.

For their help in reviewing the papers, the editors would like to thank the other members of the Programme Committee of ThEdu'20 and the external reviewers, namely Francisco Botana (University of Vigo at Pontevedra, Spain), David Cerna (Research Institute for Symbolic Computation, Johannes Kepler University, Austria), Filip Maric (University of Belgrade, Serbia), Adolfo Neto (UTFPR, Brazil), Vanda Santos (University of Aveiro, Portugal), Wolfgang Schreiner (Johannes Kepler University, Austria) and Jørgen Villadsen (Technical University of Denmark).

We, the volume editors, hope that this collection of papers will further promote the development of theorem-proving-based software, and that it will allow to improve the mutual understanding between computer mathematicians and stakeholders in education. With some luck, we would actually expect that the very special circumstances set up by the worst sanitary crisis in a century will happen to reinforce the need for the application of certified components and of verification methods to the production of educational software that would be available even when the traditional on-site learning experiences turn out not to be recommendable.

While this volume goes to press, the next edition of the ThEdu workshop is being prepared: ThEdu'21 is planned to be a satellite event of CADE-28, Pittsburgh, PA, United States, July 2021.