4 ms·

I would hard disagree that undergrad level Analysis or even just the trickier corners of vector calculus are within the bounds of what programmers can easily pi

I would hard disagree that undergrad level Analysis or even just the trickier corners of vector calculus are within the bounds of what programmers can easily pick up without dedicated and guided study. Everybody's gangster until they have to parameterize some bullshit helical structure in R3. Comparable levels of programming, what we expect of CS juniors, are regularly picked up by "the guy who is good with Excel" in office settings as it's mostly a function of experience and exposure, not theory. And now my worthless anecdotal evidence: I self taught myself into professional programming and it was a simple matter of banging my head against a wall until shit started working. The feedback loop, "did the thing crash or not", permitted me to learn on my own. I wouldn't even begin to understand how to self-teach myself Stokes Theorem or some shit, and have zero ability to author the proofs required to reach the conclusions higher level mathematics are built on.

zozbot234 4y ago
> I wouldn't even begin to understand how to self-teach myself Stokes Theorem or some shit Input it into a proof assistant, and rely on the same sort of feedback "does the computer accept your proof, or get stuck". The hard job of formalizing stuff for this purpose has seen significant progress, e.g. by the Lean mathlib project.
- dysoco 4y ago
  Do you have more information on this approach? Sounds very interesting. I've read and toyed a little with things like Lean and I'm interested in that field but the barrier seems a bit high (without pre-existing knowledge) to just "input" a theorem and toy with it.
- nickelpro 4y ago
  I would quibble with whether this is exactly equivalent. In programming I knew I needed to sort a list or find a most efficient path because some practical problem I was trying to solve demanded that I do that. Frequently I had a basically crap but working independent solution before I learned the names "EWD" or "A*". I independently discovered that I needed virtual interfaces (before I knew them by that name, "I wish pointers to parent classes could call implementations in subclasses") and then discovered language facilities for polymorphism and OOP. Without formal or at least guided instruction I would never think to move towards or discover "I wonder if there's a relationship that makes these double integrals of curls of vector fields easier to solve for". Programming has a high coupling between necessity, experience, and theory. In mathematics that coupling is much, much, much looser. Self learners in programming regularly re-discover and re-implement, typically less efficiently, all sorts of fundamentals of CS. The equivalent in mathematics rarely happens post-algebra.
  - nextos 4y ago
    I think your comparison is a bit unfair. Essentially, CS is as hard as mathematics because it is mathematics. For example, take any good static analyzer that implements abstract interpretation. It generally works using Galois connections, which is just abstract algebra. Dijkstra's algorithm or A* came pretty early in the history of CS. It would be fair to compare their difficulty to something similar in mathematics, say some basic results in Euclidean geometry.
    - nickelpro 4y ago
      CS may be mathematics but programming certainly isn't If you're discussing pure CS, the thing you can write down in a book and for which a computer is a largely theoretical device, sure CS is mathematics. If we're talking about the practical reality that CS majors in America today are trying to achieve, and their undergraduate programs are trying to prepare them for, that's becoming a working programmer and has very little relation to mathematics.
      - __MatrixMan__ 4y ago
        I wish we'd just start issuing software engineering degrees so it would be easier to get an actual computer science education.
    - eternityforest 4y ago
      A* is already intermediate level programming. CS is math because it's what we call the parts of programming that are math. But so much of programming isn't. It doesn't require deep understanding, static analysers are advanced level things that are way beyond what many working programmers ever encounter. I can't say I've ever seen "Real math" myself.
