49 ms·

Nontrivially fillable gaps in published proofs of major theorems

77 points by mathgenius 7y ago

chisleu 7y ago
In the south, I don't think we really did. It evolved, sure, but the southern accent is based on southern english royalty.
- seanhunter 7y ago
  I think the parent comment relates to a different subject. https://news.ycombinator.com/item?id=22288440 https://news.ycombinator.com/item?id=22288440 specifically.
enricozb 7y ago
Hopefully as theorem provers improve and become more expressive, we can begin to state these theorems and even formalize proofs of them, letting a computer verify the proof for us. Check out Lean[1] if this sounds interesting to you. [1]: https://leanprover.github.io/ https://leanprover.github.io/
- gpm 7y ago
  I've been checking out lean in my spare time over the last week. While it seems like a nice formal proof checker, it doesn't seem to have any automated their theorem proving abilities yet? I can't imagine trying to do math where I have to manually supply a proof of every trivial statement... Something like Isabelle and it's sledgehammer automated proof finder seems more reasonable to me (which I hope to find time to dip my toes into this week). Am I missing something?
  - bonoboTP 7y ago
    I assume it could be done by having a "library" of such trivial statements. It's like in programming: we wouldn't want to deal with trivialities like how to decode utf8 or deal with files in a high level app, so we use libraries/APIs. You have to memorize them to some extent, but there can be autocomplete, documentation etc, just like in programming. Surely it needs a different mentality compared to old fashioned idealist type math people who may dislike such mechanization as taking the "soul and art" out of pencil and paper math, but I think the new generation of math people do have more overlap with CS-like thinking and they would be onboard.
    - gpm 7y ago
      Trivial statements of the kind I'm talking about are often incredibly proof specific, because they are often of the form "take the proof context and rephrase it so a pre proven theorem applies". Not the type of thing that can be enumerated in a library.
      - bonoboTP 7y ago
        Well, I'm not a mathematician, but it seems like if it's really trivial, it shouldn't be hard to formalize on a high level why it's true, like almost in natural language and then compile that high-level expression into a lower level argument. And if it's hard to even do that, then is the statement really trivial, or is it perhaps something that seems intuitive, but may not be sure (perhaps some pathological edge case may apply)?
        gpm 7y ago
        So here's a dumb example I just came up with. Let's say we know that x = 3^a 5^b. It's a trivial fact at this point that x isn't divisible by 2 (by the fact that prime factorization is unique). Disclaimer: I'm not actually good enough with lean to prove this sort of statement quickly... I could be under or even over selling lean here, hence why I phrased my original comment as a question about whether I was missing something. If I was trying to prove this formally, I'd have to say something like (in computer speak): Suppose x is divisible by 2, x = 2 * y, y has a prime factorization p by <theorem in library>, and 2 * p is therefore a prime factorization of x (ouch, already not sure how to specify that statement). 2 * p = x = 3^a 5^b, so 2 * p = 3^a 5^b. Both are prime factorizations, prime factorizations are unique by <theorem>, therefore both expressions should have the same number of 2 terms, but the one on the left has at least one, and the one on the right has 0, so they don't. This is a contradiction, so x is not divisible by two. You see why I'd like a computer to fill in the long formal proof instead of doing it myself? It's not because the statement might be false, it's because it's a pain to phrase everything in terms of the re-usable result about unique prime factorization. While I'm disclaiming things, disclaimer 2: I'm a hobbyist, not a real mathematician.
btrettel 7y ago
In my experience, Linus's law [1] is false in scientific research. There's a popular view that peer review is a strong filter that allows other researchers to have confidence that a claim is correct. My guess is that this might contribute to Linus's law being false, because many researchers actually do seem to think "it's been checked, so it must be okay, I don't need to check anything myself". Or, perhaps, people don't do much checking in the first place. My view is that peer review is a fairly low (and random) bar to pass that doesn't necessarily say much about the validity of a work. More people should check things more carefully. Recently I got reviews for a paper I wrote back, and a reviewer was skeptical of one claim I made because (paraphrasing) "If this were true, that would mean all previous researchers were wrong." They're exaggerating as it would only mean many researchers were wrong; I think some were skeptical of this for a long but kept quiet about it. But the idea that "everyone seemed to accept it, therefore you are probably wrong" independent of any arguments made seems popular, despite it being obviously fallacious. I have some arguments. The reviewer should engage with those arguments rather than make some appeal to popularity. Edit: To be clear, what I was claiming here would overturn something dating back to the 1930s that last received a well-accepted revision about 40 years ago. [1] https://en.wikipedia.org/wiki/Linus%27s_law https://en.wikipedia.org/wiki/Linus%27s_law
- rtkwe 7y ago
  I think the bigger reason it's false in science while somewhat more true in CS is that it's basically free to check the source code for something and setup a small localhost test where replication in science is tough and expensive. Even if someone does have the funds to check experimental descriptions don't actually cover all the details usually and there's some combination of small but important details left out and well meaning but imperfect directions. Also there's just the fact that in CS we're working on a defined system. From top to bottom it's possible to definitively say when I execute X the following Y things happen. The details may be buried deep within the hardware for the truly eldritch bugs but fundamentally it's all human defined and the bits that do exist outside human design are well understood enough they can largely be ignored (no one is reasonably going to find a bug that traces down to some unknown quirk of semiconductor physics). In the sciences we're poking at the edges to see what the system actually is.
beleuze 7y ago
related: Epistemic Injustice in Mathematics (2018) Rittberg, Colin Jakob and Tanswell, Fenner Stanley and Van Bendegem, Jean Paul. http://philsci-archive.pitt.edu/15133/ http://philsci-archive.pitt.edu/15133/
downerending 7y ago
Better: Gaps not trivially fillable... That is, the point is that the gaps cannot be trivially filled.

