4 ms·

The only major problem (IMO) is that Lean and the others (Coq, Hol, Isabelle, Agda, Idris, etc...) are all pretty hard to read. Check out "Automated Propositio

The only major problem (IMO) is that Lean and the others (Coq, Hol, Isabelle, Agda, Idris, etc...) are all pretty hard to read. Check out "Automated Propositional Sequent Proofs in Your Browser with Tau Prolog" for a promising approach: https://www.philipzucker.com/javascript-automated-proving/ https://www.philipzucker.com/javascript-automated-proving/ It's rendering LaTeX proof trees.

nynox 6y ago
Following this proof tree idea, this recent paper https://arxiv.org/abs/2102.03044 https://arxiv.org/abs/2102.03044 suggests to think of proofs of theorems as large trees, a tiny subset of which needs to be made explicit to convey the confidence the rest could be written out (if ever needed).
- carapace 6y ago
  Does that presuppose that it's computationally expensive to verify proofs? If so, isn't that kind of unrealistic?
  - nynox 6y ago
    Verifying fully formalized proofs is cheap. What is expensive is to produce such formalized proofs. More precisely, to formalize a proof written in a typical math paper is extremely time-consuming and not so informative (that's why it's almost never done in practice).
    - carapace 6y ago
      Ah, cheers. :) But doesn't that bring us full-circle to Buzzard's point? Isn't that why he's saying, "Hey gang, let's do math with machines." in the first place?
asdftemp 6y ago
that is a neat demo with a lot of useful links! In fact, it seems that the Lean developers/community are very interested in new methods of achieving readability, and providing users with tools to build interfaces that scale up to the complexity of real workflows. For example, Lean in vscode supports interactive html "widgets": https://youtu.be/8NUBQEZYuis?t=453 https://youtu.be/8NUBQEZYuis?t=453 (at that timestamp, there's a quick introduction to their typical use at the moment). lean4 is committed to all sorts of extensibility; here's a demonstration of the new macros: https://twitter.com/derKha/status/1354082976456441861 https://twitter.com/derKha/status/1354082976456441861. There have also been several instances of users implementing old lean3 features (for example, the `calc` tactic mode, which has unique syntax for proving (in)equalities) by simply defining new type classes and short macros.
ImprobableTruth 6y ago
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.

nynox 6y ago

Following this proof tree idea, this recent paper https://arxiv.org/abs/2102.03044 https://arxiv.org/abs/2102.03044 suggests to think of proofs of theorems as large trees, a tiny subset of which needs to be made explicit to convey the confidence the rest could be written out (if ever needed).

carapace 6y ago
Does that presuppose that it's computationally expensive to verify proofs? If so, isn't that kind of unrealistic?
- nynox 6y ago
  Verifying fully formalized proofs is cheap. What is expensive is to produce such formalized proofs. More precisely, to formalize a proof written in a typical math paper is extremely time-consuming and not so informative (that's why it's almost never done in practice).
  - carapace 6y ago
    Ah, cheers. :) But doesn't that bring us full-circle to Buzzard's point? Isn't that why he's saying, "Hey gang, let's do math with machines." in the first place?

asdftemp 6y ago

that is a neat demo with a lot of useful links! In fact, it seems that the Lean developers/community are very interested in new methods of achieving readability, and providing users with tools to build interfaces that scale up to the complexity of real workflows. For example, Lean in vscode supports interactive html "widgets": https://youtu.be/8NUBQEZYuis?t=453 https://youtu.be/8NUBQEZYuis?t=453 (at that timestamp, there's a quick introduction to their typical use at the moment). lean4 is committed to all sorts of extensibility; here's a demonstration of the new macros: https://twitter.com/derKha/status/1354082976456441861 https://twitter.com/derKha/status/1354082976456441861. There have also been several instances of users implementing old lean3 features (for example, the `calc` tactic mode, which has unique syntax for proving (in)equalities) by simply defining new type classes and short macros.

ImprobableTruth 6y ago

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.