- JadeNB 4y ago
  > Input it into a proof assistant, and rely on the same sort of feedback "does the computer accept your proof, or get stuck". The hard job of formalizing stuff for this purpose has seen significant progress, e.g. by the Lean mathlib project. As a math teacher who disagrees with the premise of the GGP post ("This couldn’t be more wrong. … I’m sorry, but mathematics is orders of magnitude more intensive and difficult than most programming"), and thinks that any good programmer can learn mathematics—of course there are code wodgers out there who don't really understand their craft of programming, and so can't translate that knowledge to facilitate an understanding of mathematics—I think I also disagree with this. I've never tried it, but I can't imagine someone learning about Stokes's theorem in anything like this way. One of the many axes along which I imagine this failing are that the state of human readability in proof assistants is, well, let's say it's less well developed than the, cough, stellar state of the art in compiler error messages. But, more importantly, you can, at least in principle, know every single step in a proof of Stokes's theorem without understanding in any real sense why it's true—and a proof assistant in particular will force you into the weeds of minutiae that absolutely do not help to build any intuitive picture—and, even if you manage in the process to piece together that understanding of why it's true, you will never thereby gain an understanding of why it's interesting (e.g., among other things, its connections to physics and the entrée it offers to differential geometry).
  - zozbot234 4y ago
    The flip side of a proof assistant's 'minutiae' (and there's plenty of room to disagree wrt. whether paying attention to those minutiae helps with gaining a better, more accurate intuition!) is its ease of refactoring a proof. A proof assistant can instantly tell you whether a seemingly nicer, better-abstracted proof B really manages to prove the same thing as proof A, something that's very hard to do without the use of precise formalized statements and automated checking.
- dinkumthinkum 4y ago
  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).
  - zozbot234 4y ago
    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.
    - solveit 4y ago
      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.
    - dinkumthinkum 4y ago
      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.
hgsgm 4y ago
[dead]
geysersam 4y ago
I think you're hitting the nail on the head here. Something about the learning process makes programming much easier to pick up. What if we had something similar for mathematics? Rapid feedback, error messages, maybe even linters and highlighting for the "mathematical syntax". I've though about this before and I think tools like this could unlock math for a lot of people, and also increase the effectiveness of professional mathematicians. When learning math / seeing other learning math I've noticed that simple errors such as typos often slow down or hinder understanding of the subject.
- sillysaurusx 4y ago
  What a creative, delightful solution. I encourage you to pursue this!
- kthielen 4y ago
  I think this is the goal of proof assistants based on the Curry-Howard isomorphism, which the original author thought to denigrate for some reason.
- __MatrixMan__ 4y ago
  I'd love to play around with such tools, but I think they'd only get you so far before they'd start to become a hinderance. The linter in mathematics is whether the other mathematician (whoever you're proving to) knows what you mean. If you're locked into a rigidly defined syntax, an obvious line of questioning is: what's not expressible in this syntax? I fear that by the time the tooling was agreed on, built, and taught in schools, you'd have something like APL, which might be cool to code in, but from which the mathematical conversion would have moved on a while ago. Efforts like that, after all, are how math becomes engineering. Consider, for instance, Russel's theory of types, which was interesting math at the time and now strikes the student with an engineering background as "pretty much just Java" (or any "normal" statically typed language).
  - eternityforest 4y ago
    If you're learning math for career reasons rather than just pure curiosity, engineering is the main/possibly only place you'd use it besides statistical analysis.

zozbot234 4y ago

> I wouldn't even begin to understand how to self-teach myself Stokes Theorem or some shit Input it into a proof assistant, and rely on the same sort of feedback "does the computer accept your proof, or get stuck". The hard job of formalizing stuff for this purpose has seen significant progress, e.g. by the Lean mathlib project.

dysoco 4y ago
Do you have more information on this approach? Sounds very interesting. I've read and toyed a little with things like Lean and I'm interested in that field but the barrier seems a bit high (without pre-existing knowledge) to just "input" a theorem and toy with it.
nickelpro 4y ago
I would quibble with whether this is exactly equivalent. In programming I knew I needed to sort a list or find a most efficient path because some practical problem I was trying to solve demanded that I do that. Frequently I had a basically crap but working independent solution before I learned the names "EWD" or "A*". I independently discovered that I needed virtual interfaces (before I knew them by that name, "I wish pointers to parent classes could call implementations in subclasses") and then discovered language facilities for polymorphism and OOP. Without formal or at least guided instruction I would never think to move towards or discover "I wonder if there's a relationship that makes these double integrals of curls of vector fields easier to solve for". Programming has a high coupling between necessity, experience, and theory. In mathematics that coupling is much, much, much looser. Self learners in programming regularly re-discover and re-implement, typically less efficiently, all sorts of fundamentals of CS. The equivalent in mathematics rarely happens post-algebra.
- nextos 4y ago
  I think your comparison is a bit unfair. Essentially, CS is as hard as mathematics because it is mathematics. For example, take any good static analyzer that implements abstract interpretation. It generally works using Galois connections, which is just abstract algebra. Dijkstra's algorithm or A* came pretty early in the history of CS. It would be fair to compare their difficulty to something similar in mathematics, say some basic results in Euclidean geometry.
  - nickelpro 4y ago
    CS may be mathematics but programming certainly isn't If you're discussing pure CS, the thing you can write down in a book and for which a computer is a largely theoretical device, sure CS is mathematics. If we're talking about the practical reality that CS majors in America today are trying to achieve, and their undergraduate programs are trying to prepare them for, that's becoming a working programmer and has very little relation to mathematics.
    - __MatrixMan__ 4y ago
      I wish we'd just start issuing software engineering degrees so it would be easier to get an actual computer science education.
  - eternityforest 4y ago
    A* is already intermediate level programming. CS is math because it's what we call the parts of programming that are math. But so much of programming isn't. It doesn't require deep understanding, static analysers are advanced level things that are way beyond what many working programmers ever encounter. I can't say I've ever seen "Real math" myself.
