If you want to double down on the nerd-snipe, Immersive Linear Algebra

http://immersivemath.com/ila/index.html

I'm insufficiently nerd-sniped - what I'd really want is a book where every single mathematical expression is written in code, which I could manipulate. I'm thinking essentially of a book version of a Scrimba[0] course. I personally would love it to be in SymPy code, but I'd be happy with anything.

[0] https://v2.scrimba.com/

YES please. I'm really terrible at math, and even more terrible at trying to convert equations into code whenever I ask a math expert for help.

Something that drives me up the wall is just how sloppy math notation can be. Supposedly this pure discipline, but many authors use custom conventions all over the place, shorthand, skip steps, etc.

Give me some math code, where the end result has to compile. No sneaky tricks allowed.

You want mathlib, the lean library of established results: https://github.com/leanprover-community/mathlib4

They skip steps in writing because they can generally do them and it obscures the flow of the argument to have every thing spelled out.

There is also a book on mechanics by the authors of SICP: https://mitpress.mit.edu/9780262028967/structure-and-interpr...

Lean doesn't have expressiveness notation. It's like Perl line noise.

> They skip steps in writing because they can generally do them and it obscures the flow of the argument to have every thing spelled out.

They do that in lean too; that's the idea of simp.

Looking at the determinant section... I am so glad I got to learn linear algebra separate from matrices because oof this is hard to grok for me. Real "makes esnse if you already know the thing" stuff. But interesting to see that form of determinant definition!

https://textbooks.math.gatech.edu/ila/determinants-definitio...

Agreed - it's like they transplanted the "found in a rigorous math class" definition of a determinant. That's the one where the desired properties are the assumption and then you show that your preferred mechanical method of computation gives those properties. Usually there's a final step where you show the properties are enough to establish uniquemess.

None of those mathy steps occur in this book. There are just statements in boxes like "remember: all methods of computing the determinant give the same answer".

Honestly, looking at that section I'm having a hard time understanding how they justify the name "interactive linear algebra". The extent of my interactions is clicking on the arrow to expose the example.

The graphics are fine, but they aren't interactive like it says on the cover.

I do respect this, a lot:

> This textbook is exclusively targeted at Math 1553 at Georgia Tech. As such, it contains exactly the material that is taught in that class; no more, and no less: students in Math 1553 are responsible for understanding all visible content.

I went there for undergrad and trust me it’s the hunger games. I remember for one class, DSP we would have labs before they would actually teach the material and as a student you were how the Fck can I achieve whatever the lab is asking with the knowledge we learned so far… you couldn’t and it would take a couple of labs to realize that material req was from next class.

The mathematical pedagogical design isn't bad. But the presentation is terrible -- out of order (linking to sections ahead for explanation), and written awkwardly with minor technical errors (like multiplying by 0) that show the author doesn't fully understand what they are saying or how to express it. They are using stilted English as an attempt at formal mathematical writing.

I strongly dislike this approach to linear algebra. I much prefer matrix-less approach like in "algebra done right". I guess the latter is less suited for computation, but much, much better for understanding what's going on.