Parallels Between Math and Software Engineering
beta.oreilly.com
beta.oreilly.com
Some mathematicians did not like the law of excluded middle, which states that for any proposition A, either A is true or A is false. So they invented intuitionistic logic, which is normal logic without the excluded middle, and started rewriting mathematical proofs in this new system. Turns out there's a lot of stuff you can prove in intuitionistic logic.
Some mathematicians did not like the axiom of choice. One of the consequences of this axiom is that every subset of the real numbers has a least element according to some ordering. Think about it, what is the least element of {1/n : n >= 1} ? Who knows! So what did they do? Some people found it so weird they either replaced it with a weaker axiom or a contradictory one.
There's even syntax arguments in mathematics! What's the derivative of a function f? is it f'(x) or df/dx ? Is multiplication represented by a dot (.) or a cross (x) or by a juxtaposition of expressions?
Sometimes we use big existing proofs in the middle of a proof to save time. And sometimes we use the big proof to prove something far simpler than the big proof. This creates a big dependency and some people dislike hate these dependencies because the reader of the new proof will have trouble understanding the proof completely. It's like dropping in some magic in the middle of the proof and saying: "if you want to understand this proof completely, go read this other 50 page article" Sound familiar? Some mathematicians hate this so much they insist on proving things from the ground up whenever possible so that the proof is as comprehensible as possible. This is the mathematical equivalent of dependency management.
An even weirder consequence of AC is the Banach-Tarski paradox [1].
Other examples of how mathematicians come up with alternative perspectives are non-Euclidean geometries that replace the parallel postulate of the common Euclidean geometry, e.g. Lobachevskian [2] and Riemannian geometry [3].
[1] https://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox
It's easy to find such an ordering for any countable subset -- i.e., one that set-theoretically is no bigger than the integers. For instance, we can do it for all the rational numbers by saying that we order numbers p/q (p,q integers, no common factor, q positive) by converting p/q to 2^signbit(p) 3^|p| 5^|q| or something of the kind, where signbit(x)=0 is what in C you write as (x<0), and comparing the positive integers that result.
It's much harder to see how to do it for all the real numbers. In fact, you provably can't see how, in the sense that there actually is known to be no construction that does it -- no way to say explicitly which numbers to put before which.
(This is a common pattern; cases where you need AC to do something are always ones where there is no explicit construction that does it. That kinda has to be true, because there are models of set theory in which AC is false.)
For the rational numbers, this is not difficult, since we can enumerate the rational numbers. As the ordering we could then pick "a <= b" if the index of "a" in the enumeration is less than the index of "b". The least element of any set of rational numbers is then the rational number with the least index in that set.
However, the real numbers are uncountable. Tricks like this cannot work.
----
The real culprit is the axiom of excluded middle, which confounds the notions of existence and embodiment. Under classical logic it may be proven that P = NP, even though no algorithm actually exists. This already happened for certain graph problems... (=> Graph minor theorem, moving from minor-closed graph property to finite set of excluded minors is essentially non-constructive.)
Without excluded middle, the axiom of choice is exactly as trivial as it sounds: Given a non-empty set, give me an element in that set. In order to show that a set is non-empty you need to give enough information to construct an element in that set. So the proof contains the information to validate the "axiom".
With excluded middle, the proof that a set is non-empty doesn't contain enough information to pick an element from that set. So adding both excluded middle and choice takes you into an axiomatic system whose connection with the real world is rather tenuous.
----
The article is spot on: Not only is mathematics a designed system, but the analogy between programming languages and logic is perfect in view of the Curry-Howard correspondence. Elevating Zermelo-Fraenkel set theory is like insisting that your software project has to be built using Turing machines. After all, everything else is just encoding. There is a huge design space in logics as well as in programming languages. For instance, you can do physics in the setting of synthetic differential geometry and work without preconditions and use theorems which are literally impossible in ZFC.
A soundness proof for a new logic is, by the way, the logical equivalent of building a compiler. :)
The reason is intuitively clear: in order to prove that the infinite product is non-empty, we need to produce an infinitely long vector. Well, since the individual sets are non-empty, we can just for each set choose an element and put it in the vector. But this takes infinitely many steps! and that's not allowed in mathematics. The axiom of choice is a way of collapsing infinitely many steps into 1 invocation of the axiom (so 1 step, so finitely many steps). Not too much to do with excluded middle.
But you are right, the devil is in the details, so let me spell it out precisely:
The axiom states that for every set X, there is a function
\epsilon : P(X)/{\empty} -> X
To go from the higher-order version to the cartesian product, note that the cartesian product of an I-indexed family of sets is a set of functions f from I to the union of all X_i's, such that f(i) \in X_i for all i. Let (X_i)_{i\in I} be an I-indexed family of sets, all of which are non-empty, then (i -> \epsilon(X_i)) is in the cartesian product of the X_i's, where we use \epsilon for the union of all X_i's. The reason we couldn't build that element without AC is precisely that we have no way of selecting exacly one element from each X_i, even though we know that they are non-empty.
In the other direction we can use Zermelo's well-ordering theorem to construct a well-order on X. We define \epsilon to pick out the minimum with respect to this order.
(1) This really is what the axiom of choice was meant to express. If you can read German, you can refer to Zermelo's own work:
https://eudml.org/doc/158167
(2) Another example of the drawbacks of working with a first-order axiomatization is the axiom of regularity. The idea we want to express is that there are no infinitely descending element chains ("every set is well-founded"), but expressing this in first-order logic leads to a convoluted statement which obscures the simple idea... and is also not a correct encoding of this idea in intuitionistic logic!
Those aren't arguments. All of those are very standard things to do.
There's a Spiked Math comic with some good mathematics-engineering trash talk, though, with the mathematicians shooing away a hapless engineer with comments like "do you even know how to spell 'imaginary'?" and "why don't you go jmagine you have friends?" Again, I wouldn't describe this as an area of active debate.
(MIT Sussman, SICM book) http://mitpress.mit.edu/sites/default/files/titles/content/s...
Weirdly enough, I always struggled with advanced syntax, but I recently understood that it was a lack of focus on the abstraction. Kinda like programming languages :) But that's something you can't really understand when too young.
I'm a big fan of linear algebra because it's the best example of why learning math is useful. Sure knowing about equation and calculus come in handy, but linear algebra is pure modelling superpowers and a much more valuable tool overall.
Related: An awesome LA introductory lecture by Prof. Strang: http://ocw.mit.edu/courses/mathematics/18-06-linear-algebra-...
Related 2: A short tutorial on LA that I wrote: http://minireference.com/static/tutorials/linear_algebra_in_...
Mathematics is a vast topic that every quantitative discipline must necessarily draw from. Each field of study will benefit more from certain topics of it.
I agree that calculus and diff. equations techniques are important, but if you look closely, you'll see they are only "necessary" for engineers and physicists, and other "hard" sciences, and not so essential for non-science studies.
Imagine "pitching" the benefits of learning university-level math to a class of Arts students. Can you honestly say their lives will be improved if they were to learn about a bunch of techniques of integration?
On the other hand, I wouldn't hesitate to recommend learning LA to them. Thinking about operators, vector spaces, dimensions, etc. is applicable much more widely. (I speak from experience here, because I've been "finishing up" the applications chapter in my LA book and I keep finding new applications to cover: balancing chemical equations, electric currents and other network flows, nutrition, least squares approximations, linear programming, cryptography, network coding, error correcting codes, Fourier analysis, prob. theory, and quantum mechanics. The LA party just don't stop ;)
I thought it was hilarious. Almost made me want to be a math major (I was just a physics major). Which makes me think of: https://www.xkcd.com/435/
i.e. not Arts, History or Literature :)
I think it is important to remember this, because mathematics, like a computer, "fights back." You cannot simply dream up whatever structure you want and have it mean what you want and behave how you want. See Godel's incompleteness theorems. No matter what you are doing, your mathematical constructs (including your implicit Turing Machines in your computer programs) must obey certain underlying constraints that are completely mind-independent. These constraints are what mathematicians study, albeit through a glass, darkly.
Regardless of ontological issues with the post, I like that it emphasizes the designed nature of our mathematical tools. The space of possible tools is so large that there is near-limitless room for human creativity and design in mathematical research. It is a shame that most mathematics classes don't really get that across.
edit: fixed misgendering, sorry, that was sexist.
There are knowledgeable people who do not believe that mathematics is independent of our minds. It's not too far fetched of an idea. While I do not personally agree with this, I won't downplay such beliefs.
What makes you say this? Isn't this an open philosophical question? What makes you say that mathematical objects exist independent of our minds? I can dream up a set of axioms of my own and do maths from there, so I don't think mathematics necessarily exists in some Platonic ideal dimension independent of our minds.
It's actually a she =)
Anyway, I do agree with you (and the author) that mathematics has the potential of being a superb pedagogical vehicle in teaching design thinking.
While its almost certainly true that the content of mathematics is mind independent, it is far from obvious that these objects are "real things".The real meat of the issue is how exactly the mind-independence is cashed out. Different ideas paint a vastly different picture of mathematics and even the universe. For example platonism vs. nominalism. Lets not be so quick to put forward as an obvious truth the critical issue in question.
The real numbers seem to be a perfect example: if you work in physics at scales where quantization doesn't noticeably apply, the only way to calculate correct predictions is really to use real numbers and continuous (mostly Euclidean) spaces. But that doesn't mean physical objects are ontological shadows of our mathematical abstractions, as Plato's Allegory of the Cave portrayed it. Quite the reverse: when you get down to a sufficiently small, fundamental level, objects, space, and time stop being continuous and correct experimental predictions only come from using discrete formalisms.
You can then proceed to ask, which one is Platonically real, the continuous mathematical spaces or the discrete physical ones? But I think the answer there might be, "Who says anything is Platonically real? The map is not the territory, so shut up and calculate."
Maybe, but its not obvious. The fact that the same generalizations are multiply realizable in different processes/structures certainly says something interesting. The consequences of this multiple realizability hasn't been fully investigated.
Your response seems to be arguing against my post which was mainly about mind-independence, by arguing against platonism. I don't see that mind-independence necessarily implies platonism. In fact, I find all forms of platonism extremely distasteful.
>The map is not the territory, so shut up and calculate.
Right, but this in fact goes to the heart of the question of the philosophy of mathematics. When someone says that mathematical objects are mind-independent, they are not talking about the notation itself (the map), but rather the content of the notations (the territory), i.e. the structure revealed through the notation. It should be pretty obvious that there are many interesting questions about the mind-independent structure of the territory. "Shut up and calculate" isn't an answer to this question, but rather the attitude that the answer simply doesn't matter. For many fields the answer doesn't matter, but the question is worth asking nonetheless.
True, it is our observation and our model which are similar, so I suppose the philosophical question then is up to what point we can trust our observations. And if we trust our observations, I would conclude that the similarity of our observations and math means that the real world can at least exhibit 'maths', which means our minds are not the only place where math can exist.
The smartphone I'm typing this on leads me to conclude that lots of our observations are highly trustworthy :)
Our math sense could even conflict with our other useful facilities (as is the case with how easily fooled humans are when it comes to statistics).
That is not at all what the Incompleteness Theorems actually say. They say literally nothing whatsoever about what sorts of structures you can implement inside a given foundational theory, except that there will always be more, because given any foundational theory, you can construct two more foundational theories as extensions (one in which the Goedel statement is unprovable, and one in which the theory believes it's inconsistent).
From an OO point of view, the real numbers inherit almost every useful trait: they're a field, they have a topology, they have a measure. Studying the parent classes, so to speak, gives you abstract algebra, topology, and analysis, respectively.
Once you get the basics of each, you can study how they interact. Then, once that stuff is clear, they can be recombined in beautiful ways to give you new objects to study.
I came here to say the same thing. I went through a lesser known engineering discipline, "Mathematics and Enigneering" [0] and found that the type of thinking one learns doing pure math proofs has served me well in my eventual career in aerospace systems engineering. I find that the thought process in considering a proof as a high level whole/black box or being able to drill down to the finest detail while still keeping the big picture in mind has translated quite well to my day to day traversal up and down the abstraction ladder at work.
But when I look at the implementation in code it's so obvious what's going on.
I can't fathom how someone who cannot understand the math formula can understand the code.
Here's the Hokusai paper: http://www.auai.org/uai2012/papers/231.pdf
And here's an implementation: https://github.com/dgryski/hokusai
For me to understand the paper, I had to go through the code to piece out the Math jargon, even though the Math behind it is really quite simple. Another way of saying this is, "I'm dumb," sure. Not gonna argue with anyone there.
Though I still think it's curious why it's easier for me to understand a concept through code than it is through Math. It's sort of reminiscent of when you first learned Algebra, your teacher would tell you to replace the variable with an easy number and work through it to understand the mechanics of equations.
I think code is an example of that - literally working through the mechanics of algorithms to understand what they actually do and how they work.
Interesting. I'll have to check it out. Thanks!
1. An ancestor of Djinn is automated theorem proving. Why can't machines prove math theorems for us? This quest goes back to the dawn of computing science.
2. A more recent development is the Curry-Howard Correspondence. Programming in a (typed) FP language is like playing tetris. Solving symbolic logic problems [1] is also like playing tetris. Djinn exposes the connection in a REPL you can play with. And see how the computer plays tetris for you!
3. Don't want to install Djinn? No problem, just hop over to the Haskell IRC [2]. Lambdabot has a working Djinn plugin.
[0] https://hackage.haskell.org/package/djinn
From the first page:
"Geometric algebra and its extension to geometric calculus unify, simplify, and generalize vast areas of mathematics that involve geometric ideas, including linear algebra, multivariable calculus, real analysis, complex analysis, and euclidean, noneuclidean, and projective geometry. They provide a unified mathematical language for physics (classical and quantum mechanics, electrodynamics, relativity), the geometrical aspects of computer science (e.g., graphics, robotics, computer vision), and engineering."
For example, in mathematics we often have the notion of a product of two structures. The simplest is the product of two sets A and B, which in computer programming terms would just be a structure containing a field of type A and a field of type B. There are more subtle and sophisticated examples in other fields like topology, but it turns out that the categorical definition[1] matches the definition of product mathematicians were already using in each of these fields, even though it came about much later!
[1]: https://en.wikipedia.org/wiki/Product_(category_theory)
Actually mathematicians virtually never do this. Almost all of mathematics (from arithmetic to calculus to category theory) operates in the confines of ZFC[1] and adds no further axioms. All of these fields may add definitions, but these are just shorthand; the are conservative and have no actual consequences. It is more like fixing Newton's laws and then experimenting with all the machines you can build with them.
[1]: https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...
I wouldn't really say they're "totally distinct". For example, one could say that general group theory is studying the theory (in the logic sense) of a group (usually the second order theory rather than first order, but you get idea). Then adding assumptions about the structure of the group under consideration is like adding axioms and looking at the new theory.
But even then, it's not really an appropriate distinction -- accidentally assuming inconsistency and moving forward with it is exactly as far-reaching as assuming inconsistency at the foundations. And, doing some obscure work on an inconsistent foundations that no body uses is exactly as harmless as doing some obscure work on a structure without elements.
They may not do so explicitly, but it is easy to see where the axioms become important when dealing with mathematical structures. For example, if you are considering the group of integers with addition, the existence of this group is predicated on the existence of the integers, which is predicated on the existence of the natural numbers as a set, which is an axiom of ZFC (axiom of infinity[1]). The case for other foundations is similar.
> But even then, it's not really an appropriate distinction -- accidentally assuming inconsistency and moving forward with it is exactly as far-reaching as assuming inconsistency at the foundations.
No, because when studying a mathematical structure we always consider concrete instances of it, which are usually in fact the motivation for the definition of the structure. So mathematics based on possibly (relatively) inconsistent structures (other than foundational systems) is not really a thing; group theory was not initiated prior to the discovery of structures satisfying the groups axioms, and neither was the study of rings, fields, modules, topological spaces etc. On the other hand, we cannot consider models of ZFC unless we build it within the assumptions of a foundational system (possibly ZFC itself). So at some point we have to pick a set of axioms to be the bottom of our ladder of turtles, and the axioms of that system are very special indeed.
Another difference is that the axioms of a group (or a field, or a topological space) cannot stand on their own; they clearly reference sets and functions. ZFC's axioms only reference sets, all of the fundamental properties of which are enumerated in the axioms themselves. If you gave an (english speaking) alien the definition of a group, he would need to ask you what the definition of sets and functions were. So even if we wanted the group axioms to be our foundations, this would not be possible.
1. Assume false.
2. Anything follows.
For what odd-ball definition of "far reaching" is "anything" not "far reaching"? An assumption doesn't have to be an Axiom to have "far reaching" consequences. Period.
So, you're wrong -- assuming non-foundational axioms can have far reaching consequences. Assumptions are assumptions, and flaws are flaws. Assuming "false" is just as bad as working with an inconsistent foundations. It's just a fact.
That said, the actual difference you're trying to elucidate is sociological, not technical -- you suppose that people are less likely to accept non-foundational assumptions, and so that'll check back something from a sociological viewpoint. You assume people won't build results on top of a system with an unproven assumption thrown in.
That argument would be a lot more compelling if Mathematicians formalized their arguments in terms of an underlying foundations, because then we would always know that all assumptions are checked. But Mathematicians don't work like that. And errors creep in. And if people build on top of those errors, it can be pretty catastrophic.
In short, what matters is that people accept the incorrect fact and move forward from it, NOT whether that incorrectness comes from foundations or from something built on top of them. The impact of either depends entirely upon how many people trust the result and build on top of it.
> That argument would be a lot more compelling if Mathematicians formalized their arguments in terms of an underlying foundations, because then we would always know that all assumptions are checked.
But they do! You can find many books on real analysis that prove that the reals exist from the foundation, as well as proving that the naturals and integers exist on the way. They don't constantly refer to the foundations, but they use facts that have been rigorously proved from the foundations. And although they don't write "axiom schema of specification" every time they consider a subset satisfying a property, that doesn't mean they don't know that it is required.
> In short, what matters is that people accept the incorrect fact and move forward from it, NOT whether that incorrectness comes from foundations or from something built on top of them. The impact of either depends entirely upon how many people trust the result and build on top of it.
My whole point is that you don't have to trust the group axioms, because they can (and typically are) validated relative to ZFC. Since the trivial group can be constructed within ZFC they are consistent in ZFC, full stop. The same goes for refinements like commutative groups. If the group axioms lead to a inconsistency, it can only be because ZFC itself is inconsistent. Do you not think that being a possible source of inconsistency or not is an important distinction?
[1]: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
Except for all the non-ZFC foundations, like type theory or category-theoretic foundations.
- everybody can vote? Well, we have https://en.wikipedia.org/wiki/Felony_disenfranchisement and, on the other end of the spectrum, in the UK "Although the law relating to elections does not specifically prohibit the Sovereign from voting in a general election or local election, it is considered unconstitutional for the Sovereign and his or her heir to do so” (http://www.royal.gov.uk/MonarchUK/QueenandGovernment/Queenan...)
- everybody with a sufficiently high income must pay social security taxes? Not if you’re member of certain religious groups (https://faq.ssa.gov/link/portal/34011/34019/Article/3821/Are...)
Even the universal declaration of human rights (http://www.un.org/en/documents/udhr/) often has small exceptions. For example:
- "Everyone has the right to take part in the government of his country, directly or through freely chosen representatives"? Not quite in the USA, as one must be born in the USA to become president.
- "higher education shall be equally accessible to all on the basis of merit": questionable in many countries, given the costs.
It seems there’s no rule so universal that it doesn’t have some exception. That, IMO, makes law so different from math that any analogy is useless.
If it were just that the axioms of law are more complicated in the sense of being more conditional, then law would be extremely math-like. After all, theorems with lots of conditional properties (e.g., very common in certain types of algebra, a lot of dynamics, any programming language theory, etc.) are still mathematical theorems.
Law is distinguished from Math in two ways:
1) Law has more politics and isn't immune from politics. Mathematical truth, at least, is.
2) In law, the atomic propositions are always difficult to quantify and require human judgement; there is rarely an algorithm for weighing the evidence and determining guilt (or constitutionality, etc).
Actually, these laws are the most dystopian.
One concept that seems to have this design goal is strict liability: what you intended, what you believed, what elaborate conspiracies were created to deceive you, none of that matters. If you did it, you are guilty and will be punished, full stop. This is attractive because it's much harder to prove beyond a reasonable doubt that someone did something "with malice" or "intentionally" than to prove that they did it. This tends to show up around youth sexuality, probably because that's an area where social norms have changed quite a bit.
It doesn't matter if the 17.5-year-old you slept with presented a fake ID saying she was 18, took the lead in all sexual activity, etc. It doesn't matter if she shows up in court and begs the judge to let you go. People whose 18th birthday has not elapsed cannot give consent, full stop. Sex without consent is rape, rapists are bad people and should be made to suffer, so you're going to prison and then on to the sex offender registry. Your judge, and the judges you appeal to, all think this is ridiculous, but their hands are tied because the law was written like a computer program that failed to consider edge cases. (Literally edge cases - those that fall near numerical boundaries. Some states have patched their legal systems to allow consent between partners who are close in age but under the normal age of consent. Some have, but only for heterosexual couples. Some still haven't. My state actually tried and convicted two teenagers as adults for raping each other at the same time.)
Same with child porn. Child porn laws were created a time when taking and distributing a picture could only be part of a commercial publishing operation. Anyone who creates or possesses an image of a nude child is guilty of a child pornography offense. Seems reasonable. Now every teenager has an internet-connected camera in their process, and we found an edge case we forgot: the child pornographer is the child him/herself and the consumer is her long-term boyfriend, also underage. Still just as illegal and the same punishment is required. You would hope prosecutors would turn a blind eye, but "the law is the law."
These rather salacious examples are the most high-profile, but I'm sure the same problems happens in more mundane areas of law as well.
At some point you have to trust judges and you have to empower bureaucrats to help people get out of obviously ridiculous situations. Laws are much more difficult to change than computer programs; there needs to be a reasonable amount of discretion for a manual override until the law can be fixed.
In theoretical CS, people talk of catching and fixing "bugs" in proofs, namely, mistakes that make the proof fail but can hopefully be fixed while sticking to essentially the same idea.
One can "refactor" proofs, in superficial ways (e.g., renaming of concepts), but in deeper ways also, e.g., extract part of a proof to make it an independent lemma that you can reuse (or "invoke") from other parts of the proof. One often tries to "decouple" large proofs into independent parts with clearly defined "interfaces", that the reader can understand separately from each other, though this usually implies a tradeoff (a more tightly integrated proof requires more mental space but is usually shorter overall).
One can think of the statement of sub-results (lemmas) as providing an "interface" to invoke them elsewhere, which you try to "decouple" from the actual "implementation", namely, the way the lemmas are really proven. It takes practice to find the right way to abstract away the essence of a result to state it correctly, without burdening it with implementation details, but without forgetting an important aspect of the result that will be necessary later. As in software engineering, once a result is proven, you stop burdening your mind with the implementation and mostly think about the statement (i.e., what the result is supposed to be doing) when using it.
In software engineering, one must decide which part of the code is "responsible" for checking certain properties on the objects, and that code may "assume" some preconditions on its inputs and must "guarantee" some preconditions on its outputs. In the same way, in proofs, one often wonders where certain conditions should be verified. Should they be part of the definition of the object? Does this lemma enforce more conditions on the object than what is guaranteed by its statement?
The parallel is not perfect. In software engineering, you can rely on the computer to check that your code is correct, and to execute it. In mathematics you rely on other humans to do this and check that they are convinced by your proofs. This means you can get away with appeals to human intuition which are not fully formal, but on the other hand there is no safety net when you make an error in your reasoning, no reality check that you can invoke to avoid exploring erroneous consequences. Also, this does not apply to all types of proofs; but it applies especially well to proofs that describe a construction, i.e., a way to "build" a certain abstract object, often to justify that an object with a certain desirable set of properties exists.
(Disclaimer: I'm hardly an expert in these languages; I just dabble.)
For example, creating new domain specific control flows with Lisp macros versus defining a Dirac delta function using limits and integrals. In programming it's easy for bugs to seep in because there are more little/subtle details and leaky abstractions. But math on the other hand feels much more abstract and clean.
Perhaps this is just because dumb silicon boxes interpret our code and humans interpret our math which gives us a much more sophisticated base language to work with.
And describing pre / post invariants of imperative statements, turns them into typed functions isn't it ? I'm having a hard time seeing the difference.
the operational semantics of functional languages are much more well-defined.
Logic programming is itself firmly based in axiomatic semantics
[Hoare-logics for imperative languages] is comparatively understudied, though.
I have a keen interest in neural networks and it requires good foundation of Math.
I've never taken a college-level linear algebra course, and I've found KhanAcademy's linear algebra course to be a good gentle introduction. I just skip the parts I already know.