77 points by mathgenius 7y ago

In the south, I don't think we really did. It evolved, sure, but the southern accent is based on southern english royalty.

seanhunter 7y ago
I think the parent comment relates to a different subject. https://news.ycombinator.com/item?id=22288440 https://news.ycombinator.com/item?id=22288440 specifically.

enricozb 7y ago

Hopefully as theorem provers improve and become more expressive, we can begin to state these theorems and even formalize proofs of them, letting a computer verify the proof for us. Check out Lean[1] if this sounds interesting to you. [1]: https://leanprover.github.io/ https://leanprover.github.io/

gpm 7y ago
I've been checking out lean in my spare time over the last week. While it seems like a nice formal proof checker, it doesn't seem to have any automated their theorem proving abilities yet? I can't imagine trying to do math where I have to manually supply a proof of every trivial statement... Something like Isabelle and it's sledgehammer automated proof finder seems more reasonable to me (which I hope to find time to dip my toes into this week). Am I missing something?
- bonoboTP 7y ago
  I assume it could be done by having a "library" of such trivial statements. It's like in programming: we wouldn't want to deal with trivialities like how to decode utf8 or deal with files in a high level app, so we use libraries/APIs. You have to memorize them to some extent, but there can be autocomplete, documentation etc, just like in programming. Surely it needs a different mentality compared to old fashioned idealist type math people who may dislike such mechanization as taking the "soul and art" out of pencil and paper math, but I think the new generation of math people do have more overlap with CS-like thinking and they would be onboard.
  - gpm 7y ago
    Trivial statements of the kind I'm talking about are often incredibly proof specific, because they are often of the form "take the proof context and rephrase it so a pre proven theorem applies". Not the type of thing that can be enumerated in a library.
    - bonoboTP 7y ago
      Well, I'm not a mathematician, but it seems like if it's really trivial, it shouldn't be hard to formalize on a high level why it's true, like almost in natural language and then compile that high-level expression into a lower level argument. And if it's hard to even do that, then is the statement really trivial, or is it perhaps something that seems intuitive, but may not be sure (perhaps some pathological edge case may apply)?
      - gpm 7y ago
        So here's a dumb example I just came up with. Let's say we know that x = 3^a 5^b. It's a trivial fact at this point that x isn't divisible by 2 (by the fact that prime factorization is unique). Disclaimer: I'm not actually good enough with lean to prove this sort of statement quickly... I could be under or even over selling lean here, hence why I phrased my original comment as a question about whether I was missing something. If I was trying to prove this formally, I'd have to say something like (in computer speak): Suppose x is divisible by 2, x = 2 * y, y has a prime factorization p by <theorem in library>, and 2 * p is therefore a prime factorization of x (ouch, already not sure how to specify that statement). 2 * p = x = 3^a 5^b, so 2 * p = 3^a 5^b. Both are prime factorizations, prime factorizations are unique by <theorem>, therefore both expressions should have the same number of 2 terms, but the one on the left has at least one, and the one on the right has 0, so they don't. This is a contradiction, so x is not divisible by two. You see why I'd like a computer to fill in the long formal proof instead of doing it myself? It's not because the statement might be false, it's because it's a pain to phrase everything in terms of the re-usable result about unique prime factorization. While I'm disclaiming things, disclaimer 2: I'm a hobbyist, not a real mathematician.

btrettel 7y ago

In my experience, Linus's law [1] is false in scientific research. There's a popular view that peer review is a strong filter that allows other researchers to have confidence that a claim is correct. My guess is that this might contribute to Linus's law being false, because many researchers actually do seem to think "it's been checked, so it must be okay, I don't need to check anything myself". Or, perhaps, people don't do much checking in the first place. My view is that peer review is a fairly low (and random) bar to pass that doesn't necessarily say much about the validity of a work. More people should check things more carefully. Recently I got reviews for a paper I wrote back, and a reviewer was skeptical of one claim I made because (paraphrasing) "If this were true, that would mean all previous researchers were wrong." They're exaggerating as it would only mean many researchers were wrong; I think some were skeptical of this for a long but kept quiet about it. But the idea that "everyone seemed to accept it, therefore you are probably wrong" independent of any arguments made seems popular, despite it being obviously fallacious. I have some arguments. The reviewer should engage with those arguments rather than make some appeal to popularity. Edit: To be clear, what I was claiming here would overturn something dating back to the 1930s that last received a well-accepted revision about 40 years ago. [1] https://en.wikipedia.org/wiki/Linus%27s_law https://en.wikipedia.org/wiki/Linus%27s_law

rtkwe 7y ago
I think the bigger reason it's false in science while somewhat more true in CS is that it's basically free to check the source code for something and setup a small localhost test where replication in science is tough and expensive. Even if someone does have the funds to check experimental descriptions don't actually cover all the details usually and there's some combination of small but important details left out and well meaning but imperfect directions. Also there's just the fact that in CS we're working on a defined system. From top to bottom it's possible to definitively say when I execute X the following Y things happen. The details may be buried deep within the hardware for the truly eldritch bugs but fundamentally it's all human defined and the bits that do exist outside human design are well understood enough they can largely be ignored (no one is reasonably going to find a bug that traces down to some unknown quirk of semiconductor physics). In the sciences we're poking at the edges to see what the system actually is.

beleuze 7y ago

related: Epistemic Injustice in Mathematics (2018) Rittberg, Colin Jakob and Tanswell, Fenner Stanley and Van Bendegem, Jean Paul. http://philsci-archive.pitt.edu/15133/ http://philsci-archive.pitt.edu/15133/

downerending 7y ago

Better: Gaps not trivially fillable... That is, the point is that the gaps cannot be trivially filled.