6 ms·

No one will ever bother to read this work. There are millions of claimed proofs of various conjectures. If you want to prove Goldbach or P=NP (etc...) you eit

No one will ever bother to read this work. There are millions of claimed proofs of various conjectures. If you want to prove Goldbach or P=NP (etc...) you either need a very simple to verify proof (not a 1,000 page proof) or you need to prove a set of interesting conjectures along the way to give yourself credibility. In the pages of this mathematician's proof, there must be a few smaller proofs he could publish that show genuine insight, which would give him credibility. Otherwise it's just another sci.math sideshow.

balsam 14y ago
true that. Say, if you wanted to modify a page on Wikiproof titled "Goldback conjecture" you have to first summarize your approach, with a tree diagram of subtheorems, and at least provide a few proofs of those subtheorems that are original, and of course, citations for those that aren't. Wikipedia for original work! It'll be fun to maintain, considering that it'll be like allowing advertisements on Wikipedia.
tinco 14y ago
I wonder if it's possible for an machine learning algorithm to simplify these proofs. I take it because of the rather strict domain specificness of math papers it should be possible to develop an algorithm that can parse these papers into lemmas. Proofs normally structured as a tree of lemmas right? Or are there proofs that have more complex structure? A single basic thing could be to extract the leaf lemmas and assert their validity. If they are valid, and the relations between the lemmas are valid then the eventual conclusion should also be valid. Has anything like this ever been attempted? A math paper proof verifying machine learning algorithm?
- jlouis 14y ago
  Automated Therom Proving is ridiculously hard and a guess would be that it is almost impossible to train an ML algorithm to do this efficiently. However, verifying that a proof is correct is somewhat simple, if you give the machine enough information to actually run the formalization details. In modern mathematics, this may be a necessary thing to do since nobody has time to verify these 1000 page developments anymore. The problem is that the level of detail currently needed is very high. And this slows down the formalization process. But the area is in wild development these years, so hopefully something good comes out of it.
  - jamesaguilar 14y ago
    Just imagine inputting the final character of the last inference step, then waiting for a few minutes while the computer performs incremental compilation of the last few rules. Finally, it emits simply these four characters: "QED."
    - dandrews 14y ago
      I like this, and it reminds me of the tagline from Asimov's The Last Question.
      - sp332 14y ago
        There was a billionaire in the book Permutation City who uploaded his brain into a supercomputer, then let an optimizer run on it for years. The goal was to get his brain to run in real-time or better, but eventually it spit out an empty file and a log message: "This program produces no output."
  - raverbashing 14y ago
    Yes Still, I think it would be better if mathematicians started writing their theorems and proofs in a machine readable way Of course there is no standart for that today that gets "everything". Something "let G be a Galois Group, let Xk be the set of all matrixes of dimension k,k where Det(x)=1" etc This is hard. But to put it in that way would allow for piecewise revision, reassembly, study and proof (not that you can't do that on paper, but it's much harder), and then you can start growing your machine programs around those proofs.
    - ColinWright 14y ago
      : I think it would be better if mathematicians : started writing their theorems and proofs in : a machine readable way And software would be more reliable if people used the correctness-proving systems that have been developed.
      - 14y ago
- nairboon 14y ago
  There are numerous projects for proof checking: https://en.wikipedia.org/wiki/Automated_proof_checking https://en.wikipedia.org/wiki/Automated_proof_checking Such an algorithm could consist of the following parts: * a parser * a syntax checker: to test how correct the used mathematical notation is * if possible translate non-standard notation to standard * using some sort of supervised learning for checking existing proofs with existing proof solvers * manual intervention: improve translator or underlying proof solver
