you have strong point - i hadn't thought about it this way before. Just the other day someone called me out on a derivation and i spent a couple of hours writi

you have strong point - i hadn't thought about it this way before. Just the other day someone called me out on a derivation and i spent a couple of hours writing out a very tedious proof. there were lots of special cases and i really resented the bastard when i was done. the experience was very much like filling out IRS forms. it would have been very nice to have a proof assistant to back up the points where i would have much preferred to handwave. I really like the comparison to manual memory management that's exactly what this proof felt like - freeing the mallocs. but think about the following two situations: (1) you have serious doubt as to whether a statement is true. presenting a proof removes all doubt. Computer proofs, no matter how ugly, are a win for this situation (2) you have overwhelming experimental evidence that something is true and you want a mathematical proof to help you understand why it is true. Computerized proofs are less helpful here - this is where you want an elegant and simple proof. it should be very intuitive how the result depends on the assumptions. it should be something you'll be able to remember when you're 70 years old.