Preface

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 10th International Workshop on Theorem Proving Components for Educational Software, (ThEdu'21), was a satellite event of the 28th International Conference on Automated Deduction, on July 11th, 2021, at Carnegie Mellon University, in the USA. Due to the COVID-19 pandemic, CADE-28 and all its co-located events took place as virtual events.

ThEdu'21 was a vibrant workshop, with an invited talk by Gilles Dowek (ENS Paris-Saclay), eleven contributions, and one demonstration.

An open call for papers was then issued, and attracted ten submissions, of which seven have been accepted by our reviewers, who jointly produced at least three careful reports on each of the contributions. The resulting revised papers are collected in the present volume.

The contributions in this volume are a faithful representation of the wide spectrum of ThEdu, ranging from those more focused on the automated deduction research, not losing track of the possible applications in an educational setting, to those focused on the applications, in educational settings, of automated deduction tools and methods.

Two new and exciting additions to the dynamic geometry system GeoGebra are explored. Zoltán Kovács and Jonathan H. Yu explore the automated discovery of theorems in elementary planar geometry, introducing a new GeoGebra command and tool, Discovery, with which it is possible to analyse geometric figures for salient patterns and properties. Zoltán Kovács and Róbert Vajda introduce another new GeoGebra feature, the Compare command, which allows to automatically obtain proofs of conjectures not only about equalities, but also about inequalities. Given that GeoGebra is hugely popular with the community of secondary schools' math teachers, the possible applications to education are real, opening the automated deduction area to a new community of non-experts who are eager to use new and intelligent tools for educational purposes. The paper by Pedro Quaresma and Vanda Santos discusses precisely this problem: how can we bring automated theorem tools and methods to the practice of the secondary schools? What are the strong and weak points, and how can we begin to address them? Four applications of automated deduction to university-level education are presented. Clemens Eisenhofer and Martin Riener use an SMT solver for tracing the execution of code, in a bounded model-checking style, to help on teaching how to program. Merlin Carl, Hinrich Lorenzen and Michael Schmitz present and analyse the employment of the Diproche system, a natural language proof checker, within a one-semester mathematics beginners lecture. The system is used to check the students' solution attempts to prove exercises in set theory and elementary number theory, and to give them immediate feedback. Jørgen Villadsen, Asta Halkjær From and Patrick Blackburn describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. John Boyland describes the evolution of SASyLF, an educational proof assistant for teaching type theory, from 2008 to 2021, reviewing its strong points, its weak points and the plans to address the latter as well as to continue the development of this tool, that has been used in courses at several universities in the USA.

For their help in reviewing the papers, the editors would like to thank the other members of the Programme Committee of ThEdu'21: Francisco Botana (University of Vigo at Pontevedra, Spain); David Cerna (Czech Academy of Sciences Institute of Computer Science, Czech Republic); Ludovic Font (École Polytechnique de Montréal, Canada); Filip Marić (University of Belgrade, Serbia); Adolfo Neto (UTFPR, Brazil); Philippe Richard (University of Montreal, Canada); Vanda Santos (University of Aveiro, Portugal); Wolfgang Schreiner (Research Institute for Symbolic Computation (RISC), Austria) and Jørgen Villadsen (Technical University of Denmark, 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 scientists, mathematicians and stakeholders in education.

While this volume goes to press, the next edition of the ThEdu workshop is being prepared: ThEdu'22 will be a satellite event of 11th International Joint Conference on Automated Reasoning, IJCAR 2022, to be held in Haifa (Israel), in August 2022, as part of FLoC 2022.