Hacker News Reader

Comment by dinkumthinkum | Hacker News Reader

Self teach Stokes Theorem by inputting it into a proof assistant? Are you serious? That is very inefficient; the OP was talking about learning the kind of vector calculus taught in first calculus sequence. I think just watching a short YouTube video and doing a few exercises will work and is a proven method. Proofs of theirebs are very often much more complicated than applying them (understatement intended).

View on HN

If you don't understand the proof of any theorem, you haven't really "learned" it in any real sense. Wrt. doing computational exercises in vector calculus, that requires knowing the "rules of the game" which is also something that you can test precisely in a proof assistant.

First, of course you can understand a theorem without knowing the proof! Uniqueness of prime factorization, for instance, is notoriously tricky to prove, but it would be a stretch to say people who haven't majored in maths haven't learned it in any real sense.

Second, even if you wanted to understand the proof of a theorem, doing it with a proof assistant is an atrocious way to go about it.

Many proofs of theorems in calculus would require topology to understand. You’re suggesting that you cannot be competent in vector calculus without knowing the proofs at a professional. I think I, along with probably everyone, will have to disagree with that.

Reply on news.ycombinator.com