Proceedings 12th International Workshop on Theorem proving components for Educational software

• URL: http://arxiv.org/abs/2404.03709v1
• Date: Thu, 4 Apr 2024 11:51:26 GMT
• Title: Proceedings 12th International Workshop on Theorem proving components for Educational software
• Authors: Julien Narboux, Walther Neuper, Pedro Quaresma,
• Abstract summary: 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. 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. Seven submissions have been accepted by our reviewers, who jointly produced at least three careful reports on each of the contributions.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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)

Related papers

• First Steps towards K-12 Computer Science Education in Portugal -- Experience Report [49.1574468325115]
  This paper reports on the efforts of the ENSICO association to implement such aims in Portugal. Starting with pilot projects in a few schools in 2020, it is currently working with 4500 students, 35 schools and 100 school teachers. The main aim is to gain enough experience and knowledge to eventually define a comprehensive syllabus for teaching computing as a mandatory subject.
  arXiv  Detail & Related papers  (2024-11-15T12:32:52Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  We introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. We fine-tune the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs. Our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any.
  arXiv  Detail & Related papers  (2024-05-23T09:03:42Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)
• Proceedings Fifth International Workshop on Formal Methods for Autonomous Systems [0.0]
  FMAS 2023 was co-located with 18th International Conference on integrated Formal Methods (iFM'22) The workshop itself was held at Scheltema Leiden, a renovated 19th Century blanket factory alongside the canal.
  arXiv  Detail & Related papers  (2023-11-15T14:20:56Z)
• Proceedings 39th International Conference on Logic Programming [53.44544554999452]
  This volume includes the Technical Communications presented at the 39th International Conference on Logic Programming (ICLP 2023) Main Track, the Doctoral Consortium, the Application and Systems/Demo track, the Birds-of-a-Feather track, the Thematic Tracks on Logic Programming and Machine Learning, and Logic Programming and Explainability, Ethics, and Trustworthiness.
  arXiv  Detail & Related papers  (2023-08-28T20:46:59Z)
• TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
  GPT-4's capabilities to solve these problems are unparalleled, achieving an accuracy of 51% with Program-of-Thoughts Prompting. TheoremQA is curated by domain experts containing 800 high-quality questions covering 350 theorems.
  arXiv  Detail & Related papers  (2023-05-21T17:51:35Z)
• Proceedings 11th International Workshop on Theorem Proving Components for Educational Software [0.0]
  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. ThEdu'22 was a vibrant workshop, with two invited talk by Thierry Dana-Picard and Yoni Zohar. The resulting revised papers are collected in the present volume.
  arXiv  Detail & Related papers  (2023-03-09T16:10:13Z)
• Proceedings 10th International Workshop on Theorem Proving Components for Educational Software [0.0]
  ThEdu'21 was a vibrant workshop, with an invited talk by Gilles Dowek (ENS Paris-Saclay), eleven contributions, and one demonstration. 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.
  arXiv  Detail & Related papers  (2022-02-02T05:48:14Z)
• What's New? Summarizing Contributions in Scientific Literature [85.95906677964815]
  We introduce a new task of disentangled paper summarization, which seeks to generate separate summaries for the paper contributions and the context of the work. We extend the S2ORC corpus of academic articles by adding disentangled "contribution" and "context" reference labels. We propose a comprehensive automatic evaluation protocol which reports the relevance, novelty, and disentanglement of generated outputs.
  arXiv  Detail & Related papers  (2020-11-06T02:23:01Z)
• Proceedings 9th International Workshop on Theorem Proving Components for Educational Software [0.0]
  The 9th International Workshop on Theorem-Proving Components for Educational Software (ThEdu'20) was scheduled to happen on June 29 as a satellite 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 our workshop. Given that many of us had already planned and worked for that moment, we decided that
  arXiv  Detail & Related papers  (2020-10-28T00:36:08Z)
• Proceedings 8th International Workshop on Theorem Proving Components for Educational Software [0.0]
  This volume contains the proceedings of the ThEdu'19 workshop, promoted on August 25, 2019, as a satellite event of CADE-27, in Natal, Brazil. Representing the eighth installment of the ThEdu series, ThEdu'19 was a vibrant workshop, with an invited talk by Sarah Winkler, four contributions, and the first edition of a Geometry Automated Provers Competition. 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 favoring software support for this transition by exploiting the power of theorem-proving
  arXiv  Detail & Related papers  (2020-02-27T03:10:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.