Teach Coq first?

Stream: Lean for teaching

[Martin Dvořák]

I stumbled across: https://arxiv.org/pdf/1803.01466v1.pdf

Has it been discussed here before? It is not precisely what Kevin Buzzard used to do in his freshmen class on mathematical proving. This is for students of Computer Science, not Math; and it is using Coq, not Lean. Still, it might be a valuable input about the educational potential of Lean.

[Martin Dvořák]

It should roughly correspond to the Chapter 7 of this thesis:
https://publishup.uni-potsdam.de/opus4-ubp/frontdoor/deliver/index/docId/42379/file/boehne_diss.pdf

[Patrick Massot]

This all seems very much logic and computer science again:first order logic, propositional logic, data type, inductive data types...

[Martin Dvořák]

I should say that (but somebody should confirm it, as I am not an expert, nor did I read most of the article) I think that the students who were developing the textbook-style proofs from scratch spent much less time on the task than the students who started with proving the same theorem in Coq. Therefore, the higher score in the latter category does not necessarily reflect higher efficiency of this teaching method.

[Kevin Buzzard]

@Martin Dvořák to answer the question you raised about teaching undergraduates in their first term, the problem is that in some sense it was a failure, because the students who became engaged with the software and started using it are now all doing MSc's and PhD's -- they were the very smart ones. I wanted to help the weak ones. The other method -- learn the maths first and then try it in lean when you understand it -- we're trying to figure out if this is more successful with the average students. Another issue with maths v CS is that in the CS departments the undergraduates are not averse to using computers! This is not the case in mathematics, there are plenty of people who do not like the computing courses at all and avoid them.

[Martin Dvořák]

Thanks for the explanation!

[Kevin Buzzard]

It's also worth stressing that you do not need to use a computer at all to do most kinds of modern research in pure mathematics

[Kevin Buzzard]

I would imagine that this isn't the case for research in a CS department. Hence computers are generally less prominent.

[Martin Dvořák]

Kevin Buzzard said:

(...) it was a failure, because the students who became engaged with the software and started using it are now all doing MSc's and PhD's -- they were the very smart ones. I wanted to help the weak ones (...)

Did the weak ones learn the basics of mathematical rigor? I thought that was why Lean was amazing. They could not half-ass the proofs of the elementary statements.

[Martin Dvořák]

I am not no expert here. It just seemed to me that it was a great idea to start teaching the basics using very easy proofs but with the highest requirement for the mathematical rigor. And only later, you relaxed the requirements for the proof details, so that the students could reasonable prove more difficult theorems.

[Kevin Buzzard]

The weak ones never touched Lean, they endured me using it to prove some of the results in the course, they read the proofs in the lecture notes (which were traditional) and then some of them complained at the end that they had not paid £37000 pounds per year to come to Imperial to learn computer science.

[Arthur Paulino]

The barrier of getting a Lean environment to work properly, dealing with git, syntax errors and type theory really shows

[Martin Dvořák]

I think that having to deal with set theory instead would not be less of a hassle.

[Martin Dvořák]

That being said, I agree that the computer-related issues are a significant barrier.

[Martin Dvořák]

Kevin Buzzard said:

The weak ones never touched Lean (...)

Didn't they have to do homework in Lean?

[Martin Dvořák]

Kevin Buzzard said:

£37000 pounds per year

Is college education in Britain that expensive?!

[Kevin Buzzard]

Our job in a mathematics department is to teach the basics of mathematical rigor as soon as possible and constantly, in most of the courses which are running. This is what we do. There are no courses on hardware or compilers or how memory works -- most of the courses are just proof proof proof. We've been doing it like that for centuries. We know, and have known for ever, how to teach our students the basics of mathematical rigor, and the students in our department are already more inclined that way, and may well be averse to computers. I'm trying to stress that it is not at all clear that experiments in computer science departments can be used to draw conclusions about the students who I am told to teach.

[Alex J. Best]

RE: tuition. For non-uk students, yes. For UK the tuition is less (EU also used to pay less pre Brexit). But then you also have to factor in cost of living on top of tuition, in London which is expensive.

[Kevin Buzzard]

Martin Dvořák said:

Kevin Buzzard said:

The weak ones never touched Lean (...)

Didn't they have to do homework in Lean?

No! I would have been fired if I'd tried that! My students in my optional final year course have to do their homework in Lean, but they have self-selected. The compulsory first year introduction to proof course where I was experimenting before follows a set format which I can't fiddle with; I was offering optional extras and occasionally doing stuff in the classroom but telling them "if you're not into this, just read the proof in the course notes". And the people I attracted were the ones who already knew very very well what a proof was and could see that the software was stretching them in interesting ways.

[Kevin Buzzard]

Martin Dvořák said:

Kevin Buzzard said:

£37000 pounds per year

Is college education in Britain that expensive?!

If you're not from the UK and you're at Imperial, then yes.

[Patrick Massot]

Arthur Paulino said:

The barrier of getting a Lean environment to work properly, dealing with git, syntax errors and type theory really shows

You don't need to ask student to get a Lean environment and deal with git. What OS are you using?

[Arthur Paulino]

I've been using Linux (mostly Debian-based distros) since 2010. Do you mean it's all on gitpod?

[Martin Dvořák]

Kevin Buzzard said:

Martin Dvořák said:

Kevin Buzzard said:

The weak ones never touched Lean (...)

