![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
why it sucks to write proofs (by hand)
Dec. 1st, 2003 03:36 amSo 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.
