ABSTRACT. This paper summarises seven papers published since 2016 with the aim of fostering collaboration towards a relatively unexplored goal: supporting the learning of mathematics by software at an early stage of learning, starting with the introduction of variables and ending up somewhere in academic engineering courses. The summary is self-contained and relatively brief, as it refers to the seven papers in which the technical details of the software are presented and discussed, in which related work is mentioned, and which contain many further references. As in many of the seven papers, also this summary starts from education considerations, the requirements arising from the practical teaching of mathematics in schools and at university. These requirements determine the technology implemented in the project Isabelle/MAWEN which is the central point in this summary.

ABSTRACT. Isabelle is a powerful generic proof assistant, usable with many different object logics. Its most common incarnation is with Higher-Order Logic (HOL) as Isabelle/HOL, where it offers powerful proof automation (among a plethora of other features). Ordinarily, this is a strong advantage of Isabelle. But it presents a challenge for teaching its use: powerful automation can easily obscure the basic underlying mechanics of the proof assistant, and thus lead beginner’s understanding astray. Likewise, Isabelle’s version of HOL has evolved significantly compared to Gordon’s original formulation, and a conventional introduction to Gordon’s HOL in a course about Isabelle can easily raise more questions than it will answer. To address both these issues, we introduce MiniHOL, a smaller, readable-for-beginners version of the object logic implemented in Isabelle/HOL’s actual HOL.thy & friends, and report on its use in the introductory theorem proving course on Isabelle/HOL held in the winter semester 2025/2026.

ABSTRACT. We present a tool for teaching classical propositional logic using the sequent calculus. The tool is a concise formalization in the Isabelle proof assistant. The formalization shows that the proof system is sound and complete. The tool has been used for several years as a gentle introduction to propositional logic and automated reasoning in courses for computer science students.

ABSTRACT. The computation of geometric loci is a foundational feature of Dynamic Geometry software. Despite its conceptual importance and long history, current Dynamic Geometry systems still lack a fully symbolic and algebraically meaningful approach to locus computation. Even platforms that integrate computer algebra, such as GeoGebra, mainly provide numerical or graphical outputs whose interpre- tation remains limited. In this paper, we present a Computer Algebra System-based exploration of symbolic locus computation aimed at identifying conceptual, algebraic, and algorithmic challenges that arise when attempting to move beyond current Dynamic Geometry capabilities. Computer Al- gebra Systems play a central role in our work, not as a black-box calculator, but as a research tool that allows the design and testing of non-standard symbolic algorithms based on elimination theory, ideals, and parameter handling. Through a series of representative examples, we show why truly symbolic locus computation is mathematically nontrivial and computationally demanding, and why a Computer Algebra System is essential for experimenting with new approaches that may eventually inform the development of future Dynamic Geometry commands. Our work should be understood as an ongoing process to lay the groundwork for gradual and feasible advances rather than proposing finished solutions.

ABSTRACT. In German secondary education, students' exposure to proof-writing is typically limited to simple term rewriting, informal arguments, and the use of computer algebra systems (CAS). The Deutsche SchülerAkademie is a program offering intensive academic summer courses to secondary-school students in their final two years before graduation. Within this context, a course aimed at teaching students the basics of Isabelle/HOL was conducted, culminating in the formalization of the students' own correctness proof of the RSA cryptosystem. The authors participated in this course, one as a student and the other as an instructor. In this paper, we describe the aims and the framework of the course as well as the resulting curriculum. Furthermore, we discuss the difficulties faced by the students and how these were addressed. Finally, we reflect on the students' achievements and possibilities for further improvement.

ABSTRACT. We study the use of an educational proof assistant in an introductory proof course through a quasi-experiment in a varied setting: multiple teachers, students with different study programs, and a mixed Dutch-English language environment. First-year university students are known to struggle with writing proofs. Waterproof is a proof assistant that is designed to support the transfer of skills to paper proofs by working with controlled natural language. We focus on the students' ability to construct valid mathematical proofs, and on their learning process. We study this through in-class observation, surveys, and analysis of student performance and proof structure. We present evidence that effects of using an educational proof assistant carry over to the pen-and-paper context, even when the assistant is English and the proof is given in Dutch. We also present evidence that suggests students in the Mathematics-Computer Science program achieve higher grades when using Waterproof. Our most important conclusion is that an educational proof assistant can help students be more explicit in their proofs.

ABSTRACT. We introduce Waterproof River: An LLM-based tutor that augments the educational software Waterproof. In Waterproof, students can write proofs in controlled natural language. Waterproof River gives additional support with writing proofs in this form. We give an overview of its features, such as helping with syntax, asking for a hint, translating a free-form natural language proof to Waterproof syntax, and asking questions on the lecture notes. We present its implementation and discuss how such a tool could evolve based on in-class experience.

ABSTRACT. In this talk, we will present a formalization of a preparatory-class propositional-logic corpus which is both readable and machine-checked. The goal of this work is to produce material that can be used to teach students who are not acquainted with a proof assistant. To reach this goal, we base our work on a layer above the Lean proof assistant called Yalep [10] which allows to express proofs in a minimalistic controled natural language. We explain the scope of the formalization, the main modeling choices, and the main difficulties. We also present representative results, including the formalization of two competitive exam problems to show that the library is usable in this context.

ABSTRACT. Developing software for formal mathematics is straightforward since the problem and the method of solution are clearly defined. But then the software is also intended to be used by students and/or pupils and it turns out (as is well known from commercial products) that the user interface requires several times the development effort compared to the backend. This demonstration shows that the proof assistant Isabelle possesses generic functionalities that allow an existing backend to be connected to the state-of-the-art user interface Isabelle/jEdit with a reasonable amount of effort.

ABSTRACT. We present Rocq Game, a web-based educational tool designed to support interactive learning with the Rocq proof assistant. The system provides a setup-free, browser-based environment leveraging jsCoq, combining gamified progression, structured learning paths, and real-time proof feedback. Rocq Game separates pedagogical content from application logic through a lightweight domain-specific language, enabling instructors to create modular learning materials efficiently. Initial classroom deployment in a type theory course indicates that the tool lowers the entry barrier to proof assistants while maintaining the expressive power of Rocq.