why it sucks to write proofs (by hand)
Dec. 1st, 2003 03:36 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslSo I just finished my take-home exam for modal logic. This week I probably did more "serious" proofs than the whole year put together.
But I absolutely hate doing proofs of this kind, and I remember why I got tired of doing math: it takes me hours and hours to get through with it. I am normally a slow thinker (maybe because I am thorough? maybe because I try hard to integrate it to my existing concepts?), but such slowness of proving things surely has to do with disorganization, and maybe (I'm starting to think) with having a short working memory. I absolutely need to write things down. If you want me to buy you three things at the grocery store, I need to write them down. Perhaps it is this, not ADD, that is to blame for my low productivity: I have a small RAM.
In this assignment, like most math assignments I remember, I found myself writing the same proof patterns over and over again. On all problems, using the techniques from Exner's book gets you very far: work out examples, work out non-examples; prove specific cases first and then generalize; don't try to prove it in one go, etc. Also, don't forget to try both backward chaining and forward chaining: some proofs are much easier with backward chaining. But either way, writing proofs is a pain in the ass, because it's too much information to have in my head at one time, so I have to manage everything in one piece of paper (or more). By the end of my assignment, I was begging for a proof assistant. I really think this would be a good idea: many, many people would be better off by having a piece of software help them organize their proofs. I do not want to be a specialist in syntactic manipulation: my Palm Pilot could do a better job.
Why are we expected to do such complicated processing on paper? I think the mathematicians of the future will remember today's mathematicians the same way we remember people who used to complicated calculations with pencil and paper and the occasional slide rule.
So, let me ask you expert provers, how do YOU do your proofs? What % of the time (and steps) do you spend on mechanical things, and what percentage is "intelligent" or "creative" work? When you're bored with having to write every little step, how much do you skip while still trying to keep the proof clear? Am I exceptional in wanting computerized help? It simply seems silly to try to learn to prove these "deep" theorems all by yourself, when you can do it much more quickly with the help of a machine.
NB: This is not about "theorem-proving" or "automated reasoning" systems. It's about "things that make us smart", tools to enhance our intelligence, although such proof assistants could use some from the above techniques. Afterall, the best systems are the ones which integrate human & computer intelligence.
But I absolutely hate doing proofs of this kind, and I remember why I got tired of doing math: it takes me hours and hours to get through with it. I am normally a slow thinker (maybe because I am thorough? maybe because I try hard to integrate it to my existing concepts?), but such slowness of proving things surely has to do with disorganization, and maybe (I'm starting to think) with having a short working memory. I absolutely need to write things down. If you want me to buy you three things at the grocery store, I need to write them down. Perhaps it is this, not ADD, that is to blame for my low productivity: I have a small RAM.
In this assignment, like most math assignments I remember, I found myself writing the same proof patterns over and over again. On all problems, using the techniques from Exner's book gets you very far: work out examples, work out non-examples; prove specific cases first and then generalize; don't try to prove it in one go, etc. Also, don't forget to try both backward chaining and forward chaining: some proofs are much easier with backward chaining. But either way, writing proofs is a pain in the ass, because it's too much information to have in my head at one time, so I have to manage everything in one piece of paper (or more). By the end of my assignment, I was begging for a proof assistant. I really think this would be a good idea: many, many people would be better off by having a piece of software help them organize their proofs. I do not want to be a specialist in syntactic manipulation: my Palm Pilot could do a better job.
Why are we expected to do such complicated processing on paper? I think the mathematicians of the future will remember today's mathematicians the same way we remember people who used to complicated calculations with pencil and paper and the occasional slide rule.
So, let me ask you expert provers, how do YOU do your proofs? What % of the time (and steps) do you spend on mechanical things, and what percentage is "intelligent" or "creative" work? When you're bored with having to write every little step, how much do you skip while still trying to keep the proof clear? Am I exceptional in wanting computerized help? It simply seems silly to try to learn to prove these "deep" theorems all by yourself, when you can do it much more quickly with the help of a machine.
NB: This is not about "theorem-proving" or "automated reasoning" systems. It's about "things that make us smart", tools to enhance our intelligence, although such proof assistants could use some from the above techniques. Afterall, the best systems are the ones which integrate human & computer intelligence.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
(no subject)
Date: 2003-11-30 07:19 pm (UTC)As far as how to do it well. At least if it's a problem that's at all interesting, I find it much more an art than a science. I enjoy proving things because there's a creative problem solving feel to it and I feel like I'm gaining insight into the problem.
If you're doing one of these hideous 900 case proof by induction on derivations or formulas or some such thing, I can understand why you hate it, since those are very tedious. I think it would be better of people teaching material to ask questions like given some hypothesis X, tell why it fails inductively, etc.. But maybe those kinds of question just aren't my thing.
(no subject)
Date: 2003-11-30 07:41 pm (UTC)Yeah, it's a great feeling to get insight into a problem. In fact, I had a little moment of joy during this assignment when I figured out an interesting problem, but it was overshadowed by the amount of wasted time.
Perhaps I go into automatic mode when I start rewriting things neatly in "proof form". I copy a bunch of writing I did which I don't want to lose (so I don't have to think again), but on other hand, I become a symbol-manipulating machine (and a terribly slow one).
Ironically, if I weren't so lazy, maybe I wouldn't be afraid of figuring the problem out several times, in progressively better drafts (better understanding), my proofs would be more joyful and faster, and I would understand the proof better.
Once I learn TeX, maybe I'll write my proofs straight into the computer and save myself the work of writing things down many times.
On average how many pages of scratch paper per pages of proof do you write?
(no subject)
Date: 2003-12-02 12:04 am (UTC)I use scratch paper sometimes when I'm first working out a proof, if I'm sure I'll just need to get a general overview, or if I have to draw some pictures to tell myself how it goes. But anything that's actually an argument goes on in LaTeX.