4 ms·

Regardless, unproven theorems should not make it to publish papers. At the very least, they should be marked as "conjectures".

gizmo686 8y ago
There is a difference between unproven, and the published proof contains a mistake.
- loup-vaillant 8y ago
  Seriously, who cares? When you publish the proof for a theorem, you're generally the first to do so. Aren't you? If there is an error in the only published proof ever, your theorem is unproven. QED. Edit: to downvoters: please explain my error. I thought I was only telling the obvious here.
  - cma 8y ago
    Maybe they feel you didn't rigorously prove your case.
    - loup-vaillant 8y ago
      They more likely didn't read past the first sentence. I suspect a very thin skin. Seriously though, I don't know what makes this forum tick. Someone's gotta explain what is socially acceptable around here. I know we're not supposed to complain about votes here, but I genuinely don't understand what happened. (Or rather, what is happening, the votes seem to flow up and down for no discernible reason.)
      - pvg 8y ago
        Whining about downvotes and then trying to goad other users is bad and you shouldn't do it.
        loup-vaillant 8y ago
        Perhaps, but it looked like it worked. Somehow. For now. At the time I write this, the comment you are replying to is still positive (edit: oops, no longer), while it clearly breaks the stated rules of this forum (sated both officially and by you just now). And I'm pretty sure that if I didn't do it, my "who cares" comment above would have been further downvoted. I observed this several times on several forums, sometimes votes have a momentum, and breaking the rules like I did can sometimes stop that momentum. (This works the other way too: popular comments often stop having further upvotes after the first reply that disagrees.) Incidentally, I really think a good proportion of downvoters hit the button before reaching the end of the comment. Not because they're personally offended, but because their troll filter judge quickly, from the very first words (thinking back with a cooler head, I can't blame them). Starting a comment by something that looks offensive if taken out of context is a pretty sure way to get it downvoted to oblivion. Still, the threshold looks pretty damn low.
        pvg 8y ago
        Perhaps, but it looked like it worked. That's not the reason you shouldn't whine about downvotes or goad other users. Not a 'perhaps' thing.
        loup-vaillant 8y ago
        I wouldn't know about any absolute rule. Including "thou shalt not eat babies", if the circumstances are extreme enough. I understand why complaining about downvotes is looked down upon (off topic, distracting, feed the troll…), but there are cases where those are both unexpected and unwarranted. I mean, I originally replied to a comment that didn't add to the discussion with a comment that did. What was I supposed to do with it? What am I supposed to learn from it? Not even you provided any meaningful feedback.
        pvg 8y ago
        What am I supposed to learn from it? That not everything is about you is a decent start.
  - Bahamut 8y ago
    Not all published proofs are necessarily proving a new theorem. Sometimes they are new approaches to proving known theorems. One example of that is the Prime Number Theorem, for which there have been multiple proofs over the years exploring different angles.
amelius 8y ago
Translating this to computer science/programming: what would you call an unproven program?
- barrkel 8y ago
  One that fails to compile with a type error. Probably, pseudocode - enough to convey the concept, but eliding some details that a compiler may require.
- loup-vaillant 8y ago
  One that isn't machine checked to conform to the specification (with Coq or similar). My standard is even higher for programs than it is for mathematical statements, because they tend to be orders of magnitude more complex. On the other hand, it's okay for a program to not be proven, because it can be useful even if it has bugs.
  - AnimalMuppet 8y ago
    > On the other hand, it's okay for a program to not be proven, because it can be useful even if it has bugs. True, and a very important point. But... if the program has bugs, do they affect the results? Do they affect the results enough to matter? How do you know? In particular, what is your objective proof that the program does what you need it to do? For many programs, such concerns are extreme overkill. For some, though, you have to prove that it does what you need it to.
    - loup-vaillant 8y ago
      That's where you quit proofs, and start experimenting. I found tests to be extremely effective at rooting out most bugs. Especially if you use property based tests. Programs that do need a proof still have model checkers like TLA+, and proof assistants like Coq.
      - AnimalMuppet 8y ago
        Sure, tests are part of what I meant by "objective evidence".

