David Mumford says we should replace plane geometry with programming and I’m not sure he’s wrong

MAA Mathfest is in Madison this week — lots of interesting talks about mathematics, lots of interesting talks about mathematics education.  Yesterday morning, David Mumford gave a plenary lecture in which he decried the lack of engagement between pure and applied mathematics — lots of nodding heads — and then suggested that two-column proofs in plane geometry should be replaced with basic programming — lots of muttering and concerned looks.

But there’s something to what he’s saying.  The task of writing a good two-column proof has a lot in common with the task of writing a correct program.  Both ask you to construct a sequence that accomplishes a complicated goal from a relatively small set of simple elements.  Both have the useful feature that there’s not a unique “correct answer” — there are different proofs of the same proposition, and different programs delivering the same output.  Both quite difficult for novices and both are difficult to teach.  Both have the “weakest link” feature:  one wrong step means the whole thing is wrong.

Most importantly:  both provide the training in formalization of mental process that we mathematicians mostly consider a non-negotiable part of general education.

But teaching coding instead of two-column proofs has certain advantages.  I am not, in general, of the opinion that everything in school has to lead to employable skills.  But I can’t deny that “can’t write five lines of code” closes more doors to a kid than “can’t write or identify a correct proof.”  People say that really understanding what it means to prove a theorem helps you assess people’s deductive reasoning in domains outside mathematics, and I think that’s true; but really understanding what it means to write a five-line program helps you understand and construct deterministic processes in domains outside a terminal window, and that’s surely just as important!

Computer programs are easier to check, for the teacher and more importantly the student — you can tell whether the program is correct by running it, which means that the student can iterate the try-check-fail-try-again process many times without the need for intervention.

And then there’s this:  a computer program does something.  When you ask a kid to prove that a right triangle is similar to the triangle cut off by an altitude to the hypotenuse, she may well say “but that’s obvious, I can just see that it’s true.”  And she’s not exactly wrong!  “I know you know this, but you don’t really know this, despite the fact that it’s completely clear” is a hard sell, it devalues the geometric intuition we should be working to encourage.

 

 

 

 

 

 

“The rest of the world was uncertain what had been proven and what not.”

Until a minute ago I had never heard of Mizar, a project to record as much mathematics as possible in computer-readable form.  The pieces of this project are published in the Journal of Formalized Mathematics.  Here, for instance, is the paper “Non-negative Real Numbers, part I.”

I learned about Mizar when glancing through the publicly available archive of QED, a mailing list from the early 90s devoted to the formalization of mathematics.  It’s interesting to be reminded just how excited people were about the prospects of computerizing large precincts of mathematical practice, an ambition which as far as I can tell has now receded almost entirely from view.

I found the QED archive, in turn, via Math Overflow, which quoted these pointed remarks of Mumford about algebraic geometry in the Italian style:

The best known case is the Italian school of algebraic geometry, which produced extremely good and deep results for some 50 years, but then went to pieces. There are 3 key names here — Castelnuovo, Enriques and Severi. C was earliest and was totally rigorous, a splendid mathematician. E came next and, as far as I know, never published anything that was false, though he openly acknowledged that some of his proofs didn’t cover every possible case (there were often special highly singular cases which later turned out to be central to understanding a situation). He used to talk about posing “critical doubts”. He had his own standards and was happy to reexamine a “proof” and make it more nearly complete. Unfortunately Severi, the last in the line, a fascist with a dictatorial temperament, really killed the whole school because, although he started off with brilliant and correct discoveries, later published books full of garbage (this was in the 30’s and 40’s). The rest of the world was uncertain what had been proven and what not. He gave a keynote speech at the first Int Congress after the war in 1950, but his mistakes were becoming clearer and clearer. It took the efforts of 2 great men, Zariski and Weil, to clean up the mess in the 40’s and 50’s although dredging this morass for its correct results continues occasionally to this day.

Readers with good memories will recall that this is the second time I’ve quoted uncomplimentary remarks about Severi.