4 ms·

This is quite interesting, especially since one of the major objections to computer-aided proofs has that they are more difficult for humans to understand. Com

This is quite interesting, especially since one of the major objections to computer-aided proofs has that they are more difficult for humans to understand. Common wisdom has been that proof techniques matter more than the results, but if human-authored proofs are no longer being inspected, it seems like it's just a matter of time before computer-aided proofs take over. I wonder how long it will be before proof assistants (like Lean, Coq, etc.) become ergonomic enough that the average non-technical math researcher will feel social pressure to publish a computer-aided proof along with their result.

plake 5y ago
I think it will be quite some time yet. As a researcher, my objection to computer-aided proofs is not that they're hard to read -- you would of course write a human readable version to go with it -- but rather that they're extremely time-consuming to write. (And writing papers is hard enough already.) A typical research paper is written at a very high level; often steps in the argument will assume the reader is also a skilled mathematician, and invite them to fill in the lower-level details themselves. This reasoning is as much intuitive as it is formal; I suspect it will be a while before proof assistants are as intelligent as the typical reader of a mathematics paper. I think there's an outside perspective that if math isn't 100% logically verified, it's worthless, which doesn't really match up with my own experience. Most results rely more on the intuition of the authors than on the precise logic they write down; thus the surprising result that papers with logical gaps are, very often, still correct.
- benrbray 5y ago
  That's basically what I meant by "ergonomics" -- do you think we're still quite far from researchers being able to develop their own "tactics" to automate the sort of reasoning that would normally be "left as an exercise" to the reader of a research publication?
  - plake 5y ago
    Yeah, "left as an exercise" can mean anything from "this is an undergraduate exercise" to "if you understand both the field and this paper, you could write a different, much longer paper, and we both know this, so let's assume I wrote that one." It's probably not impossible to build a proof language that makes that kind of thing doable, but I suspect that (a) it would be genuinely difficult to operate it skilfully, much as being a really good developer is difficult, and (b) it would take a huge collective effort on behalf of each research community to prove the foundational results everyone relies on. Whereas the system we have right now, despite sounding kind of weird to outsiders, mostly works okay? I'm just not sure a switch to formal proofs would be worth the time investment -- or that you could convince the many researchers less interested in tech than myself.
    - daxfohl 5y ago
      I came here to say that maybe it makes things simpler though when everyone speaks the same language, and all proofs are written in the same format. However then I remembered the new codebase I inherited and OMG it's such a mess because somehow just converting a UI enum to a DB enum is a 25-line function that's repeated over and over everywhere. (Needs to be version-safe for different clients that may have old enum values, needs to create error message in appropriate language, etc, and the callers are in different layers and all have different ways of getting the corresponding info). So yeah maybe the high-level "I get it, you get it, we all get it, let's just state this an move on" is better.
jkhdigital 5y ago
This is an explicit goal of one of of the creators of homotopy type theory, Fields medalist Vladimir Voevodksy: https://www.ias.edu/ideas/2014/voevodsky-origins https://www.ias.edu/ideas/2014/voevodsky-origins Apparently he now uses Coq in his everyday work.
- alexilliamson 5y ago
  He's been dead for four years?
  - dhosek 5y ago
    Apparently he didn’t shut down his computer before he died.
    - queuebert 5y ago
      Dat uptime tho
  - jkhdigital 5y ago
    Oh snap, I had no idea that he died! Wow... that's a profound loss for the field of mathematics.
aaronlevin 5y ago
The main objection to computer-aided proofs is not that they are more difficult for humans to understand. The main objection is that most proof-assistants use a different logical foundation than modern mathematics. Modern mathematics is built on ZFC[0] whereas most proof assistants, such as Coq, Isabelle, Agda, etc use different logical foundations, such as the Calculus of Constructions[1]. Many important results in modern mathematics are not easily stated or proven in systems such as CoC[1]. For example, Brouwer's _Fixed Point Theorem_[2], a pretty bog standard result in Topology that is useful to proof many things in Functional Analysis, has a clear statement in ZFC, but does not, to my knowledge, have an equivalent in CoC (and if it does it will be stated radically different). [0]: https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... [1]: https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions [2]: https://en.wikipedia.org/wiki/Brouwer_fixed-point_theorem https://en.wikipedia.org/wiki/Brouwer_fixed-point_theorem

