>So it's really more of an issue of presentation? The techniques are fine?
Well, both techniques are ultimately just a way of representing natural deduction (for a different proof calculus that isn't closely related to natural deduction you'll definitely need different techniques). Proof terms are the representation you get from the Curry-Howard Isomorphism (essentially the derivation is left implicit since it is unambiguous), while tactics based proofs are approximations of traditional proofs written in prose.
Are they 'fine'? Well, maybe there's some amazing graph-based way that will make current approaches look completely inadequate, but at the moment they work and we just don't know any better way.
>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.
It's definitely the standard, but I personally don't find working with diagrams in it pleasant (though I know some disagree). WSYIWYG tools exist, but don't find much usage. Everyone I know simply has a preview window open right next to their latex code, so it's not really an 'interactive' process. If you're fine with that, I'd just recommend generating latex code from proof objects/tactics scripts (which there already is some work on as far as I know). You should be able to generate e.g. proof trees very easily, they'll just be massive.
>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?
I imagine it's a combination of all sorts of factors. Proof assistants are very niche, the community is very academic and proof assistants require a lot of infrastructure which is why most users are concentrated among a handful of proof assistants. Proof assistants using dependent types (such as Lean) are also programming languages which I think naturally biases them towards text.
>Are graphical proof assistants only good for students and teaching, not "heavy lifting"?
I don't see any reason why that should fundamentally need to be - but I think the same applies to visual programming languages, which are essentially stuck in the same position for whatever reason.
>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.
I don't think this is controversial at all - _how_ to improve presentation on the other hand might be.
>In the meantime, externalizing and formalizing these subjective intuitive processes with the machinery we've got seems like a fun and useful challenge, eh?
Sure, but anything beyond very incremental improvements also strike me as very hard, so it's not an area where I would expect much change for now, especially because there's still a good amount of low-hanging fruit in the area of proof assistants.
Well, both techniques are ultimately just a way of representing natural deduction (for a different proof calculus that isn't closely related to natural deduction you'll definitely need different techniques). Proof terms are the representation you get from the Curry-Howard Isomorphism (essentially the derivation is left implicit since it is unambiguous), while tactics based proofs are approximations of traditional proofs written in prose.
Are they 'fine'? Well, maybe there's some amazing graph-based way that will make current approaches look completely inadequate, but at the moment they work and we just don't know any better way.
>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.
It's definitely the standard, but I personally don't find working with diagrams in it pleasant (though I know some disagree). WSYIWYG tools exist, but don't find much usage. Everyone I know simply has a preview window open right next to their latex code, so it's not really an 'interactive' process. If you're fine with that, I'd just recommend generating latex code from proof objects/tactics scripts (which there already is some work on as far as I know). You should be able to generate e.g. proof trees very easily, they'll just be massive.
>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?
I imagine it's a combination of all sorts of factors. Proof assistants are very niche, the community is very academic and proof assistants require a lot of infrastructure which is why most users are concentrated among a handful of proof assistants. Proof assistants using dependent types (such as Lean) are also programming languages which I think naturally biases them towards text.
>Are graphical proof assistants only good for students and teaching, not "heavy lifting"?
I don't see any reason why that should fundamentally need to be - but I think the same applies to visual programming languages, which are essentially stuck in the same position for whatever reason.
>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.
I don't think this is controversial at all - _how_ to improve presentation on the other hand might be.
>In the meantime, externalizing and formalizing these subjective intuitive processes with the machinery we've got seems like a fun and useful challenge, eh?
Sure, but anything beyond very incremental improvements also strike me as very hard, so it's not an area where I would expect much change for now, especially because there's still a good amount of low-hanging fruit in the area of proof assistants.