Are freshmen ripe for formal proofs?

Stream: Lean for teaching

[Johan Commelin]

I've just read the fabulous "Mathematician's lament" again: https://www.maa.org/external_archive/devlin/LockhartsLament.pdf
The author strongly makes the point that every mathematician is well aware of: a proof tells a story, it should explain an idea. The "formal" proofs of high school geometry are typically the only places where students are exposed to discovering proofs, as opposed to mere rote computations. The author asserts that formal proofs have their place. They should be used whenever there is a crisis, whenever there is a paradox, when our intuition doesn't suffice.
In particular, students should first do lots of freestyle exploration before being exposed to formal proofs.

I think I agree with most of what the author says. Given the current state of our high school curricula, this means that we get freshmen at university that don't know what maths is about, and that don't know what a proof is supposed to be.

I know for a fact that I find it extremely annoying to grade Linear Algebra exams that are full of sentences that don't typecheck. Coming from that angle, it is very natural to teach students Lean in their first semester, so that at least they are aware of what it means to prove something, and to write down meaningful formulas.

On the other hand (and I had not yet appreciated this so much before) the author claims that these students are in fact not yet ripe for formal proofs. They should first learn to play and run and leap and fall and scramble and climb in the world of mathematics before destroying the proofs by formalised accounts of their adventures.

I'm quite curious about your opinions on these issues.

[Scott Morrison]

I'm not sure that formalisation is actually the enemy of "to play and run and leap and fall and scramble and climb".

The enemy is teaching people "the quadratic formula" and asking them to use it over and over again. One should learn to use the quadratic formula only in service of learning why there is such a formula, roughly its shape (which sometimes matters), and how in most subsequent instances to ask a computer to do it for you.

Similarly for Gaussian elimination --- teaching what it really says, what you can expect to gain from it, when it's a relevant tool, how to ask the computer to do it for you, and why the computer sometimes gives silly answers, are all more helpful that drilling people to be able to do it on an exam with some contrived explicit matrix. (I'm as much to blame as anyone here; I've done the wrong thing here too many times, without the energy to rewrite courses, get sign-off from other departments, etc, etc.)

I'm fully aware that students handed a theorem prover have an unfortunate tendency to blindly bash their way around (I succumb to the same temptation too often). But they're still doing something fantastic --- they're exploring and communicating (at least with the computer) and hitting their head against difficult things and hopefully learning something.

Finally, at the end of the day, we don't use (should not use?) interactive theorem provers because we're worried about rigour, and want to pin down all our proofs like lifeless butterflies. They're here (they're coming?) because, just like computer algebra systems, they are (will, hopefully, one day be?) tools that will let us explore more quickly and more freely.

[Scott Morrison]

For anyone who hasn't read Lockhart's Lament (linked above), please do. It has some gems:

All metaphor aside, geometry class is by far the most mentally and emotionally destructive
component of the entire K-12 mathematics curriculum. Other math courses may hide the
beautiful bird, or put it in a cage, but in geometry class it is openly and cruelly tortured.
(Apparently I am incapable of putting all metaphor aside.)

[Scott Morrison]

Lockhart has some strong words for us:

This is what comes from a misplaced sense of logical rigor: ugliness. The spirit of the argument has been buried under a heap of confusing formalism.

[Johan Commelin]

Right. It was quotes like that, that made me start this thread.
I think that I generally agree with what you said, @Scott Morrison. The promise of ITP is clearly there. But how do we strike the right balance in practice, when teaching freshmen (or anyone else for that matter)? It's maybe even more difficult than redesigning a linear algebra course to get rid of contrived matrix exercises.

[Kevin Buzzard]

Teaching mathematics to K-12 is very different to what we are doing. The article is bemoaning teaching at schools, where maths is compulsory and many people loathe it. My personal take on the issue (and I have some unfinished essay on the subject somewhere which I wrote shortly after getting into this business) is that truth and beauty are two different things, and whilst Lockhart is lamenting the fact that truth is trampling all over beauty at school, my concern is that beauty is trampling over truth at research level.

[Johan Commelin]

Sure. But that doesn't mean that freshmen (who were "prepared" by K-12) are "ready" for formal proofs. I'm not saying they aren't either. I'm just curious about which pitfalls there are, and how to find the right balance in teaching. I'm definitely convinced that there is a place for formal proofs in research maths.

[Patrick Massot]

This kind of essay is fun to read, but taking it too seriously makes enormous damage. In France this idea that kids should discover everything by themselves rather than being taught anything is everywhere, and it's a complete disaster.