3 ms·

Proof trees just become unmanageable for anything but trivial example and not only that, their biggest benefit - knowing which rule is applied, doesn't get you

Proof trees just become unmanageable for anything but trivial example and not only that, their biggest benefit - knowing which rule is applied, doesn't get you much for a dependent type system. Not to mention that any format that isn't just strictly text is probably doomed to fail from the start. If you want essentially a text version of proof trees, just write fully annotated terms for your proofs. I think you'll quickly see that this just tends to make the proof _less_ readable because they become incredibly bloated.

carapace 6y ago
Hmm... If not proof trees, what? > Not to mention that any format that isn't just strictly text is probably doomed to fail from the start. LaTeX is text. (I'm not being snarky.) - - - - The key might be in formalizing the subjective processes like what was described starting here: > Mathematicians think in pictures > I have a picture of the real numbers in my head. It’s a straight line. This picture provides a great intuition as to how the real numbers work. I also have a picture of what the graph of a differentiable function looks like. It’s a wobbly line with no kinks in. This is by no means a perfect picture, but it will do in many cases. ...
- robinzfc 6y ago
  > If not proof trees, what? Just make the proof language similar to the standard mathematics language and possibly process it with a presentation layer that makes it even better. The examples start from Mizar [1] (since 1973), IsarMathLib [2] (disclaimer: my project), Naproche-SAD [3] (bundled with Isabelle recently) [1] http://mizar.org/ http://mizar.org/ [2] https://isarmathlib.org/ https://isarmathlib.org/ [3] http://ceur-ws.org/Vol-2634/FMM4.pdf http://ceur-ws.org/Vol-2634/FMM4.pdf
  - ImprobableTruth 6y ago
    But the key difference between Mizar style proofs and Coq/Lean style proofs is just that the former is declarative and the latter is procedural. They're both ultimately just tactics based. Sure, a declarative style is nice when reasoning about equations, but otherwise the proofs simply degenerate into awkwardly written procedural tactics proofs.
- ImprobableTruth 6y ago
  > Hmm... If not proof trees, what? I don't know. Both tactics and proof terms are already quite old (for CS concepts, that is) and there hasn't been any real competition, so I imagine in the medium-term we'll just see refinements of them. >LaTeX is text. (I'm not being snarky.) I can't imagine anyone wanting to read latex source code over tactics/proof term code. Unless you're talking about rendered latex? But that's not something people can realistically work with. Graphical proof assistants exist, but nobody uses them. For better or worse, plain text is simply king. >The key might be in formalizing the subjective processes like what was described starting here: In a sense, tactics are a very weak form of this. Instead of just describing a proof as its structured in the system, they allow a proof author to also describe some of their intent or intuition. It's definitely why some people prefer tactics based proofs. I imagine we'll see some attempts to incorporate some more of this into proof terms, but I don't know how successful this will be. But honestly, I can't even imagine would formalizing something so subjective would even look beyond this. I'm not sure if it's even possible. If it is, I imagine it's going to be a radical departure from everything we know.
  - carapace 6y ago
    > Both tactics and proof terms are already quite old (for CS concepts, that is) and there hasn't been any real competition, so I imagine in the medium-term we'll just see refinements of them. So it's really more of an issue of presentation? The techniques are fine? (I'm a professional programmer but an amateur logician, I really don't know what the big kids do.) > I can't imagine anyone wanting to read latex source code over tactics/proof term code. Unless you're talking about rendered latex? Yeah, you would generally only be looking at LaTeX source to debug your tools. > But that's not something people can realistically work with. I don't understand. I rarely work with it, but I was under the impression that it's pretty standard for writing math and science papers? Are there no WYSIWYG tools for working with rendered LaTeX? How do people work with it now, I guess is what I'm asking. > Graphical proof assistants exist, but nobody uses them. I just did a quick search and found two but they seem obscure: https://en.wikipedia.org/wiki/Jape_(software) https://en.wikipedia.org/wiki/Jape_(software) https://github.com/liamoc/holbert https://github.com/liamoc/holbert I guess the question I have is why does no one use them? Is it just inertia? I mean this is a thread about promoting the use of Lean et. al., so even the non-graphical, well-known tools are still kind of a niche, no? Are graphical proof assistants only good for students and teaching, not "heavy lifting"? In any event, I still feel that we can do better on the presentation side of things. (That's not controversial is it? The Lean folks are working on it?) I want to understand what kinds of software would help mathematicians. > In a sense, tactics are a very weak form of this. Instead of just describing a proof as its structured in the system, they allow a proof author to also describe some of their intent or intuition. It's definitely why some people prefer tactics-based proofs. That's pretty cool. :) > I can't even imagine would formalizing something so subjective would even look beyond this. I'm not sure if it's even possible. The Turing Machine is itself a formalization of a subjective process, eh? If we get to the point where the machines can "read our minds" then it will be really easy. :) Heck, mathematicians can just watch videos of each other's mental imagery! In the meantime, externalizing and formalizing these subjective intuitive processes with the machinery we've got seems like a fun and useful challenge, eh?

