There are areas of mathematics for which proof assistants do a much better job; here is an interesting presentation using the theorem prover Coq as a virtual TA for discrete math: http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA-ITP.pdf
I want to take objection to the presentation of your example. It should be contextualized with the first chapter of Spivak's textbook, where he talks about algebraic properties of addition and multiplication for "numbers" (which aren't particularly well defined, but ostensibly since this is a Calculus textbook they are actually real numbers.) You can do these proofs fairly straightforwardly with rewrite rules, and proof assistants actually have rather good support for this. (The real difficulty shows up when you get to more complicated theorems, when we'd like to sweep rigor a little bit under the rug.) Look at the end of this book chapter for an exercise which asks the user to teach a proof assistant how to automatically show many simple properties of groups http://adam.chlipala.net/cpdt/html/LogicProg.html
I'll read that presentation when I get back. First impression: the author needs to learn about luminance as it applies to readability! Blue text on black background == headache.
When you say "do a better job" what do you mean? I'd love to see papers about it.
And yes, in that chapter you learn the field axioms and it's fairly straightforward for a computer to verify the statement given you present it to the computer in the correct way.
That's my point, and I think Dan's point, too. Mathematicians don't do math that way.
Like I said: "If you see that and think "That's easy enough to express in a way a computer understands, and there are proof verification systems" you're missing the point."
As for http://adam.chlipala.net/cpdt/html/LogicProg.html, it looks relatively foreign to me. I'm going to read through it and figure it out, but would it helpful for a first-year college student who went from AP Calculus the previous year to Spivak's Calculus the next to be spending their time on logic programming?
They've probably never even heard the word "lemma."++ It assumes you're at least a little proficient with the language of mathematics.
Pointing to things like Coq as a solution is like telling an average computer user, "Why use Dropbox when you can just use rsync and some shell scripts?"
It might be the basis for something better designed, but it's only part of a larger, hitherto undiscovered, solution.
++: I'm describing my experience. Spivak was the first time I was introduced to the proof-as-exercise paradigm that's the cornerstone of every higher-math textbook.
Proof assistants have close ties to logic and type theory, so it's not much surprise that they're quite good for doing this small, subarea of mathematics. (Indeed, I think in the not too distant future we will be teaching logic using something like an interactive theorem prover. It makes a bit of the formalism quite clearer.) There has been some push, especially in Europe, for using these programs to prove other mathematics; it is certainly possible, although few would say it is pleasant or resembles how ordinary mathematicians work. But I think that, for specific areas of mathematics, these tools are useful today. Especially when trying to teach students how to think formally; you'll find that formal corresponds closely to how the computer thinks about things (and the whole problem is that mathematicians are not very formal at all.)
I just went through the presentation. It's an interesting experiment, but seems completely unsuitable for teaching the example I gave from Spivak to a first-year college student with no prior exposure to CS or formal mathematics.
It might be useful to someone who has a extensive background in functional programming, but it's in a completely different universe than the one most mathematicians live in.
I agree that at this point, it's completely unsuitable for the staples of college mathematics (e.g. calculus, differential equations), although it was not clear non-mathematicians were being subject to any sort of rigor anyway.
That said, these tools have been used to teach Freshmen CS majors, and to reasonably good effect.
I want to take objection to the presentation of your example. It should be contextualized with the first chapter of Spivak's textbook, where he talks about algebraic properties of addition and multiplication for "numbers" (which aren't particularly well defined, but ostensibly since this is a Calculus textbook they are actually real numbers.) You can do these proofs fairly straightforwardly with rewrite rules, and proof assistants actually have rather good support for this. (The real difficulty shows up when you get to more complicated theorems, when we'd like to sweep rigor a little bit under the rug.) Look at the end of this book chapter for an exercise which asks the user to teach a proof assistant how to automatically show many simple properties of groups http://adam.chlipala.net/cpdt/html/LogicProg.html