Didn't they have to do homework in Lean?

No! I would have been fired if I'd tried that! My students in my optional final year course have to do their homework in Lean, but they have self-selected. The compulsory first year introduction to proof course where I was experimenting before follows a set format which I can't fiddle with; I was offering optional extras and occasionally doing stuff in the classroom but telling them "if you're not into this, just read the proof in the course notes". And the people I attracted were the ones who already knew very very well what a proof was and could see that the software was stretching them in interesting ways.

I get your point. Nevertheless, I have an impression that you were talking about not having sufficient resources to comment on every student's proof. Hence the check by computer was crucial in enforcing they actually adopt the mathematical rigor.

[Patrick Massot]

Arthur, download https://www.imo.universite-paris-saclay.fr/~pmassot/mdd154/mdd154_linux.tar.gz, un pack and launch the mdd154 executable from the resulting mdd154 folder

[Patrick Massot]

You'll be running a VSCodium+Lean+mathlib+course library completely independent from your system-wide install

[Patrick Massot]

Everything is inside this folder.

[Patrick Massot]

Martin, from my experience the main help provided by Lean is not that it has no mercy, it is that it constantly displays the tactic state.

[Arthur Paulino]

Patrick Massot said:

Arthur, download https://www.imo.universite-paris-saclay.fr/~pmassot/mdd154/mdd154_linux.tar.gz, un pack and launch the mdd154 executable from the resulting mdd154 folder

This is way nicer than I was expecting! You even developed some kind of dialect inside the tactic mode

[Martin Dvořák]

Patrick Massot said:

Martin, from my experience the main help provided by Lean is not that it has no mercy, it is that it constantly displays the tactic state.

Did you ever have an impression that a student got "addicted" to seeing the tactic state all the time? To a degree that writing proofs without computer was a problem for them? I mean, emotionally problematic; not that the output of their work (without the computer) would be a bad.

[Patrick Massot]

The tactic dialect is not what I wanted to show here, but see https://github.com/PatrickMassot/lean-verbose if you're interested in that aspect

[Patrick Massot]

Martin, it's hard to tell but I don't think so

[Arthur Paulino]

And then you ask your students to zip the exos directory upload it somewhere, I suppose

[Patrick Massot]

They can download this thing for working at home, but we mostly work on this during our lab session. And then I mostly look at the proofs they write on paper after convincing Lean. Note the tactic dialect is here to make it easier to translate from Lean to paper, not the other way around

[Arthur Paulino]

Yeah I was surprised when I read it on the README file. I thought the intent was to make it easier for the students to put their thoughts in Lean

[Arthur Paulino]

It's still pretty awesome nevertheless

[Martin Dvořák]

Patrick Massot said:

The tactic dialect is not what I wanted to show here, but see https://github.com/PatrickMassot/lean-verbose if you're interested in that aspect

How difficult is it to follow the syntax of your dialect? From what I can see, there are some "commands" that consist of several words and some arguments are written in between the words (to resemble English syntax obviously).

[Patrick Massot]

It's definitely harder than normal Lean tactic, because it looks free form but isn't. That's why it would be a very bad way of making Lean easier to write, but that was never the intent.

[Damiano Testa]

In terms of the general discussion about learning mathematics by using Lean, I find that, besides proofs, an extremely important part of mathematics is developing an intuition for the concepts, to have examples and counterexamples, mental pictures and expectations.

My impression is that Lean forces you to think deeply about proofs, but I have a harder time creating an intuition by coding my way through a Lean proof.

[Arthur Paulino]

Disclaimer: I am not an expert in education science nor do I teach for living. I've only taught some young teenagers and with a small set of them, we went further and played some kind of "convincing game", where I motivated them to come up with arguments to convince the group of some simple results.

After an unpretentious quick read on the work Martin posted above, their experiments didn't have the goal to capture what I was expecting. I was thinking more in terms of a test/control experiment with different treatments in order to evaluate the students' abilities regarding proof writing afterwards.

The randomly assigned treatments being:
A: exposure to formal proofs
B: traditional teaching

[Martin Dvořák]

What happens on this line, please?
https://github.com/PatrickMassot/lean-verbose/blob/4166b4e1517babc52b3bbe092f16aa6e9400dde6/test/sample.lean#L90
@Patrick Massot

[Martin Dvořák]

Ah, I got it.

[Kevin Buzzard]

I think Paola Iannone is still very interested in this stuff. She's organising a meeting in Loughborough later this year which I'll go) and is working with Gihan Marasingha on his students in Exeter. She has a PhD in algebraic geometry and now works in education, and was one of the authors of the paper which analysed my efforts

[Arthur Paulino]

@Kevin Buzzard would you mind sharing the paper?
Is it this one? Learning about proof with the theorem prover LEAN: The abundant numbers task

[Arthur Paulino]

The paper is really well done!
There is indeed the problem of self-selection bias.

One way out is to find volunteers by saying "you may or may not be chosen to use Lean" and then split the group randomly among those. This way the issue of expecting some students to use the tool against their will doesn't come into play. Although there may be some bias related to the frustration of volunteering and not being chosen to learn Lean, since the Lean volunteers seem to be the smartest ones (and probably the hungriest).

I'm looking forward to incoming studies and results!

[Notification Bot]

7 messages were moved from this topic to #Lean for teaching > Waterproof: educational software for learning how to writ... by Heather Macbeth.