carapace 6y ago

Hmm... If not proof trees, what? > Not to mention that any format that isn't just strictly text is probably doomed to fail from the start. LaTeX is text. (I'm not being snarky.) - - - - The key might be in formalizing the subjective processes like what was described starting here: > Mathematicians think in pictures > I have a picture of the real numbers in my head. It’s a straight line. This picture provides a great intuition as to how the real numbers work. I also have a picture of what the graph of a differentiable function looks like. It’s a wobbly line with no kinks in. This is by no means a perfect picture, but it will do in many cases. ...

robinzfc 6y ago
> If not proof trees, what? Just make the proof language similar to the standard mathematics language and possibly process it with a presentation layer that makes it even better. The examples start from Mizar [1] (since 1973), IsarMathLib [2] (disclaimer: my project), Naproche-SAD [3] (bundled with Isabelle recently) [1] http://mizar.org/ http://mizar.org/ [2] https://isarmathlib.org/ https://isarmathlib.org/ [3] http://ceur-ws.org/Vol-2634/FMM4.pdf http://ceur-ws.org/Vol-2634/FMM4.pdf
- ImprobableTruth 6y ago
  But the key difference between Mizar style proofs and Coq/Lean style proofs is just that the former is declarative and the latter is procedural. They're both ultimately just tactics based. Sure, a declarative style is nice when reasoning about equations, but otherwise the proofs simply degenerate into awkwardly written procedural tactics proofs.
ImprobableTruth 6y ago
> Hmm... If not proof trees, what? I don't know. Both tactics and proof terms are already quite old (for CS concepts, that is) and there hasn't been any real competition, so I imagine in the medium-term we'll just see refinements of them. >LaTeX is text. (I'm not being snarky.) I can't imagine anyone wanting to read latex source code over tactics/proof term code. Unless you're talking about rendered latex? But that's not something people can realistically work with. Graphical proof assistants exist, but nobody uses them. For better or worse, plain text is simply king. >The key might be in formalizing the subjective processes like what was described starting here: In a sense, tactics are a very weak form of this. Instead of just describing a proof as its structured in the system, they allow a proof author to also describe some of their intent or intuition. It's definitely why some people prefer tactics based proofs. I imagine we'll see some attempts to incorporate some more of this into proof terms, but I don't know how successful this will be. But honestly, I can't even imagine would formalizing something so subjective would even look beyond this. I'm not sure if it's even possible. If it is, I imagine it's going to be a radical departure from everything we know.
- carapace 6y ago
  > Both tactics and proof terms are already quite old (for CS concepts, that is) and there hasn't been any real competition, so I imagine in the medium-term we'll just see refinements of them. So it's really more of an issue of presentation? The techniques are fine? (I'm a professional programmer but an amateur logician, I really don't know what the big kids do.) > I can't imagine anyone wanting to read latex source code over tactics/proof term code. Unless you're talking about rendered latex? Yeah, you would generally only be looking at LaTeX source to debug your tools. > But that's not something people can realistically work with. I don't understand. I rarely work with it, but I was under the impression that it's pretty standard for writing math and science papers? Are there no WYSIWYG tools for working with rendered LaTeX? How do people work with it now, I guess is what I'm asking. > Graphical proof assistants exist, but nobody uses them. I just did a quick search and found two but they seem obscure: https://en.wikipedia.org/wiki/Jape_(software) https://en.wikipedia.org/wiki/Jape_(software) https://github.com/liamoc/holbert https://github.com/liamoc/holbert I guess the question I have is why does no one use them? Is it just inertia? I mean this is a thread about promoting the use of Lean et. al., so even the non-graphical, well-known tools are still kind of a niche, no? Are graphical proof assistants only good for students and teaching, not "heavy lifting"? In any event, I still feel that we can do better on the presentation side of things. (That's not controversial is it? The Lean folks are working on it?) I want to understand what kinds of software would help mathematicians. > In a sense, tactics are a very weak form of this. Instead of just describing a proof as its structured in the system, they allow a proof author to also describe some of their intent or intuition. It's definitely why some people prefer tactics-based proofs. That's pretty cool. :) > I can't even imagine would formalizing something so subjective would even look beyond this. I'm not sure if it's even possible. The Turing Machine is itself a formalization of a subjective process, eh? If we get to the point where the machines can "read our minds" then it will be really easy. :) Heck, mathematicians can just watch videos of each other's mental imagery! In the meantime, externalizing and formalizing these subjective intuitive processes with the machinery we've got seems like a fun and useful challenge, eh?