Next week with Micaela Mayero and @Pierre Rousselin we will be tutoring 1st year high-school students and having hands-on Coq sessions with them. Is there anyone here who tried that ? We would be grateful for any kind of feedback if there is some.

Do you mean "des élèves de seconde" !? :flushed:

Julien Puydt said:

Do you mean "des élèves de seconde" !? :flushed:

Yes, from high-schools near Villetaneuse. The idea is push them into scientific studies before they make a restricting choice.

This is brave. I have a friend who is teaching to "secondes" and the ~~most difficult~~ only proof he's asked for in their first exam was "Prove that the sum of two even numbers is even." And only a few students actually did it.

We won't be doing any formalization, only playing with logical connectors.

Well, even that looks so above what they do...

Good luck!!!

If you have some material, I'd like to try it on my last son...

Julien Puydt said:

If you have some material, I'd like to try it on my last son...

Not yet, but we'll let you know

IMHO it is a good thing to do this. I have the impression that usual math education really never comes to the point what math really is. Even in university the teachers somehow assume that students have an understanding of some sort of grown and not written down codex. I find that Coq does a good job in teaching these basics.

An anecdote around this: one of my sons asked in 4th form elementary school if the distributive law of natural numbers is something "defined or naturally true". I showed him then how to define natural numbers addition and multiplication in Coq and how to prove the distributive law. Of course he did not understand the proofs and only had a rough idea (but still some idea) of the definitions of addition and multiplication, but he clearly did understand when one defines numbers, addition and multiplication in the way we did, that the distributive law follows from it.

Disclaimer: this is my physicists view on things ...

I have experience teaching discrete math using Coq through ProofWeb (http://carol.dimap.ufrn.br/proofweb/) to first year bachelor students. Though not the same audience they are also not what I would define as mature. Yet, around 50% do their exercises in logic through ProofWeb and enjoy it (I make it optional and not a requirement for the course). Don't underestimate how much students are used to software tools nowadays for solving their math homework!

I have experienced teaching logic with coq using some self written coq equivalent to the first chapters of a logic book(I would maybe use logical foundation now although the presentation used was slower). I defined formulas as an inductive type and start from there.

It was for adults with no background (some had no background in programming).

Overall I had no more or less success than with a standard logic book, but it was fun.

A few remarks:

- having two layers of logical connectives (coq ones and the inductive of formulas) was not a problem. I was careful to use different notation for each level and it went surprisingly well.
- the chapter that was most successful was the one where I defined ltac for each tableau deduction rules and have them solve exercises with it. So I guess this is something to dig: make the effort of implementing tactics dedicated for exercises.

I wonder what the goal of a high school course should be: teaching logic as such or teaching what rigorous math looks like. For the latter I would say using CIC as foundation might be better than using classical logic because CIC is IMHO more impressive to beginners with more "Aahs and Oohs" than classical logic. Say the fact that the induction principle on natural numbers is just an ordinary function and not something magic is an eye opener for how CIC and with it. "a" foundation of math works. I find it hard to find similar instructive examples in classical logic. In a way I have the impression that CIC is more "hands on" and ready to use for something interesting than classical logic, because in classical logic one needs quite a few axioms to do something useful, and I believe that this is what most beginners struggle with most - somehow get a grasp on what kind of foundations they stand on. Classical logic more feels like an excavation site where the foundations are deeply buried, while CIC is more like a steel construction with clearly visible features.

Again, this is a physicists view on math and logic, but it might be closer to what high school students think than the view of educated mathematicians.

I think logic by itself is not important. Well it *is* important to teach logic in high school imho but I was only considering as an example of a subject that you can define quite simply from scratch (leaving fundational considerations for later). I guess an argument against CIC in high school is that understanding CIC is difficult and we would avoid explaining how it really works. You would end up with something as magical and wrongly considered as "given by nature" than usual math approaches. What I like with logic (or any subject you can study from the start) is that we can show that math is *first* about defining things from the beginning *and then* reason about it.

(and of course we omit the fact that the initial definition needs to take place in some predefefined math universe...)

Interesting approach to use proofs on HS, while I do not think it will pan out (students would likely deem it as waste of time).

Pierre Courtieu said:

What I like with logic (or any subject you can study from the start) is that we can show that math is

firstabout defining things from the beginningand thenreason about it.

The question is how much you have to add on top of the foundations so that you get something high school students show some genuine interest in.

Of course the formal definition of CIC is complicated, but I don't think one needs an understanding beyond Curry-Howard to see how it does work as a foundation.

I see that I am saying that one should teach mathematical rigour by not looking with rigour at the foundations and yes this is questionable (physicists ...). But then I don't see how to teach rigour to high school students starting with ZF. You simply can't span the gap between a solid understanding of foundations and something interesting in a high school course. Maybe logic and SAT solvers might work.

@abab9579 : I don't think so - one can explain that the world we live in is technically so complicated that proves might be the only way to stay on top of technology.

Michael Soegtrop said:

I wonder what the goal of a high school course should be: teaching logic as such or teaching what rigorous math looks like. For the latter I would say using CIC as foundation might be better than using classical logic because CIC is IMHO more impressive to beginners with more "Aahs and Oohs" than classical logic. Say the fact that the induction principle on natural numbers is just an ordinary function and not something magic is an eye opener for how CIC and with it. "a" foundation of math works. I find it hard to find similar instructive examples in classical logic. In a way I have the impression that CIC is more "hands on" and ready to use for something interesting than classical logic, because in classical logic one needs quite a few axioms to do something useful, and I believe that this is what most beginners struggle with most - somehow get a grasp on what kind of foundations they stand on. Classical logic more feels like an excavation site where the foundations are deeply buried, while CIC is more like a steel construction with clearly visible features.

Again, this is a physicists view on math and logic, but it might be closer to what high school students think than the view of educated mathematicians.

For us, it's not really a course but a few practical sessions with no evalution in mind. The goal is to give them a first taste of logic and of what proving things looks like.

Michael Soegtrop: I mean, saying that would not be very convincing to the high schoolers. They had only limited exposure to the world yet.

To give a bit of context to the non-French people of this thread, Villetaneuse is also a very special kind of city. It's a very poor area, with a very young population (40% < 30 y.o.), many of whom are first-generation immigrants (35% pop., and second-generation is probably a lot more). Those students are likely to have had even *less* exposure to the world than the average French highschooler.

for the class breaks, may I recommend the Coqoban game on top of jsCoq? https://coq-next.vercel.app/fun/coqoban.html

@Pierre-Marie Pédrot : thanks for the context! Actually I have a little bit of experience teaching robotics (building and programming little autonomous robots) in a Bavarian "Mittelschule" where most of the kids become craftsmen after school (you need a master in a craft before you can go to university with this education). I would say as long as one does such a course such that it depends more or smartness and genuine curiosity than on acquired knowledge, you can find kids which can master such things (or fail miserably) everywhere. But indeed the topic must be well adjusted to the intended audience.

@abab9579 : I would say that high school kids depend very much on technology today and it doesn't take much to make them aware of what this means.

@Marie Kerjean : how many sessions of what length do you plan for? Something like 4 afternoons (3 hours)?

Michael Soegtrop said:

Marie Kerjean : how many sessions of what length do you plan for? Something like 4 afternoons (3 hours)?

3 morning session of 3 hours each, we'll have lunch together and other activities in the afternoon.

Karl Palmskog said:

for the class breaks, may I recommend the Coqoban game on top of jsCoq? https://coq-next.vercel.app/fun/coqoban.html

Cool project :) do you think that a similar approach could be used to implement a tool like ProofWeb in jsCoq? like have a custom predicate that links the current goal to the AST of the proof tree being built and then a pretty printer in JS?