plake 5y ago

I think it will be quite some time yet. As a researcher, my objection to computer-aided proofs is not that they're hard to read -- you would of course write a human readable version to go with it -- but rather that they're extremely time-consuming to write. (And writing papers is hard enough already.) A typical research paper is written at a very high level; often steps in the argument will assume the reader is also a skilled mathematician, and invite them to fill in the lower-level details themselves. This reasoning is as much intuitive as it is formal; I suspect it will be a while before proof assistants are as intelligent as the typical reader of a mathematics paper. I think there's an outside perspective that if math isn't 100% logically verified, it's worthless, which doesn't really match up with my own experience. Most results rely more on the intuition of the authors than on the precise logic they write down; thus the surprising result that papers with logical gaps are, very often, still correct.

benrbray 5y ago
That's basically what I meant by "ergonomics" -- do you think we're still quite far from researchers being able to develop their own "tactics" to automate the sort of reasoning that would normally be "left as an exercise" to the reader of a research publication?
- plake 5y ago
  Yeah, "left as an exercise" can mean anything from "this is an undergraduate exercise" to "if you understand both the field and this paper, you could write a different, much longer paper, and we both know this, so let's assume I wrote that one." It's probably not impossible to build a proof language that makes that kind of thing doable, but I suspect that (a) it would be genuinely difficult to operate it skilfully, much as being a really good developer is difficult, and (b) it would take a huge collective effort on behalf of each research community to prove the foundational results everyone relies on. Whereas the system we have right now, despite sounding kind of weird to outsiders, mostly works okay? I'm just not sure a switch to formal proofs would be worth the time investment -- or that you could convince the many researchers less interested in tech than myself.
  - daxfohl 5y ago
    I came here to say that maybe it makes things simpler though when everyone speaks the same language, and all proofs are written in the same format. However then I remembered the new codebase I inherited and OMG it's such a mess because somehow just converting a UI enum to a DB enum is a 25-line function that's repeated over and over everywhere. (Needs to be version-safe for different clients that may have old enum values, needs to create error message in appropriate language, etc, and the callers are in different layers and all have different ways of getting the corresponding info). So yeah maybe the high-level "I get it, you get it, we all get it, let's just state this an move on" is better.

jkhdigital 5y ago

This is an explicit goal of one of of the creators of homotopy type theory, Fields medalist Vladimir Voevodksy: https://www.ias.edu/ideas/2014/voevodsky-origins https://www.ias.edu/ideas/2014/voevodsky-origins Apparently he now uses Coq in his everyday work.

alexilliamson 5y ago
He's been dead for four years?
- dhosek 5y ago
  Apparently he didn’t shut down his computer before he died.
  - queuebert 5y ago
    Dat uptime tho
- jkhdigital 5y ago
  Oh snap, I had no idea that he died! Wow... that's a profound loss for the field of mathematics.

aaronlevin 5y ago

The main objection to computer-aided proofs is not that they are more difficult for humans to understand. The main objection is that most proof-assistants use a different logical foundation than modern mathematics. Modern mathematics is built on ZFC[0] whereas most proof assistants, such as Coq, Isabelle, Agda, etc use different logical foundations, such as the Calculus of Constructions[1]. Many important results in modern mathematics are not easily stated or proven in systems such as CoC[1]. For example, Brouwer's _Fixed Point Theorem_[2], a pretty bog standard result in Topology that is useful to proof many things in Functional Analysis, has a clear statement in ZFC, but does not, to my knowledge, have an equivalent in CoC (and if it does it will be stated radically different). [0]: https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... [1]: https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions [2]: https://en.wikipedia.org/wiki/Brouwer_fixed-point_theorem https://en.wikipedia.org/wiki/Brouwer_fixed-point_theorem