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 12th International Workshop on Theorem Proving Components for Educational Software (ThEdu'23) was a satellite event of the 29th international Conference on Automated Deduction (CADE 2023), July 1- 4, 2023, Rome, Italy. ThEdu'23 was very successful, with one invited talk, by Yves Bertot (Inria, France), "The challenges of using Type Theory to teach Mathematics", and seven regular contributions. An open call for papers was then issued, to which eight contributions were submitted. Seven submissions 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 describe the many systems/approaches that share the goal of reaching a wider audience. In doing so, they aim to promote the possibilities of using automatic deduction systems/approaches in education. In his invited talk, Yves Bertot addressed the challenges of using Type Theory to teach Mathematics, the abstract of which is here contained in HTML format only. Christophe Scholliers presents a small dependently typed programming language called WebPie; the author believes that his article can provide a step forward towards the understanding and systematic construction of dependently typed languages for researchers new to dependent types. Merlin Carl describes two systems currently being developed that use large language models for the automatized correction of (i) exercises in translating back and forth between natural language and the languages of propositional logic and first-order predicate logic and (ii) exercises in writing simple arguments in natural language in non-mathematical scenarios. In a second article Merlin Carl introduces the Diproche system. An automated proof checker for texts written in a controlled fragment of German, designed for didactical applications in classes introducing students to proofs for the first time. Simon Tobias Lund and Jørgen Villadsen present a formalization of higher-order logic in the Isabelle proof assistant built in such a way that it can serve as a good introduction for someone looking into learning about higher-order logic and proof assistants. Qinxiang Cao, Xiwei Wu and Yalun Liang present a small Coq library of sets and relations, that they have developed, in such a way that standard math notations can be used when teaching denotational semantics of simple imperative languages. Jelle Wemmenhove et al. introduce the system "Waterproof", an adaptation of the Coq proof assistant into an educational tool in order to help students learn how to write mathematical proofs. Walther Neuper presents the second part (see EPTCS 328) of a precise description of the prototype that has been developed in the course of the ISAC project. The ISAC project aims to develop software to support the most frequently encountered learning scenarios, the solving of mathematical problems. This second part of the description concerns the specification phase, which precedes the solving of engineering problems.

For their help in reviewing the papers, the editors would like to thank the other members of the Programme Committee of ThEdu'23: Francisco Botana (University of Vigo at Pontevedra, Spain), David Cerna (Johannes Kepler University, Austria) João Marcos (Federal University of Rio Grande do Norte, Brazil), Filip Marić (University of Belgrade, Serbia), Julien Narboux (University of Strasbourg, France), co-chair, Adolfo Neto (Federal University of Technology - Parana, Brazil), Walther Neuper (Johannes Kepler University Linz, Austria), co-chair, Pedro Quaresma (University of Coimbra, Portugal), co-chair, Vanda Santos (University of Aveiro, Portugal), Anders Schlichtkrull (Aalborg University, Denmark), M. Pilar Vélez (Nebrija University, Spain) and Jørgen Villadsen (Technical University of Denmark, Denmark) and the external reviewers Pierre Boutry (University of Strasbourg, France) and Frédéric Tran-Minh (ESISAR Grenoble INP, Valence, France).

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'24 will be a satellite event of the International Joint Conference on Automated Reasoning, Nancy, France, July 1-6, 2024.

The challenges of using Type Theory to teach Mathematics

The last decade has seen tremendous progress in the adoption of Type Theory-based interactive theorem provers to describe mathematical results, as illustrated by formal verification in group theory (the Feit-Thompson theorem, using Coq) and recent work in algebraic geometry (Formalisation of perfectoid spaces, using Lean).

Much of this work relies on expertise in using the proof systems, so that the question of applying these advances to teach mathematics remains an open problem. In the context of education, one must take into account the ever-changing level of expertise of the audience, the need to exercise skills to acquire them, etc.

In this talk, I will review a variety of features of Type Theory-based interactive provers that actually make these systems hard to use for teaching mathematics and reflect on corrective actions. In particular, I will review the issues that come specifically from the distance between the language of Type Theory and the language used in introductory mathematics at the level of undergraduate mathematics.