5 ms·

I work professionally as an applied mathematician and I'd love if more people were to embrace proof assistant tools. That being said, I've worked with Coq a fa

by kxyvr 10y ago

I work professionally as an applied mathematician and I'd love if more people were to embrace proof assistant tools. That being said, I've worked with Coq a fair amount in the past and I find it really hard to prove things related to my primary field, optimization. Some of it is getting more practice with the tools. However, how proofs are generated in these tools is different than how I was trained to produce proofs and I don't find it to be a simple process to just learn how. If anyone is curious about these tools, I recommend the Coq'Art book (https://www.springer.com/us/book/9783540208549 https://www.springer.com/us/book/9783540208549) As an additional, somewhat controversial comment, I think these tools are important because there's quite a bit of corruption with publishing. In short, if you're well known and liked author, you often get a pass on your papers and they're not well checked for errors. I've been yelled at by editors for questioning proofs of famous people. I'm not the only one. No. I will not name names or publications. Also, although it's not universal, when some journals say communicated by so-and-so, that means that so-and-so vouched for the paper, so they published it immediately without other peer review. Is the paper right? Maybe. However, I find the practice unsettling. Bringing the comment back to proof assistant tools, I believe they would remedy some, but not all of the problems described above. We don't have to worry if a paper got a pass because the author was well liked. When can just run the proof through the tool and check that it's correct. Anyway, if someone has some references or tutorials for people using proof assistant tools for applied math kinds of results, I'd love to read them. Things like stability regions for ODE solvers or convergence results for stuff like Newton's method. Or, honestly, anything that helps understand the tools and methodology more easily.

Joof 10y ago
I was very interested in this as well for learning purposes. Without an instructor it's fairly easy to accidently make logical jumps and come up with wrong proofs. I figured that math is effectively a somewhat formal language for communicating concepts, so a compiler that checks errors (or even suggests corrections) could work well. Tools like coq are great, but difficult to use (even as a programmer used to languages like Haskell) and they don't have a large set of existing proofs to work off of. My opinion is that we need a good intermediate representation for proof tools (to share results; each new tool now needs a huge base built up to start being useful) and simpler tools to work with. It would be an enormous benefit to mathematicians and the world at large.
- kxyvr 10y ago
  That'd be great, but I think the hard part about sharing representations is that many of the proof tools are based on different underlying type theories, which make it hard to go back and forth. For example Coq is based on the calculus of inductive constructions whereas Isabelle is based on HOL. Though, I'm guessing it's possible once a type scheme is fixed. Just poking around briefly, here's an SO question and answer on some of the differences between CIC and HOL (https://stackoverflow.com/questions/30152139/what-are-the-strengths-and-weaknesses-of-the-isabelle-proof-assistant-compared-t https://stackoverflow.com/questions/30152139/what-are-the-st...)
  - mafribe 10y ago
    This should be possible when the underlying logics are similar (e.g. Isabelle/HOL and HOLight) but can be tricky if the logics are far apart (e.g. Isabelle/HOL and Coq).
  - Joof 10y ago
    Fair. I need to spend a few weeks with coq before I really form an opinion of how these things could be improved.
jeff_marshall 10y ago
When I worked as an RA while getting my BSCS (and for a time during my first post-college job), I spent quite a bit of time with ACL2 (a language, logic, and proof assistant using a first-order variant of common lisp). I spent a lot of time applying ACL2 to my research area (information flow analysis for secure systems), and I feel your pain re: proof strategies. It was almost like learning how to prove things again (e.g. learning new induction strategies that matched the logical framework used by the tool). That said, there was an incredible amount of freedom in knowing that if the tool accepted a proof, it was (probably) correct. Occasionally I would stumble on to a strategy without knowing why exactly it worked, and the interactive nature of the tool helped me gain understanding by letting my apply transformations to terms interactively without having to worry about whether I screwed up some minor detail. I'd love to see one of these tools (though, probably not ACL2 at this point - first-order logic frequently felt limiting (e.g. when proving things about parameterized equivalence relations)) used in a book covering some math topic I'd like to learn, as interactive formalism seems well-suited to self-exploration (you don't need an instructor to point out your trivial errors)
danidiaz 10y ago
Newbie question: if one is not interested in extracting programs, but only in proving stuff, is a proof assistant like Isabelle/HOL easier to use than one based on constructive logic like Coq?
- mafribe 10y ago
  The short answer is yes. That's because (1) a classical system like HOL can use external automatic theorem provers ("sledgehammer") that are based on classical logic (most of them are), in a way that constructive systems like Coq cannot (at least currently). Moreover (2) classical proofs can be shorter and simpler, sometimes considerably so. In practise many other dimensions also play an important role, in particular available tactics, tactic definition languages, proof editors, available decision procedures for the specific axioms one is interested in, libraries and so on.
  - bjz_ 10y ago
    Are there downsides to the HOL approach when compared to constructive systems?
    - mafribe 10y ago
      Depends what you want to do. If you are interested in program verification, then not all that much, because everything is about automation. Coq/Agda have a small edge if you want to prove something about Lambda calculus since Coq/Agda are themselves Lambda calculi, and not surprisingly most Coq/Agda work is about Lambda calculus ... The HOL school has probably a small edge in other areas. In practise the underlying approach (LCF vs Curry-Howard and dependent types vs HOL) makes much less of a difference than automation and availablility of proof libraries.
    - Retra 10y ago
      It's hard to take something that's been proven true and turn it into something that's been proven useful without employing some constructive means.
Tyr42 10y ago
I really think that proof assistants like Coq are going to eventually be the future of math. Once they are less painful to use :( I spent a term working as a research assistant on Coq, proving a new induction scheme for Featherweight Java classes. I came into the term quite hopeful, and already with some Coq experience, but I really don't feel like these tools are good enough to expect regular people to use. Even mathematicians. I'm hopeful that in the distant future, we can get some AI assistance going on, so that the proof assistant can actually assist, not just check and impede. I would like my month spent on transitivity of subclassing back :( It's really hard to use these tools as they are now.
- bjz_ 10y ago
  I've heard some from people that it's almost like we are still at 'the assembly language' level when it comes to theorem proving. We still have a great deal to build in order to be productive at higher levels of abstraction.
- eli_gottlieb 10y ago
  >I would like my month spent on transitivity of subclassing back :( Oh God, that gave me flashbacks. I've done at least one transitivity of subtyping proof where I actually got the right theorem, then found later in the module that I had to rewrite the whole thing with a graph-theory library supplying some theorems about DAGs/finite posets. It's horrible, and that piece of work still isn't done!
hyperbovine 10y ago
> if you're well known and liked author, you often get a pass on your papers and they're not well checked for errors. A friend who was advised by a "famous" (i.e., in his/her field) mathematician told me basically the same thing. This person unquestionably has had brilliant insights during the course of their career, most of which turned out to be correct. But (s)he has also published several false results, including one "major" false result. Some mathematicians are known to be sloppy and the field puts up with it, which seems weird to me. Regarding Coq, never tried it, but here is my guess at what's going on. Coq seems to be mainly embraced by algebraists and people doing discrete math, less so in fields which are more analytic (optimization, probability, functional analysis, PDE, etc.) Proofs in the latter branches of math seem to more commonly invoke geometric or "intuitive" arguments which, while completely rigorous, are harder to reduce to a sequence of logical statements. Take for example "convexity implies continuity". You can basically prove this in 1d by drawing a picture, whereas the full, gory, rigorous version, though elementary, requires a little effort. Proofs in modern algebra, otoh, involve a lot of symbol pushing, which computers excel at. Just a guess.
- deleted 10y ago
  [deleted]
eli_gottlieb 10y ago
Analysis and the real numbers tend to be very hard to encode in constructive foundations. We still haven't got the right balance between checking for computability of the proof and all objects it hypothesizes, versus letting some of the types we hypothesize over be uncomputable and uncountably large, while requiring that propositional types (squash types) have continuous elements.

by kxyvr 10y ago

Joof 10y ago

I was very interested in this as well for learning purposes. Without an instructor it's fairly easy to accidently make logical jumps and come up with wrong proofs. I figured that math is effectively a somewhat formal language for communicating concepts, so a compiler that checks errors (or even suggests corrections) could work well. Tools like coq are great, but difficult to use (even as a programmer used to languages like Haskell) and they don't have a large set of existing proofs to work off of. My opinion is that we need a good intermediate representation for proof tools (to share results; each new tool now needs a huge base built up to start being useful) and simpler tools to work with. It would be an enormous benefit to mathematicians and the world at large.

kxyvr 10y ago
That'd be great, but I think the hard part about sharing representations is that many of the proof tools are based on different underlying type theories, which make it hard to go back and forth. For example Coq is based on the calculus of inductive constructions whereas Isabelle is based on HOL. Though, I'm guessing it's possible once a type scheme is fixed. Just poking around briefly, here's an SO question and answer on some of the differences between CIC and HOL (https://stackoverflow.com/questions/30152139/what-are-the-strengths-and-weaknesses-of-the-isabelle-proof-assistant-compared-t https://stackoverflow.com/questions/30152139/what-are-the-st...)
- mafribe 10y ago
  This should be possible when the underlying logics are similar (e.g. Isabelle/HOL and HOLight) but can be tricky if the logics are far apart (e.g. Isabelle/HOL and Coq).
- Joof 10y ago
  Fair. I need to spend a few weeks with coq before I really form an opinion of how these things could be improved.

jeff_marshall 10y ago

When I worked as an RA while getting my BSCS (and for a time during my first post-college job), I spent quite a bit of time with ACL2 (a language, logic, and proof assistant using a first-order variant of common lisp). I spent a lot of time applying ACL2 to my research area (information flow analysis for secure systems), and I feel your pain re: proof strategies. It was almost like learning how to prove things again (e.g. learning new induction strategies that matched the logical framework used by the tool). That said, there was an incredible amount of freedom in knowing that if the tool accepted a proof, it was (probably) correct. Occasionally I would stumble on to a strategy without knowing why exactly it worked, and the interactive nature of the tool helped me gain understanding by letting my apply transformations to terms interactively without having to worry about whether I screwed up some minor detail. I'd love to see one of these tools (though, probably not ACL2 at this point - first-order logic frequently felt limiting (e.g. when proving things about parameterized equivalence relations)) used in a book covering some math topic I'd like to learn, as interactive formalism seems well-suited to self-exploration (you don't need an instructor to point out your trivial errors)

danidiaz 10y ago

Newbie question: if one is not interested in extracting programs, but only in proving stuff, is a proof assistant like Isabelle/HOL easier to use than one based on constructive logic like Coq?

mafribe 10y ago
The short answer is yes. That's because (1) a classical system like HOL can use external automatic theorem provers ("sledgehammer") that are based on classical logic (most of them are), in a way that constructive systems like Coq cannot (at least currently). Moreover (2) classical proofs can be shorter and simpler, sometimes considerably so. In practise many other dimensions also play an important role, in particular available tactics, tactic definition languages, proof editors, available decision procedures for the specific axioms one is interested in, libraries and so on.
- bjz_ 10y ago
  Are there downsides to the HOL approach when compared to constructive systems?
  - mafribe 10y ago
    Depends what you want to do. If you are interested in program verification, then not all that much, because everything is about automation. Coq/Agda have a small edge if you want to prove something about Lambda calculus since Coq/Agda are themselves Lambda calculi, and not surprisingly most Coq/Agda work is about Lambda calculus ... The HOL school has probably a small edge in other areas. In practise the underlying approach (LCF vs Curry-Howard and dependent types vs HOL) makes much less of a difference than automation and availablility of proof libraries.
  - Retra 10y ago
    It's hard to take something that's been proven true and turn it into something that's been proven useful without employing some constructive means.

Tyr42 10y ago

I really think that proof assistants like Coq are going to eventually be the future of math. Once they are less painful to use :( I spent a term working as a research assistant on Coq, proving a new induction scheme for Featherweight Java classes. I came into the term quite hopeful, and already with some Coq experience, but I really don't feel like these tools are good enough to expect regular people to use. Even mathematicians. I'm hopeful that in the distant future, we can get some AI assistance going on, so that the proof assistant can actually assist, not just check and impede. I would like my month spent on transitivity of subclassing back :( It's really hard to use these tools as they are now.

bjz_ 10y ago
I've heard some from people that it's almost like we are still at 'the assembly language' level when it comes to theorem proving. We still have a great deal to build in order to be productive at higher levels of abstraction.
eli_gottlieb 10y ago
>I would like my month spent on transitivity of subclassing back :( Oh God, that gave me flashbacks. I've done at least one transitivity of subtyping proof where I actually got the right theorem, then found later in the module that I had to rewrite the whole thing with a graph-theory library supplying some theorems about DAGs/finite posets. It's horrible, and that piece of work still isn't done!

hyperbovine 10y ago

> if you're well known and liked author, you often get a pass on your papers and they're not well checked for errors. A friend who was advised by a "famous" (i.e., in his/her field) mathematician told me basically the same thing. This person unquestionably has had brilliant insights during the course of their career, most of which turned out to be correct. But (s)he has also published several false results, including one "major" false result. Some mathematicians are known to be sloppy and the field puts up with it, which seems weird to me. Regarding Coq, never tried it, but here is my guess at what's going on. Coq seems to be mainly embraced by algebraists and people doing discrete math, less so in fields which are more analytic (optimization, probability, functional analysis, PDE, etc.) Proofs in the latter branches of math seem to more commonly invoke geometric or "intuitive" arguments which, while completely rigorous, are harder to reduce to a sequence of logical statements. Take for example "convexity implies continuity". You can basically prove this in 1d by drawing a picture, whereas the full, gory, rigorous version, though elementary, requires a little effort. Proofs in modern algebra, otoh, involve a lot of symbol pushing, which computers excel at. Just a guess.

deleted 10y ago
[deleted]

eli_gottlieb 10y ago

Analysis and the real numbers tend to be very hard to encode in constructive foundations. We still haven't got the right balance between checking for computability of the proof and all objects it hypothesizes, versus letting some of the types we hypothesize over be uncomputable and uncountably large, while requiring that propositional types (squash types) have continuous elements.