@Marie Kerjean : I see. And shall the goal be mathematical or technical? There might be technical topics doable in that time where you can do two groups where one is supposed to make a safe system and the other is supposed to break into it (both using similar methods). I have something in mind which is quite easy to spec but quite hard to get right or break into without proofs, but I haven't done it in Coq yet - need to see how accessible this would get. In case this is something you are interested in, please let me know and I can think about it.

I'm a 2nd year college student. I can offer my view as a person who started learning this stuff since grade 12. I find formal verification really fun and addictive. I believe that other high school students are likely to be hooked. If you are friendly and patient, you will be quite successful. I love the initiative and I want this to succeed.

Alessandro Bruni said:

Karl Palmskog said:

for the class breaks, may I recommend the Coqoban game on top of jsCoq? https://coq-next.vercel.app/fun/coqoban.html

Cool project :) do you think that a similar approach could be used to implement a tool like ProofWeb in jsCoq? like have a custom predicate that links the current goal to the AST of the proof tree being built and then a pretty printer in JS?

Something like the ProofWeb proof tree could definitely be visualized in some way using jsCoq. I'd recommend to start from something like https://github.com/hendriktews/proof-tree and then add graphical stuff on top...

Just to let you know it worked quite well, for propositional logic and the formalization of easy problems. The (perfectible, cleaned version to be uploaded, in french) subjects are on @Pierre Rousselin webage : https://www.math.univ-paris13.fr/~rousselin/enseignement.html

@Pierre Rousselin please consider putting the Coq files under an explicit open source license, so others can possibly translate and reuse

(incidentally, putting the files on a platform like GitHub also would simplify discovery)

Karl Palmskog said:

Pierre Rousselin please consider putting the Coq files under an explicit open source license, so others can possibly translate and reuse

I'll do that (coming from math, I usually do not care and just say "do whatever you want with this").

