3 ms·

Anyone interested in this topic, I have a prediction that the time is right for a new math, that starts from just 1 and 0, and builds every symbol up in a rigor

by breck 7y ago

Anyone interested in this topic, I have a prediction that the time is right for a new math, that starts from just 1 and 0, and builds every symbol up in a rigorous way. We're working on the infrastructure to make such a thing easier, but the project does not currently have a leader: https://github.com/treenotation/jtree/issues/83 https://github.com/treenotation/jtree/issues/83

devicetray0 7y ago
Forgive me, but why is the TreeNotation/jtree library the right place to craft a new "rigorous" mathematics language?
- breck 7y ago
  It’s a good question. This paper hints at the reason: https://github.com/treenotation/jtree/blob/master/papers/paper3/countingComplexity.pdf https://github.com/treenotation/jtree/blob/master/papers/pap... First, jtree is a bit orthogonal as that’s just an implementation. The github issue is there for convenience, it’s arbitrary. The reason for tree notation is that it’s a level up from binary. Binary notation does not give you the ability to define new symbols. Tree notation is a 2d binary. You can define new abstractions. It is a bridge between human and machine languages. Take any concept in mathematics, such as “derivative”. How would you define such a concept, starting only from 1s and 0s? Tree notation gives you a method to do that, in a way that’s not only efficient (noiseless), but also gives you practical tools, like complexity counting.
lidHanteyk 7y ago
Disregard cranks, acquire Metamath: http://us.metamath.org/downloads/metamath.pdf http://us.metamath.org/downloads/metamath.pdf
- breck 7y ago
  Very interesting, thanks! This is definitely along the lines of what I’m thinking. It uses EBNF, i think if we switched it to tree notation it would be much, simpler, tighter, and more self contained.
- drchewbacca 7y ago
  Metamath is awesome if you're willing to slum it :) https://jiggerwit.wordpress.com/2018/04/14/the-architecture-of-proof-assistants/ https://jiggerwit.wordpress.com/2018/04/14/the-architecture-...
  - lidHanteyk 7y ago
    How long does it take your preferred proof assistant to prove things? Metamath's standard set.mm takes only about 10s to prove everything.
    - drchewbacca 7y ago
      My preferred proof assistant is definitely Metamath, I think it just needs a big company to come along and build an awesome front end for it and it will become the standard.
    - digama0 7y ago
      Actually if you use the smm verifier that's been cut down to about 800ms. :) However, most of the theorem provers of today have been built on the philosophy that performance doesn't matter, or at least is secondary to ease of use, mathematical cleanliness etc, from the functional programming community. It turns out that once you make this decision it's difficult to get that raw speed back, even if you start worrying about performance later, and the HOL family provers make it worse by defining correctness in terms of the running of an ML program, which bakes the runtime of the ML system into the proof checking time. When you combine this with the fact that these ML programs are not proofs but proof scripts, that perform a lot of "unnecessary" work like searching for a proof rather than just going straight for the answer, it suddenly begins to make sense why these systems take on the order of hours to days to check their whole libraries. Coq and Lean are somewhere in the middle, because they have proof terms, but the logic itself still requires some unbounded computations. Checking a proof here is often fast, unless you make too much use of computation in the logic. But people often don't care about proof terms, and still store the proof scripts, which are as slow as ever. Metamath is in this setting somewhat unique in eschewing proof scripts altogether, or more accurately, inlining proof scripts immediately on the author's machine. The resulting proofs are often comparatively long and verbose, but I would argue this is only a display matter, since all the other provers are doing the same thing, they just aren't showing it.

by breck 7y ago

devicetray0 7y ago

Forgive me, but why is the TreeNotation/jtree library the right place to craft a new "rigorous" mathematics language?

breck 7y ago
It’s a good question. This paper hints at the reason: https://github.com/treenotation/jtree/blob/master/papers/paper3/countingComplexity.pdf https://github.com/treenotation/jtree/blob/master/papers/pap... First, jtree is a bit orthogonal as that’s just an implementation. The github issue is there for convenience, it’s arbitrary. The reason for tree notation is that it’s a level up from binary. Binary notation does not give you the ability to define new symbols. Tree notation is a 2d binary. You can define new abstractions. It is a bridge between human and machine languages. Take any concept in mathematics, such as “derivative”. How would you define such a concept, starting only from 1s and 0s? Tree notation gives you a method to do that, in a way that’s not only efficient (noiseless), but also gives you practical tools, like complexity counting.

lidHanteyk 7y ago

Disregard cranks, acquire Metamath: http://us.metamath.org/downloads/metamath.pdf http://us.metamath.org/downloads/metamath.pdf

breck 7y ago
Very interesting, thanks! This is definitely along the lines of what I’m thinking. It uses EBNF, i think if we switched it to tree notation it would be much, simpler, tighter, and more self contained.
drchewbacca 7y ago
Metamath is awesome if you're willing to slum it :) https://jiggerwit.wordpress.com/2018/04/14/the-architecture-of-proof-assistants/ https://jiggerwit.wordpress.com/2018/04/14/the-architecture-...
- lidHanteyk 7y ago
  How long does it take your preferred proof assistant to prove things? Metamath's standard set.mm takes only about 10s to prove everything.
  - drchewbacca 7y ago
    My preferred proof assistant is definitely Metamath, I think it just needs a big company to come along and build an awesome front end for it and it will become the standard.
  - digama0 7y ago
    Actually if you use the smm verifier that's been cut down to about 800ms. :) However, most of the theorem provers of today have been built on the philosophy that performance doesn't matter, or at least is secondary to ease of use, mathematical cleanliness etc, from the functional programming community. It turns out that once you make this decision it's difficult to get that raw speed back, even if you start worrying about performance later, and the HOL family provers make it worse by defining correctness in terms of the running of an ML program, which bakes the runtime of the ML system into the proof checking time. When you combine this with the fact that these ML programs are not proofs but proof scripts, that perform a lot of "unnecessary" work like searching for a proof rather than just going straight for the answer, it suddenly begins to make sense why these systems take on the order of hours to days to check their whole libraries. Coq and Lean are somewhere in the middle, because they have proof terms, but the logic itself still requires some unbounded computations. Checking a proof here is often fast, unless you make too much use of computation in the logic. But people often don't care about proof terms, and still store the proof scripts, which are as slow as ever. Metamath is in this setting somewhat unique in eschewing proof scripts altogether, or more accurately, inlining proof scripts immediately on the author's machine. The resulting proofs are often comparatively long and verbose, but I would argue this is only a display matter, since all the other provers are doing the same thing, they just aren't showing it.