Related papers: Maths with Coq in L1, a pedagogical experiment
In parallel to the ever-growing usage of mechanized proofs in diverse areas of mathematics and computer science, proof assistants are used more and more for education. This paper surveys previous work related to the use of proof assistants…
We describe the difficulties that advanced undergraduate and graduate students have with quantum measurement within the standard interpretation of quantum mechanics. We explore the possible origins of these difficulties by analyzing student…
Physics lab courses are an essential part of the physics undergraduate curriculum. Learning goals for these classes often include the ability to interpret measurements and uncertainties. The Physics Measurement Questionnaire (PMQ) is an…
The paper examines the construction of a course in mathematical analysis at a pedagogical university, aimed at developing the ability of future mathematics teachers to detect and solve problems related to finding proofs. Key words: teaching…
These are the notes for a 5-lecture-course given at ESSLLI 2006 in Malaga, Spain. The URL of the school is http://esslli2006.lcc.uma.es/ . This version slightly differs from the one which has been distributed at the school because typos…
This paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language,…
One important approach to software verification is interactive theorem proving. However, writing formal proofs often requires substantial human effort, making proof automation highly important. Traditionally, proof automation has relied on…
This paper presents an intervention study on the effects of the combined methods of (1) the Socratic method, (2) Chain of Thought (CoT) reasoning, (3) simplified gamification and (4) formative feedback on university students' Maths learning…
It is generally accepted that the retention and associated completion rates for first year classes are an area of concern for UK universities, and physics and astronomy classes at the University of Glasgow are exception. Classes are often…
Proof assistants enable users to develop machine-checked proofs regarding software-related properties. Unfortunately, the interactive nature of these proof assistants imposes most of the proof burden on the user, making formal verification…
CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive…
Elfe is an interactive system for teaching basic proof methods in discrete mathematics. The user inputs a mathematical text written in fair English which is converted to a special data-structure of first-order formulas. Certain proof…
Diproche ("Didactical Proof Checking") is an automatic system for supporting the acquistion of elementary proving skills in the initial phase of university education in mathematics. A key feature of Diproche - which is designed by the…
We are convinced of the usefulness of sketches and diagrams during mathematical work but the observation is made in our practices that they are not spontaneously used by students. In order to study the understanding and use of sketches by…
Expressive static typing disciplines are a powerful way to achieve high-quality software. However, the adoption cost of such techniques should not be under-estimated. Just like gradual typing allows for a smooth transition from…
Theorem provers are important tools for people working in formal verification. There are a myriad of interactive systems available today, with varying features and approaches motivating their development. These design choices impact their…
This report presents a formalization of May's theorem in the proof assistant Coq. It describes how the theorem statement is first translated into Coq definitions, and how it is subsequently proved. Various aspects of the proof and related…
Problems in probability theory prove to be one of the most challenging for students. Here, we formulate and discuss four related problems in probability theory that proved difficult for first to fourth-year undergraduate students whose…
We transitioned our post-CS1 course that introduces various subfields of computer science so that it integrates Large Language Models (LLMs) in a structured, critical, and practical manner. It aims to help students develop the skills needed…
How difficult are interactive theorem provers to use? We respond by reviewing the formalization of Hilbert's tenth problem in Isabelle/HOL carried out by an undergraduate research group at Jacobs University Bremen. We argue that, as…