ah, there are licenses that effectively say "do whatever you want", but in some cases this means the code can't be used in some contexts (without relicensing). If you use permissive license like we recommend here, that leads to the least trouble: https://github.com/coq-community/manifesto#best-practices

Karl Palmskog said:

(incidentally, putting the files on a platform like GitHub also would simplify discovery)

Sorry, but I'm not very comfortable with the idea of training microsoft's AI or doing anything related with this company.

fine by me, but there is also GitLab, for example (our main goal is usually preservation, like here)

Karl Palmskog said:

fine by me, but there is also GitLab, for example

I will consider it, thanks. Ideally, I would like to keep things uncentralized.

However, this is outside the main topic. The fact is that it is possible to teach intuitionist logic to 14 year-old pupils and coq is a great tool for this. All pupils said (and there was no grade or any pressure) that it was fun and interesting. They were doing it during their holidays ! They worked all the time during the sessions. I used to be a high school maths teacher, and I know that it is rare. In France, after a Bourbaki backlash, it is usually said that formalism and logic for itself should be avoided in high school (and even in university). I am more and more convinced of the opposite. It is hard to play a game if you don't know its rules.

The files are now under the GNU Lesser General Public License version 3.

for the "other" perspective on teaching Coq to undergrads and younger students: https://sites.math.rutgers.edu/~zeilberg/Opinion184.html

COQ and Lean continue the pernicious Greek tradition, that introduced the axiomatic method and made mathematics a deductive, logic-centric science. By inertia, the Euclidean axiomatic approach continues to this day.

But what truly got me scared is that, a few months ago, I heard a talk about using Lean and Coq in undergraduate math classes. The current math curriculum is already bad enough, indoctrinating our students in Greek-style math, but harnessing Lean and Coq in "Introduction to Proofs" classes, is really going too far.

it seems he gives teaching Coq for program verification a free pass ( :relief:):

computerized logic, while definitely very useful in software engineering, for verifying program-correctness, has no place in [...] mathematics

There is unfortunately an absence of argument in this very short piece, so it's hard to know if there is any insight to derive from this strange opinion.

more background here: https://sites.math.rutgers.edu/~zeilberg/Opinion94.html

I concede that "formal proofs" are not completely without interest. It is a nice game that computational logicians like to play, and it does have its uses in applied software development, in testing program-correctness, in addition to (not instead!) empirical tests. Also, it is nice that a few theorems, like 4CT, would have a completely formal proof, since Euclideanism is still the dominant religion at the early 21st century. But enough is enough. It was funny the first time, and just like the 3000th proof that a certain problem is NP-hard, the law of diminishing returns will hit very soon.

anyway, I don't agree with the view, but probably goood for people who teach Coq+math to be aware of this argument ("computerized math is a useless game"). Rob Arthan of HOL/ProofPower fame gave a response here.

May I point out that every time someone fancies getting rid of "euclideanism" (which is: rigor), catastrophic failures ensue?

I think the most interesting part in this piece is:

Real mathematics is (or at least should be) algorithmic. The axiomatic method is like machine language or a Turing machine or a Tuxedo. It is very stifling. The logicist approach that takes several hundred of pages to prove that 1+1=2 is ridiculous.

and it clearly demonstrates that the author has no idea what Coq is about, since it actually aligns quite well with their goal of making mathematics algorithmic again...

IMHO the only real argument in the recent post is positive for using Coq:

Current, human-generated, mainstream mathematics is the way it is because it is an artifact of the historical fact that computers were invented recently.

Doesn't this say that "Current, human-generated, mainstream mathematics" would like quite different if the ancient greeks already had Coq?

The argument:

go back to the much more fruitful tradition, that of ancient Egypt, Babylon, China, India, Persia, and Arabia

neglects the fact computers exist. Working with such algorithms is just fine if numeric math is done pencil and paper by humans which realise when things go wild. If such algorithms are executed by computers which don't reflect on what they are doing, these methods don't work any more - at least not always. The problem is that the failure rate dramatically increases if more and more numeric maths is done. II one does such computations once a week by a few members of a small elite, 99.99% is pretty close to perfect. If one does such computations once per millisecond in a single device of which 100 million exist on the planet, 99.99% is many orders of magnitude away from sufficient.

Théo Zimmermann said:

I think the most interesting part in this piece is:

Real mathematics is (or at least should be) algorithmic. The axiomatic method is like machine language or a Turing machine or a Tuxedo. It is very stifling. The logicist approach that takes several hundred of pages to prove that 1+1=2 is ridiculous.

and it clearly demonstrates that the author has no idea what Coq is about, since it actually aligns quite well with their goal of making mathematics algorithmic again...

Yes this is very strange. I think he is personally a heavy user of C.A.S. systems.

He's actually kinda famous for crediting his computer+Maple CAS as a coauthor in his papers (as "Shalosh B. Ekhad").

Last updated: Jan 28 2023 at 06:30 UTC