6 ms·

I feel less confident of my proofs than my programs, because I can't run them, to see what happens. Yes, there are proof assistents like coq, but mathematicians

I feel less confident of my proofs than my programs, because I can't run them, to see what happens. Yes, there are proof assistents like coq, but mathematicians look down on them. Proofs are usually about some very small thing, and require a tremendous amount of work. Then, there is a huge literature for guidance and reusable elements (though, a lot of work to use it), and peer review to check it (also labour intensive).

nerdponx 9y ago
I do not understand why mathematicians look down on proof assistants. I've heard this claim multiple times and it continues to make no sense to me. Are there any mathematicians here who can weigh in?
- znfi 9y ago
  Not really a mathematician, so take this with a grain of salt. I would guess there are probably several different reasons for "looking down" on proof assistants. On the one hand we have something like the 4-colour theorem where there is some kind of "proof", which is very large and incomprehensible. This is probably unsatisfactory to many because one is not really interested in just knowing that something is true, but ideally one also want an understanding of "why" something is true. This is, to various degrees, achived in more standard proofs. Another reason for disliking proof assistants is probably that they simply are very cumbersome to use and not very much can be proven with them so far. I would guess that even if you could get someone to admitt that the idea is cool and could be very useful, it's just not practical and for most people in mathematics it's just a distraction from what they are trying to work on at the moment. Compare with trying to convince someone that a flying car is really cool, yeah, sure, it probably would be, but so far it's basically sci-fi. If you want to work on building this, great, but most commuters will probably "look down" on your idea if you start bugging them about it.
- ufo 9y ago
  It is a bit similar to why we don't use program verification tools very much in software development. They are very complicated to use and while they do a good job at verifying existing code they don't help as much when writing code from scratch, because they tend to add extra obstacles at this stage. From what I have seen, proof assistants in math are used when extreme rigour is desired (which is not always the case) and when working with extremely long computational proofs with hundreds of cases (where you need to work at a higher abstraction level; a human writes a program that outputs the proof and then the proof checker verifies that this extremely long step by step proof is valid)