JadeNB 4y ago
> Input it into a proof assistant, and rely on the same sort of feedback "does the computer accept your proof, or get stuck". The hard job of formalizing stuff for this purpose has seen significant progress, e.g. by the Lean mathlib project. As a math teacher who disagrees with the premise of the GGP post ("This couldn’t be more wrong. … I’m sorry, but mathematics is orders of magnitude more intensive and difficult than most programming"), and thinks that any good programmer can learn mathematics—of course there are code wodgers out there who don't really understand their craft of programming, and so can't translate that knowledge to facilitate an understanding of mathematics—I think I also disagree with this. I've never tried it, but I can't imagine someone learning about Stokes's theorem in anything like this way. One of the many axes along which I imagine this failing are that the state of human readability in proof assistants is, well, let's say it's less well developed than the, cough, stellar state of the art in compiler error messages. But, more importantly, you can, at least in principle, know every single step in a proof of Stokes's theorem without understanding in any real sense why it's true—and a proof assistant in particular will force you into the weeds of minutiae that absolutely do not help to build any intuitive picture—and, even if you manage in the process to piece together that understanding of why it's true, you will never thereby gain an understanding of why it's interesting (e.g., among other things, its connections to physics and the entrée it offers to differential geometry).
- zozbot234 4y ago
  The flip side of a proof assistant's 'minutiae' (and there's plenty of room to disagree wrt. whether paying attention to those minutiae helps with gaining a better, more accurate intuition!) is its ease of refactoring a proof. A proof assistant can instantly tell you whether a seemingly nicer, better-abstracted proof B really manages to prove the same thing as proof A, something that's very hard to do without the use of precise formalized statements and automated checking.
dinkumthinkum 4y ago
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).
- zozbot234 4y ago
  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.
  - solveit 4y ago
    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.
  - dinkumthinkum 4y ago
    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.

hgsgm 4y ago

[dead]

geysersam 4y ago

I think you're hitting the nail on the head here. Something about the learning process makes programming much easier to pick up. What if we had something similar for mathematics? Rapid feedback, error messages, maybe even linters and highlighting for the "mathematical syntax". I've though about this before and I think tools like this could unlock math for a lot of people, and also increase the effectiveness of professional mathematicians. When learning math / seeing other learning math I've noticed that simple errors such as typos often slow down or hinder understanding of the subject.

sillysaurusx 4y ago
What a creative, delightful solution. I encourage you to pursue this!
kthielen 4y ago
I think this is the goal of proof assistants based on the Curry-Howard isomorphism, which the original author thought to denigrate for some reason.
__MatrixMan__ 4y ago
I'd love to play around with such tools, but I think they'd only get you so far before they'd start to become a hinderance. The linter in mathematics is whether the other mathematician (whoever you're proving to) knows what you mean. If you're locked into a rigidly defined syntax, an obvious line of questioning is: what's not expressible in this syntax? I fear that by the time the tooling was agreed on, built, and taught in schools, you'd have something like APL, which might be cool to code in, but from which the mathematical conversion would have moved on a while ago. Efforts like that, after all, are how math becomes engineering. Consider, for instance, Russel's theory of types, which was interesting math at the time and now strikes the student with an engineering background as "pretty much just Java" (or any "normal" statically typed language).
- eternityforest 4y ago
  If you're learning math for career reasons rather than just pure curiosity, engineering is the main/possibly only place you'd use it besides statistical analysis.