pdeuchler 14y ago
No one will ever bother to read this work. Yeah... but what if? Aren't you the least bit curious?
- chris_wot 14y ago
  If it is 1000s of pages of work that is unintelligible to even killed mathematicians, then it might take years o someone's life to decode it into simpler terms. In the end, they may find a fatal flaw, or a series of flaws and where would they be? They'd have spent a lot of time and effort to disprove a theorem that nobody was interested in. That said, I look at the fact that there are still people working on Ramanujan's conjectures that there may still be some worth to it...
  - nnq 14y ago
    you meant "skilled" mathematicians... I hope :)
    - chris_wot 14y ago
      Sigh. iPad keyboard... :-(
  - ColinWright 14y ago
    > ...to even killed mathematicians ... I suspect you mean "skilled". > They'd have spent a lot of time and effort to > disprove a theorem that nobody was interested in. Not to disprove the theorem, but to invalidate the proof. the conjecture would remain open. > ... there are still people working on Ramanujan's > conjectures that there may still be some worth to > it ... Ramanujan has a proven track record. Even when he first sent material to Hardy it was ignored, and it was only because some of it looked immediately plausible that he started to check. Every initial check proved correct, and so he continued, growing in his conviction that the author had something with reading. In this case there is effectively nothing to suggest that this is worth reading.
    - chris_wot 14y ago
S4M 14y ago
I actually would like to give it a shot, even though I know that it's way too far beyond my level. But after googling Henry Andrew Pogorzelski, no pdf's came out. I think he should have written a paper explaining in easier term what he does. E.g "First I will map the integers into a group defined by X and Y, it makes the work easier because that group has some interesting properties like... Then I show how the Goldback conjecture translates onto my group, then, etc." I know this is easier to be said than to be done, but on the other hand the Goldback conjecture is so simple that there have to be ways to break down its demonstration (or attempts of) into understandable steps, each steps being once again broken down, etc. and each stage introducing new layers of complexity. That way, instead of claiming "I proved the Goldback conjecture, here is the proof, just check those 1000 pages", he could have said "I proved X, Y and Z, and we can see how together they can be added up to prove the actual conjecture", with X, Y and Z (and probably lots of others) being smaller results that experts could challenge or assert. EDIT: TL;DR: If a mathematician claims to prove a long time unproven claim such as Goldbach conjecture, it belongs to him to do the vulgarisation works so even schmucks like me can have a remove idea of how he did it.

balsam 14y ago

true that. Say, if you wanted to modify a page on Wikiproof titled "Goldback conjecture" you have to first summarize your approach, with a tree diagram of subtheorems, and at least provide a few proofs of those subtheorems that are original, and of course, citations for those that aren't. Wikipedia for original work! It'll be fun to maintain, considering that it'll be like allowing advertisements on Wikipedia.

tinco 14y ago

I wonder if it's possible for an machine learning algorithm to simplify these proofs. I take it because of the rather strict domain specificness of math papers it should be possible to develop an algorithm that can parse these papers into lemmas. Proofs normally structured as a tree of lemmas right? Or are there proofs that have more complex structure? A single basic thing could be to extract the leaf lemmas and assert their validity. If they are valid, and the relations between the lemmas are valid then the eventual conclusion should also be valid. Has anything like this ever been attempted? A math paper proof verifying machine learning algorithm?

jlouis 14y ago
Automated Therom Proving is ridiculously hard and a guess would be that it is almost impossible to train an ML algorithm to do this efficiently. However, verifying that a proof is correct is somewhat simple, if you give the machine enough information to actually run the formalization details. In modern mathematics, this may be a necessary thing to do since nobody has time to verify these 1000 page developments anymore. The problem is that the level of detail currently needed is very high. And this slows down the formalization process. But the area is in wild development these years, so hopefully something good comes out of it.
- jamesaguilar 14y ago
  Just imagine inputting the final character of the last inference step, then waiting for a few minutes while the computer performs incremental compilation of the last few rules. Finally, it emits simply these four characters: "QED."
  - dandrews 14y ago
    I like this, and it reminds me of the tagline from Asimov's The Last Question.
    - sp332 14y ago
      There was a billionaire in the book Permutation City who uploaded his brain into a supercomputer, then let an optimizer run on it for years. The goal was to get his brain to run in real-time or better, but eventually it spit out an empty file and a log message: "This program produces no output."
- raverbashing 14y ago
  Yes Still, I think it would be better if mathematicians started writing their theorems and proofs in a machine readable way Of course there is no standart for that today that gets "everything". Something "let G be a Galois Group, let Xk be the set of all matrixes of dimension k,k where Det(x)=1" etc This is hard. But to put it in that way would allow for piecewise revision, reassembly, study and proof (not that you can't do that on paper, but it's much harder), and then you can start growing your machine programs around those proofs.
  - ColinWright 14y ago
    : I think it would be better if mathematicians : started writing their theorems and proofs in : a machine readable way And software would be more reliable if people used the correctness-proving systems that have been developed.
    - 14y ago
nairboon 14y ago
There are numerous projects for proof checking: https://en.wikipedia.org/wiki/Automated_proof_checking https://en.wikipedia.org/wiki/Automated_proof_checking Such an algorithm could consist of the following parts: * a parser * a syntax checker: to test how correct the used mathematical notation is * if possible translate non-standard notation to standard * using some sort of supervised learning for checking existing proofs with existing proof solvers * manual intervention: improve translator or underlying proof solver

pdeuchler 14y ago

No one will ever bother to read this work. Yeah... but what if? Aren't you the least bit curious?

chris_wot 14y ago
If it is 1000s of pages of work that is unintelligible to even killed mathematicians, then it might take years o someone's life to decode it into simpler terms. In the end, they may find a fatal flaw, or a series of flaws and where would they be? They'd have spent a lot of time and effort to disprove a theorem that nobody was interested in. That said, I look at the fact that there are still people working on Ramanujan's conjectures that there may still be some worth to it...
- nnq 14y ago
  you meant "skilled" mathematicians... I hope :)
  - chris_wot 14y ago
    Sigh. iPad keyboard... :-(
- ColinWright 14y ago
  > ...to even killed mathematicians ... I suspect you mean "skilled". > They'd have spent a lot of time and effort to > disprove a theorem that nobody was interested in. Not to disprove the theorem, but to invalidate the proof. the conjecture would remain open. > ... there are still people working on Ramanujan's > conjectures that there may still be some worth to > it ... Ramanujan has a proven track record. Even when he first sent material to Hardy it was ignored, and it was only because some of it looked immediately plausible that he started to check. Every initial check proved correct, and so he continued, growing in his conviction that the author had something with reading. In this case there is effectively nothing to suggest that this is worth reading.
  - chris_wot 14y ago

S4M 14y ago

I actually would like to give it a shot, even though I know that it's way too far beyond my level. But after googling Henry Andrew Pogorzelski, no pdf's came out. I think he should have written a paper explaining in easier term what he does. E.g "First I will map the integers into a group defined by X and Y, it makes the work easier because that group has some interesting properties like... Then I show how the Goldback conjecture translates onto my group, then, etc." I know this is easier to be said than to be done, but on the other hand the Goldback conjecture is so simple that there have to be ways to break down its demonstration (or attempts of) into understandable steps, each steps being once again broken down, etc. and each stage introducing new layers of complexity. That way, instead of claiming "I proved the Goldback conjecture, here is the proof, just check those 1000 pages", he could have said "I proved X, Y and Z, and we can see how together they can be added up to prove the actual conjecture", with X, Y and Z (and probably lots of others) being smaller results that experts could challenge or assert. EDIT: TL;DR: If a mathematician claims to prove a long time unproven claim such as Goldbach conjecture, it belongs to him to do the vulgarisation works so even schmucks like me can have a remove idea of how he did it.