gizmo686 8y ago

There is a difference between unproven, and the published proof contains a mistake.

loup-vaillant 8y ago
Seriously, who cares? When you publish the proof for a theorem, you're generally the first to do so. Aren't you? If there is an error in the only published proof ever, your theorem is unproven. QED. Edit: to downvoters: please explain my error. I thought I was only telling the obvious here.
- cma 8y ago
  Maybe they feel you didn't rigorously prove your case.
  - loup-vaillant 8y ago
    They more likely didn't read past the first sentence. I suspect a very thin skin. Seriously though, I don't know what makes this forum tick. Someone's gotta explain what is socially acceptable around here. I know we're not supposed to complain about votes here, but I genuinely don't understand what happened. (Or rather, what is happening, the votes seem to flow up and down for no discernible reason.)
    - pvg 8y ago
      Whining about downvotes and then trying to goad other users is bad and you shouldn't do it.
      - loup-vaillant 8y ago
        Perhaps, but it looked like it worked. Somehow. For now. At the time I write this, the comment you are replying to is still positive (edit: oops, no longer), while it clearly breaks the stated rules of this forum (sated both officially and by you just now). And I'm pretty sure that if I didn't do it, my "who cares" comment above would have been further downvoted. I observed this several times on several forums, sometimes votes have a momentum, and breaking the rules like I did can sometimes stop that momentum. (This works the other way too: popular comments often stop having further upvotes after the first reply that disagrees.) Incidentally, I really think a good proportion of downvoters hit the button before reaching the end of the comment. Not because they're personally offended, but because their troll filter judge quickly, from the very first words (thinking back with a cooler head, I can't blame them). Starting a comment by something that looks offensive if taken out of context is a pretty sure way to get it downvoted to oblivion. Still, the threshold looks pretty damn low.
        pvg 8y ago
        Perhaps, but it looked like it worked. That's not the reason you shouldn't whine about downvotes or goad other users. Not a 'perhaps' thing.
        loup-vaillant 8y ago
        I wouldn't know about any absolute rule. Including "thou shalt not eat babies", if the circumstances are extreme enough. I understand why complaining about downvotes is looked down upon (off topic, distracting, feed the troll…), but there are cases where those are both unexpected and unwarranted. I mean, I originally replied to a comment that didn't add to the discussion with a comment that did. What was I supposed to do with it? What am I supposed to learn from it? Not even you provided any meaningful feedback.
        pvg 8y ago
        What am I supposed to learn from it? That not everything is about you is a decent start.
- Bahamut 8y ago
  Not all published proofs are necessarily proving a new theorem. Sometimes they are new approaches to proving known theorems. One example of that is the Prime Number Theorem, for which there have been multiple proofs over the years exploring different angles.

amelius 8y ago

Translating this to computer science/programming: what would you call an unproven program?

barrkel 8y ago
One that fails to compile with a type error. Probably, pseudocode - enough to convey the concept, but eliding some details that a compiler may require.
loup-vaillant 8y ago
One that isn't machine checked to conform to the specification (with Coq or similar). My standard is even higher for programs than it is for mathematical statements, because they tend to be orders of magnitude more complex. On the other hand, it's okay for a program to not be proven, because it can be useful even if it has bugs.
- AnimalMuppet 8y ago
  > On the other hand, it's okay for a program to not be proven, because it can be useful even if it has bugs. True, and a very important point. But... if the program has bugs, do they affect the results? Do they affect the results enough to matter? How do you know? In particular, what is your objective proof that the program does what you need it to do? For many programs, such concerns are extreme overkill. For some, though, you have to prove that it does what you need it to.
  - loup-vaillant 8y ago
    That's where you quit proofs, and start experimenting. I found tests to be extremely effective at rooting out most bugs. Especially if you use property based tests. Programs that do need a proof still have model checkers like TLA+, and proof assistants like Coq.
    - AnimalMuppet 8y ago
      Sure, tests are part of what I meant by "objective evidence".