Stream: Teaching [with] Coq

Topic: High schoolers using Coq?

Karl Palmskog (Aug 26 2024 at 12:55):

Someone contacted me about some high schoolers using a proof assistant to formalize this: https://staff.math.su.se/sjoerd.devries/files/ss22.pdf (set theory to geometry, including some group theory)

These are notes for a summer school taught in June 2022 at Stockholm University. It was a two-week school for high school students in their penultimate year, and meant to give an impression of what research in mathematics is like. The notes are meant to give an accessible introduction to the congruent number problem and several areas of university-level maths. A student learning about these topics for the first time should probably try to focus on one specific topic and try to get familiar with this, rather than try to understand everything

It seems their idea is to use Lean, and I'm personally inclined to agree with them, given that MathComp would be the natural library for Coq, and I don't think it's feasible to teach high schoolers MathComp (based on my experience).

Or how would this be best done in Coq?

Karl Palmskog (Aug 26 2024 at 12:57):

rationale for MathComp or bust: Stdlib sets are cumbersome, you need bigops and number stuff like elliptic curves

Thomas Lamiaux (Aug 26 2024 at 12:59):

@Pierre Rousselin you did something with high schoolers right ?

Pierre Rousselin (Aug 27 2024 at 15:38):

We mostly studied basic logic and some easy equations/inequalities on the real numbers. It was just a 6 hours experiment (if I remember correctly). Nothing of this scale.

I don't know how/if it will be easy with Lean. I don't think something comfortable enough exists with Coq at the moment.
The usual difficulties will arise: sets and subsets, sub-structure for subgroups, rational numbers, ...

And I don't know about $\mathbb{Z}/n\mathbb{Z}$ (real quotient or as it is done in the notes a finite set ${0, 1, ..., n - 1}$).

Karl Palmskog (Aug 27 2024 at 15:40):

thanks Pierre, based on these comments I think doing things in MathComp would be the only feasible Coq route (and MathComp would be hard for highschoolers to learn)

djao (Aug 27 2024 at 16:41):

I teach Coq to first-year university students (a bit older than high school, but not much). We don't use sets, sub-structures, rational numbers, or math comp. I also don't use quotient groups, but I teach setoids, which is enough to prove certain results about modular arithmetic, most notably Fermat's Little Theorem (which I do cover in class, in Coq)

Pierre Rousselin (Aug 28 2024 at 06:40):

Thank you @djao. This is very interesting.

1. Are you focused on modular arithmetic then?
2. Is it publicly available?
3. Aren't you afraid, that "Coq maths" will be very different than usual maths (with sets and subsets everywhere)?

djao (Aug 28 2024 at 20:29):

1. My focus is not on a particular mathematical topic, but rather teaching and learning the general process of mathematical proof and discovery. Proof assistants are very helpful because, once the software is learned, students have a "correctness oracle" that they can consult without needing instructional oversight from course staff, which greatly accelerates the mathematical discovery process. This is especially true for definitions, which are normally hard to explain in an introductory class -- Coq very directly requires a "Proof" of a definition, making it clear to students what it means to show that something is well-defined. The choice of math topics is determined simply by what topics serve as the best vehicle for teaching mathematical proof and discovery. I use integer arithmetic because it's accessible to all students (even more so than set theory) while still remaining rich enough to allow students to encounter nontrivial mathematical ideas. The core topics are the Euclidean algorithm, Bezout's theorem, unique prime factorization, and modular arithmetic up to Fermat's Little Theorem.
2. I haven't published my question sets. One reason for hesitancy is that they only really make sense in the context of the entire class, and without that surrounding apparatus to prop them up, I do not believe they stand alone.
3. Since I am teaching principles of mathematics and the process of discovery, the exact topic doesn't matter. A student who learns how to do mathematics, as a process, can easily transfer that knowledge and ability to "standard" topics or any topic whatsoever.

Michael Soegtrop (Aug 29 2024 at 07:41):

A disadvantage of using integers as introductory topic is that the formalisation of integers is trivial. Formalising the questions at hand in usable definitions is a substantial part of developing mathematics. Geometry is an area which should also be accessible to all students, but where formalisation is much less obvious. I mean there is nothing wrong in starting with integers say to teach induction, but I have doubts that the knowledge acquired this way can be easily transferred to areas which are harder to formalise.

Pierre Rousselin (Aug 29 2024 at 08:41):

Thank you @djao and @Michael Soegtrop for your interesting posts.
@Michael Soegtrop, I think @djao's approach is good for teaching rigour without having to address difficulties in maths formalization. I guess the idea is not to go further with Coq but rather to bridge the gap between highschool maths with close to no rigorous proofs or research and undergraduate maths.
Using arithmetic for that purpose is good enough: there are many existential formulas and proof schemes; natural numbers are simple enough to encourage experimenting and searching, while complicated enough to present challenging (or even unsolved) problems.

I focus on real analysis, with sequences, mostly for the same reasons, but I might try to delve more into these kinds of things this year.

djao (Aug 29 2024 at 12:14):

Formalization of integers is not trivial for this audience! Yes we can say something like "the integers are the initial object in the category of rings" but for students starting out it is incredibly hard to pin down exactly what the integers are. A good chunk of my students actually end up with the well ordering principle as their basis for formalization instead of induction.

Michael Soegtrop (Aug 29 2024 at 13:21):

Maybe my statement was a subjective exaggeration. Let me reduce my message to that one should also spent some time on teaching how to formalise things - that is also have exercises for this - and not only on teaching how to prove pre-formalised statements.

djao (Aug 29 2024 at 16:23):

100% agree that teaching how to formalize things is a necessary part of foundational mathematical education. However, I don't go about teaching this topic by way of specific exercises. Rather, what I do is I deliberately assign problems where the students need to put in some formalization work for the underlying system in order to solve them, or in some cases in order even to begin working on them. Building them implicitly into the problem feels more natural, since mathematicians after all don't normally go around formalizing things for the sake of formalization, they do so because a need arises naturally as a result of some other problem or application. For example, I might have a problem that can be stated without using inequalities (e.g. "Prove that 2 does not divide 1 in the integers") but for which a solution would require formalizing the relevant concept. (Of course, I use a ground-up reimplementation of the integers rather than the built-in ZArith package in Coq, so that the relevant concepts are not already there; the students have to work for it.)

Michael Soegtrop (Aug 30 2024 at 09:12):

@djao : that's what I meant with formalisation exercises - to think about how understood mathematical concepts can be written in Coq and what impact different ways of formalising things influences theorem statements and proofs. And indeed elementary number theory does have quite a few concepts which are at least for an introductory level sufficiently interesting to formalise.

Last updated: Oct 13 2024 at 01:02 UTC