- knappa 9y ago
  Mathematician here: It isn't exactly that proof assistants are looked down upon. Rather, most of us don't do 1st order logic and it isn't on anybodies radar. Even if it were, it is often new proof techniques that lead to new interpretations, generalizations and discoveries about what we should be trying to prove in the first place. It is very hard to interpret a wall of 1st order logic. Not to mention decidability issues.
  - foobar__ 9y ago
    Both Isabelle and Coq are based on higher-order logics, so I am not sure how first-order logic is a barrier to entry. Especially Isabelle is very easy to use because the logic is so standard with nothing really surprising or especially restricting (a very strong form of the axiom of choice is deeply embedded in the system, so it's probably harder if you care about it at this level). Regarding your second point, to me this looks pretty much the same as in software: In high-quality code I expect high-level comments that give me intuition about the code, and I also expect high-level documentation giving me further intuition about the components and the system as a whole. The more complicated the system is, the more important the comments and the documentation become. I see no reason why we should hold computer-assisted proofs to a lesser standard.
- solomatov 9y ago
  I am not a professional mathematician but I worked with proof assistants semi-professionally. The problem is that proof assistants doesn't cover everything that is required by mathematicians, proofs are often verbose, and unreadable. There's some attempts to alleviate these problems, which are named Homotopy Type Theory, and they are quite successful.
  - hackermailman 9y ago
    Anybody interested, this 2016 paper is a general survey of the current proof logic refinement implementations out there, and the problems and limitations they have which they are currently trying to solve with dependent types/Computational Higher Type Theory http://www.redprl.org/pdfs/afpr.pdf http://www.redprl.org/pdfs/afpr.pdf
- deleted 9y ago
  [deleted]
- j2kun 9y ago
  It's because a good proof conveys human-level insight first and foremost, and the details are often mental baggage that can be sorted out later. Proof assistants are the opposite. Sacrifice intuition and insight for the sake of correctness. This is also why mathematicians love picture proofs.
  - foobar__ 9y ago
    I am not satisfied by picture proofs, I'd like to see derivations from axioms and known results. I love pictures that give me intuition about a proof and I agree that intuition is crucial to understanding. But all the intuition in the world is useless if the proof fails because of one tiny logically unsound step or one pathological corner case, so it's no good to ignore the technical details or, even worse, to become unable to expand a purpoted proof one has written into a fully detailed version, which I suppose can easily happen if someone relies too much on intuition.
    - j2kun 9y ago
      Of course you can't ignore details. I was explaining the source of emotions, which tend to drive whether one wants to adopt a particular tool or method. That being said, I often find convincing, false proofs as illuminating as true proofs, once the flaw is clear, because they highlight the nature of the conjecture. So I disagree with your claim that a proof can suddenly become useless due to a slight misstep. And for what it's worth, theorems are rarely thrown out due to pathological corner cases; at least I've never heard of this happening. Instead, if the insight conveyed by the proof is useful, it's called a partial result and the conditions are modified to fit the proof. Entire theories are built up specifically to avoid pathology (almost every mathematical field does this)
- kxyvr 9y ago
  I'm a professional mathematician and, candidly, most people in my subfield don't really know that they exist. I do, and would love to use them, but I find them very difficult to use and don't have good examples of proofs relevant to my work. To be specific, I've used Coq in the past to help verify properties of programs such as a sorted list really being sorted. That said, I primarily work in applied math areas such as optimization, numerical linear algebra, and numerical PDEs and I have no idea where to begin with fundamental proofs such as Newton's method converging quadratically within a certain neighborhood of the solution. Alternatively, I'd love to see formalized proofs of the theorems that we'd learn in a course in real analysis such as one based on Rudin's Principles of Mathematical Analysis. Really, if anyone has examples of these, please let me know. There's an amazing number of errors in published work. Most of the time, the work is still mostly right, but that's not OK. In my opinion, we'd be better off with formalized proofs.
  - EugeneAZ 9y ago
    > I primarily work in applied math areas such as optimization It may be rather an off-topic, but I suggest you to read my funny paper: https://docs.google.com/document/d/10pTRJFgwEGnUM5RF1CHX2OO5xZTwzyITHd4cjpZTsqw/edit https://docs.google.com/document/d/10pTRJFgwEGnUM5RF1CHX2OO5...

nerdponx 9y ago

I do not understand why mathematicians look down on proof assistants. I've heard this claim multiple times and it continues to make no sense to me. Are there any mathematicians here who can weigh in?

znfi 9y ago
Not really a mathematician, so take this with a grain of salt. I would guess there are probably several different reasons for "looking down" on proof assistants. On the one hand we have something like the 4-colour theorem where there is some kind of "proof", which is very large and incomprehensible. This is probably unsatisfactory to many because one is not really interested in just knowing that something is true, but ideally one also want an understanding of "why" something is true. This is, to various degrees, achived in more standard proofs. Another reason for disliking proof assistants is probably that they simply are very cumbersome to use and not very much can be proven with them so far. I would guess that even if you could get someone to admitt that the idea is cool and could be very useful, it's just not practical and for most people in mathematics it's just a distraction from what they are trying to work on at the moment. Compare with trying to convince someone that a flying car is really cool, yeah, sure, it probably would be, but so far it's basically sci-fi. If you want to work on building this, great, but most commuters will probably "look down" on your idea if you start bugging them about it.
ufo 9y ago
It is a bit similar to why we don't use program verification tools very much in software development. They are very complicated to use and while they do a good job at verifying existing code they don't help as much when writing code from scratch, because they tend to add extra obstacles at this stage. From what I have seen, proof assistants in math are used when extreme rigour is desired (which is not always the case) and when working with extremely long computational proofs with hundreds of cases (where you need to work at a higher abstraction level; a human writes a program that outputs the proof and then the proof checker verifies that this extremely long step by step proof is valid)
knappa 9y ago
Mathematician here: It isn't exactly that proof assistants are looked down upon. Rather, most of us don't do 1st order logic and it isn't on anybodies radar. Even if it were, it is often new proof techniques that lead to new interpretations, generalizations and discoveries about what we should be trying to prove in the first place. It is very hard to interpret a wall of 1st order logic. Not to mention decidability issues.
- foobar__ 9y ago
  Both Isabelle and Coq are based on higher-order logics, so I am not sure how first-order logic is a barrier to entry. Especially Isabelle is very easy to use because the logic is so standard with nothing really surprising or especially restricting (a very strong form of the axiom of choice is deeply embedded in the system, so it's probably harder if you care about it at this level). Regarding your second point, to me this looks pretty much the same as in software: In high-quality code I expect high-level comments that give me intuition about the code, and I also expect high-level documentation giving me further intuition about the components and the system as a whole. The more complicated the system is, the more important the comments and the documentation become. I see no reason why we should hold computer-assisted proofs to a lesser standard.
solomatov 9y ago
I am not a professional mathematician but I worked with proof assistants semi-professionally. The problem is that proof assistants doesn't cover everything that is required by mathematicians, proofs are often verbose, and unreadable. There's some attempts to alleviate these problems, which are named Homotopy Type Theory, and they are quite successful.
- hackermailman 9y ago
  Anybody interested, this 2016 paper is a general survey of the current proof logic refinement implementations out there, and the problems and limitations they have which they are currently trying to solve with dependent types/Computational Higher Type Theory http://www.redprl.org/pdfs/afpr.pdf http://www.redprl.org/pdfs/afpr.pdf
deleted 9y ago
[deleted]
j2kun 9y ago
It's because a good proof conveys human-level insight first and foremost, and the details are often mental baggage that can be sorted out later. Proof assistants are the opposite. Sacrifice intuition and insight for the sake of correctness. This is also why mathematicians love picture proofs.
- foobar__ 9y ago
  I am not satisfied by picture proofs, I'd like to see derivations from axioms and known results. I love pictures that give me intuition about a proof and I agree that intuition is crucial to understanding. But all the intuition in the world is useless if the proof fails because of one tiny logically unsound step or one pathological corner case, so it's no good to ignore the technical details or, even worse, to become unable to expand a purpoted proof one has written into a fully detailed version, which I suppose can easily happen if someone relies too much on intuition.
  - j2kun 9y ago
    Of course you can't ignore details. I was explaining the source of emotions, which tend to drive whether one wants to adopt a particular tool or method. That being said, I often find convincing, false proofs as illuminating as true proofs, once the flaw is clear, because they highlight the nature of the conjecture. So I disagree with your claim that a proof can suddenly become useless due to a slight misstep. And for what it's worth, theorems are rarely thrown out due to pathological corner cases; at least I've never heard of this happening. Instead, if the insight conveyed by the proof is useful, it's called a partial result and the conditions are modified to fit the proof. Entire theories are built up specifically to avoid pathology (almost every mathematical field does this)
kxyvr 9y ago
I'm a professional mathematician and, candidly, most people in my subfield don't really know that they exist. I do, and would love to use them, but I find them very difficult to use and don't have good examples of proofs relevant to my work. To be specific, I've used Coq in the past to help verify properties of programs such as a sorted list really being sorted. That said, I primarily work in applied math areas such as optimization, numerical linear algebra, and numerical PDEs and I have no idea where to begin with fundamental proofs such as Newton's method converging quadratically within a certain neighborhood of the solution. Alternatively, I'd love to see formalized proofs of the theorems that we'd learn in a course in real analysis such as one based on Rudin's Principles of Mathematical Analysis. Really, if anyone has examples of these, please let me know. There's an amazing number of errors in published work. Most of the time, the work is still mostly right, but that's not OK. In my opinion, we'd be better off with formalized proofs.
- EugeneAZ 9y ago
  > I primarily work in applied math areas such as optimization It may be rather an off-topic, but I suggest you to read my funny paper: https://docs.google.com/document/d/10pTRJFgwEGnUM5RF1CHX2OO5xZTwzyITHd4cjpZTsqw/edit https://docs.google.com/document/d/10pTRJFgwEGnUM5RF1CHX2OO5...