> even though the underlying rules (or underlying “language”) used in different areas of mathematics are different, there ends up being some way to translate be

> even though the underlying rules (or underlying “language”) used in different areas of mathematics are different, there ends up being some way to translate between them—so that at the next level of abstraction the path that was taken no longer critically matters. This and the previous arguments made me feel much better about the value of using proof assistants to advance mathematics! For example, there’s been quite a bit of controversies surrounding the usage of e.g. Coq to prove the 4-color theorem; folks complain that although the proof can be verified, brute-forcing it doesn’t provide us with further mathematical insight. But that might be fine, since we’d use the proof to build up other abstractions, and if we felt the need, we can always come back and re-prove 4-color using a more humanly explanable method. The other nice insight is that maybe we get to define “simplicity” with a bit more rigor than how we usually define it (I’m aware of Clojure’s definition of it): a few number of somewhat orthogonal axioms, that enable the biggest reduction of quantity of steps needed when proving things with said axioms. For software engineering, this means having relatively few primitives, that are composable enough to greatly simplify a program either statically or dynamically. No need to try too hard to reduce the axioms/helpers into a single one, as the ratio of utility might tip to the wrong side. It’s also cool to notice that such common definition of simplicity might change depending on what new concepts we assimilate. Also interesting that you can somewhat quantify it by using a probability distribution over the common use-cases of your axioms!