2 ms·
Do you have any particularly memorable example of a complicated proof which was lacking complicated "trivial" details? My experience (I work in interactive theo
by fmap 10y ago
Do you have any particularly memorable example of a complicated proof which was lacking complicated "trivial" details? My experience (I work in interactive theorem proving) is that many such proofs are subtly wrong.
- kxyvr 10y agoOff the top of my head, I'd probably say integration by parts in multiple dimensions. Generally, I see people given an outline of a proof in two dimensions for Green's theorem. I'd say it's an outline because the typical qualification is that the proof is for simple regions and that all we have to do is patch these regions together for more complicated areas. However, the details of how that works, in my opinion, are complex. The only full proof that I've ever seen for this result comes from Daniel Stroock's book, "A concise introduction to the theory of integration." He takes a little over 100 pages of background work to get there. This actually leads to my math confession, "I have a PhD in math and can't prove integration by parts in multiple dimensions." By the way, if anyone has another reference or good proof for proving integration by parts in multiple dimensions, please let me know. I'd love to see it. As another aside, I'd love to start using interactive theorem proving tools in my field, which tends to be related to things like optimization and differential equations. That said, I've never seen examples for how to prove results for stuff in calculus using interact theory proving tools, so do you know of any? Really, things like the mean value theorem or Taylor series would be great to see.