Abstract: This course will include:

• Lean and its ecosystem In this session I will discuss the ecosystem around the Lean theorem prover with a particular view to its use in education. In particular, I will pay attention to the widget system that allows for highly interactive and visual input/output. I will also showcase the flexibility of Lean's parser, and how it can be tailored to the needs of education. Finally, we can take a look at several online web-frontends built around Lean that might be of particular interest in the classroom setting.
• Formal maths in Lean: a demonstration In this session I will demonstrate several techniques that can be used to formalise mathematics in Lean. We will see various components in action that were discussed in the session on Lean's ecosystem, and show how they can be combined to create a powerful and flexible environment for exploring mathematics.

Slides: slides-pat2023-commelin-talk1.pdf and slides-pat2023-commelin-talk2.pdf Abstract: This course will include:

• An overview of the evolution of AI research on the learning of proof in mathematics.
• Lessons learned, focusing on (1) the problem of feedback, (2) the relations between reasoning-proving and knowledge representation.
• A didactic analysis of the teaching of mathematical proof and its implications for the design of learning environments.

Some pointers are available on the blog of Nicolas Balacheff.
Slides: slides-pat2023-balacheff.pdf Abstract: in this course, we will present the role of logical analysis in the teaching and learning of proof and proving in mathematics and in computer science. We will develop three main points: the relationship and distinction between truth and validity; the importance of considering syntax, semantics and pragmatics for a proper understanding of logico-mathematical activities (both in mathematics and computer science); the contribution of natural deduction to highlight the relationship between logical and mathematical aspects in proof and proving.
Slides: slides-pat2023-durand-guerrier-meyer-talk1.pdf slides-pat2023-durand-guerrier-meyer-talk2.pdf slides-pat2023-durand-guerrier-meyer-talk3.pdf Abstract: Doing mathematics using the Coq Proof Assistant The Coq proof assistant allows, using the same infrastructure, not only to implement mathematical objects and their operations using a functional programming style, but also to formally prove some of their properties. This specification and proof task is mainly devoted to the user whereas the system checks that all the reasoning arguments are correct. In this course, we first focus on basic mathematical objects, such as integers and real numbers. We describe their implementation in Coq and build some operations on them. We then introduce the Coq tactic language and show how to use it to interactively prove formal properties. Carry out proofs interactively is very useful for students to learn how to reason correctly. However when dealing with larger and more complex mathematical theories, we can take advantage of Coq advanced automated tactics which deals with most technical details, allowing the user to focus on the main steps of the proof. In a second time, we shall present some of the large formal developments available in Coq, tailored to carry out University-level mathematics, in fields such as analysis, algebra or geometry. Among the advanced topics that we shall cover, we will present the coq-interval package which allows to use Coq as a scientific calculator, including features to display correct-by-construction curves.
Slides: slides-pat2023-magaud.pdf slides-pat2023-bertot.pdf pat2023-example-bertot.v sqrt2_not_rat.v Abstract: For several years we have been offering an elective course "Introduction to Interactive Theorem Proving" to our computer science undergraduates. Although the course has extensive mathematical content and is not directly applicable to jobs in the IT industry, it is very popular with students. The course is based on the proof assistant Isabelle/ HOL and is divided into two parts: (1) proofs, proof languages and formalisation of mathematics and (2) functional programming and verification of algorithms and data structures. We keep the pace slow and introduce new concepts very gently, but in the end students still manage to do a project in which they formalise an IMO problem or verify a simple algorithm or data structure. In this PAT course I will give a short introduction to Isabelle/ HOL using the same didactic approach and exercises that our students use. I will also talk about our experiences in class.
Slides: slides-pat2023-maric.pdf
Examples: FilipMaricPAT2023.zip Abstract: A mathematical proof is typically characterized as a sequence of mathematical assertions, where each assertion is an acceptable assumption, a known fact, or a deductive consequence of a previous assertion. However, both in mathematical instruction and mathematicians' professional practice, proofs often do not satisfy this categorization. For instance, claims in proofs are sometimes warranted by the careful inspection of a diagram. This occurs both in teaching contexts (like Euclidean geometry) and in contemporary mathematical practice (like low-dimensional topology). Proofs often contain lengthy sequences of imperatives that require the reader to imagine executing a series of mathematical commands, both in teaching contexts (like calculus) and in contemporary mathematical practice (like advanced set theory). In my lessons, I will demonstrate that, and illustrate how, these phenomena occur. I will describe the challenges that these phenomena pose for students, both in understanding the proofs that are presented to them and for translating their own proofs into a rigorous verbal-symbolic syntax. Finally, I will discuss didactical considerations for making proofs more transparent and comprehensible for the student.
Slides: slides-pat2023-weber-talk1.pptx slides-pat2023-weber-talk2.pptx slides-pat2023-weber-talk3.pptx