Logic, Explainability and the Future of Understanding

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!

> It’s a similar problem in natural science. You see some elaborate set of things happening in some biological system. Can one “reverse engineer” these to find an “explanation” for them? Sometimes one might be able to say, for example, that evolution by natural selection would be likely to lead to something. Or that it’s just common in the computational universe and so is likely to occur. But there’s no guarantee that the natural world is set up in any way that necessarily allows human explanation.

It's a walk-through of George Spencer-Brown's Laws of Form.

It turns out all logic can be modeled by simple containment, and there's a complete basis (discovered by Bricken):

    A() = ()
    ((A))B = AB
    A(AB) = A(B)

Another interesting thing about it is that it's significantly more efficient to derive proofs in LoF notation than conventional notation. (Often a proof that takes several pages in conventional notation will be less than a dozen lines in LoF.)

You can write a simple SAT solver that doesn't require the input expressions to be put into a Normal Form first.

- - - -

As Wolfram and others have pointed out: It's relatively easy to program computers to search for new proofs and such[1], the trick is making it "surface" the human-interesting ones.

[1] E.g. DeepAlgebra https://arxiv.org/abs/1610.01044 https://github.com/przchojecki/deepalgebra

> We outline a program in the area of formalization of mathematics to automate theorem proving in algebra and algebraic geometry. We propose a construction of a dictionary between automated theorem provers and (La)TeX exploiting syntactic parsers. We describe its application to a repository of human-written facts and definitions in algebraic geometry (The Stacks Project). We use deep learning techniques.

I do see some value in it, but the idea of "simpleness" being captured by "least number of formulas" seems shortsighted.

In this article, what does "simple" mean? At first I assume it is "simple to understand" but clearly thats not the case.

The Leibniz rule in particular carries a lot of weight.