Marie Kerjean (Oct 19 2022 at 07:56): Marie Kerjean (Oct 19 2022 at 07:56):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.
Julien Puydt (Oct 19 2022 at 07:58):Do you mean "des élèves de seconde" !? :flushed:
Marie Kerjean (Oct 19 2022 at 07:59):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.
Théo Zimmermann (Oct 19 2022 at 07:59):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.
Marie Kerjean (Oct 19 2022 at 08:00):We won't be doing any formalization, only playing with logical connectors.
Julien Puydt (Oct 19 2022 at 08:00):Well, even that looks so above what they do...
Théo Zimmermann (Oct 19 2022 at 08:01):Good luck!!!
Julien Puydt (Oct 19 2022 at 08:06):If you have some material, I'd like to try it on my last son...
Marie Kerjean (Oct 19 2022 at 08:08):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
Michael Soegtrop (Oct 19 2022 at 08:24):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.
Michael Soegtrop (Oct 19 2022 at 08:29):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.
Michael Soegtrop (Oct 19 2022 at 08:30):Disclaimer: this is my physicists view on things ...
Alessandro Bruni (Oct 19 2022 at 09:04):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!
Pierre Courtieu (Oct 20 2022 at 07:26):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:
Michael Soegtrop (Oct 20 2022 at 07:52):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.
Pierre Courtieu (Oct 20 2022 at 09:09):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.
Pierre Courtieu (Oct 20 2022 at 09:39):(and of course we omit the fact that the initial definition needs to take place in some predefefined math universe...)
abab9579 (Oct 20 2022 at 09:42):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).
Michael Soegtrop (Oct 20 2022 at 10:45):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 first about defining things from the beginning and then reason 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.
Michael Soegtrop (Oct 20 2022 at 10:49):@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.
Marie Kerjean (Oct 20 2022 at 15:17):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.
abab9579 (Oct 21 2022 at 01:53):Michael Soegtrop: I mean, saying that would not be very convincing to the high schoolers. They had only limited exposure to the world yet.
Pierre-Marie Pédrot (Oct 21 2022 at 06:49):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.
Karl Palmskog (Oct 21 2022 at 06:55):for the class breaks, may I recommend the Coqoban game on top of jsCoq? https://coq-next.vercel.app/fun/coqoban.html
Michael Soegtrop (Oct 21 2022 at 07:53):@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.
Michael Soegtrop (Oct 21 2022 at 07:54):@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.
Michael Soegtrop (Oct 21 2022 at 08:08):@Marie Kerjean : how many sessions of what length do you plan for? Something like 4 afternoons (3 hours)?
Marie Kerjean (Oct 21 2022 at 08:16):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.
Alessandro Bruni (Oct 21 2022 at 08:58):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?
Michael Soegtrop (Oct 21 2022 at 10:24):@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.
Huỳnh Trần Khanh (Oct 21 2022 at 14:46):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.
Karl Palmskog (Oct 22 2022 at 08:43):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...
Marie Kerjean (Oct 27 2022 at 10:54):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
Karl Palmskog (Oct 27 2022 at 13:16):@Pierre Rousselin please consider putting the Coq files under an explicit open source license, so others can possibly translate and reuse
Karl Palmskog (Oct 27 2022 at 13:18):(incidentally, putting the files on a platform like GitHub also would simplify discovery)
Pierre Rousselin (Oct 27 2022 at 18:56):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").
Karl Palmskog (Oct 27 2022 at 18:58):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
Pierre Rousselin (Oct 27 2022 at 18:58):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.
Karl Palmskog (Oct 27 2022 at 18:59):fine by me, but there is also GitLab, for example (our main goal is usually preservation, like here)
Pierre Rousselin (Oct 27 2022 at 19:02):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.
Pierre Rousselin (Oct 27 2022 at 19:13):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.
Pierre Rousselin (Nov 05 2022 at 09:22):The files are now under the GNU Lesser General Public License version 3.
Karl Palmskog (Jan 03 2023 at 14:15):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.
Karl Palmskog (Jan 03 2023 at 14:17):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
Théo Zimmermann (Jan 03 2023 at 14:25):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.
Karl Palmskog (Jan 03 2023 at 14:26):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.
Karl Palmskog (Jan 03 2023 at 14:31):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.
Julien Puydt (Jan 03 2023 at 14:32):May I point out that every time someone fancies getting rid of "euclideanism" (which is: rigor), catastrophic failures ensue?
Théo Zimmermann (Jan 03 2023 at 14:40):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...
Michael Soegtrop (Jan 04 2023 at 11:11):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.
Patrick Nicodemus (Jan 05 2023 at 03:00):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.
Alexander Gryzlov (Jan 05 2023 at 14:03):He's actually kinda famous for crediting his computer+Maple CAS as a coauthor in his papers (as "Shalosh B. Ekhad").
Matthieu Sozeau (Feb 09 2023 at 18:12):I was scared for a moment it was Noam Zeilberger writing this, but you can see his perfect response at the end of it. Phew ;)
Last updated: Oct 13 2024 at 01:02 UTC