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. 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. PC Chairs:Julien Narboux (University of Strasbourg, France); Walther Neuper (JKU, Johannes Kepler University, Linz, Austria); Pedro Quaresma (University of Coimbra, Portugal)

翻译：ThEdu系列致力于推动从中学数学的直观方式向STEM教育中更为形式化的学科方法的平滑过渡，同时借助定理证明技术的优势，为此过渡提供软件支持。以下简述本卷如何推动这一事业。第十二届教育软件定理证明组件国际研讨会（ThEdu'23）是第二十九届国际自动演绎会议（CADE 2023）的卫星活动，于2023年7月1日至4日在意大利罗马举行。ThEdu'23取得圆满成功，包含一场特邀报告：由Yves Bertot（法国国家信息与自动化研究所）所作的《使用类型论教授数学的挑战》，以及七篇常规投稿。随后公开发出征稿通知，共收到八篇投稿。经评审人审核，其中七篇被录用，每篇稿件均获得至少三份详尽评审报告。修订后的论文收录于本卷。作为卷编辑，我们希望这些论文能进一步推动基于定理证明的软件发展，并促进计算机科学家、数学家和教育工作者之间的相互理解。程序委员会主席：Julien Narboux（法国斯特拉斯堡大学）；Walther Neuper（奥地利约翰·开普勒林茨大学）；Pedro Quaresma（葡萄牙科英布拉大学）