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.
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.
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?
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.
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."
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."
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.
So, you're saying that the code would be less reliable if there was no work to prove it formally? Of course you aren't. What you're saying is that proving code is correct is insufficient. Of course it is insufficient. Your comment adds nothing to the debate.
What I'm saying is that asking that mathematicians produce their proofs in a form amenable to mechanical checking is like asking programmers to produce their code in a form that is amenable to mechanical checking. It's long, tedious, error-prone in its own right, and simply not going to happen. It's like asking people who write multi-million line programs in high-level languages to get the same functionality by writing in assembler.
Programming doesn't happen like that, and proofs don't either.
And your comment adds nothing to the debate while picking on a joke.
"is like asking programmers to produce their code in a form that is amenable to mechanical checking. It's long, tedious, error-prone in its own right, and simply not going to happen"
But programs are done in a form that's subject to mechanical checking. Compilers do that and only compile code that adheres to a strict syntax and grammar. In a higher level there are static code analysers that look for other defects. Some of them are in compilers already for optimization purposes.
Also, semiconductor companies use automated checkers for the inner parts of their processors, like floating point multipliers to make sure they are correct.
But running code through a compiler is akin to making sure the statements in a proof "make sense." The proof as a whole can be complete rubbish, which still making sense at a page by page level. I can't work out if you're trolling, or if you really don't understand my point.
A lot of undergraduate mathematics has been converted into forms that automated proof checkers can work with, and have verified. But new math just isn't like that. It's not yet well understood, it's got small gaps and bits that are wrong in inconsequential ways, and it's got an over-arching sense of purpose and meaning. Trying to convert a recently produced proof into a form amenable to checking is just not going to happen, and by the time it is understood well enough, and completed to a sufficient level of detail to make it possible in a sensible amount of time, it's pretty much pointless.
"But running code through a compiler is akin to making sure the statements in a proof "make sense." The proof as a whole can be complete rubbish, which still making sense at a page by page level."
Correct. But if one statement is incorrect then the proof is wrong, at least until that statement is corrected.
So it's only a partial verification, but you can be sure that if that points to an error, you still have work to do.
Code analyzers are getting better everyday but in the end it depends on what you want the code to do, so you would need to add an annotation "prove this function calculates 2*x for parameter x" for a complete proof
" Trying to convert a recently produced proof into a form amenable to checking is just not going to happen, and by the time is is understood well enough, and completed to a sufficient level of detail to make it possible in a sensible amount of time, it's pretty much pointless."
And that's where I disagree. If you can have your new theorem
in a machine readable/verifiable format, then other theorems can make use of it.
The idea is not to redo the work every time for a new theorem. I understand new math is much more complex, and that's why we should be thinking of making this available in a theorem prover.
It's certainly a very complex work and maybe not doable today, but it would have a big impact.
>> The proof as a whole can be complete rubbish, which
>> still making sense at a page by page level."
> Correct. But if one statement is incorrect then the proof
> is wrong, at least until that statement is corrected.
The statement-by-statement work is not only trivial, it's an important step to getting your head in the right place to understand where things are going, and why. Fixing the problem of making sure each statement is, in effect, syntactically correct is not just solving the wrong problem, it's solving a non-problem.
>> Trying to convert a recently produced proof into a form amenable
>> to checking is just not going to happen, and by the time it is
>> understood well enough, and completed to a sufficient level of
>> detail to make it possible in a sensible amount of time, it's
>> pretty much pointless.
> And that's where I disagree. If you can have your new theorem in
> a machine readable/verifiable format, then other theorems can make
> use of it. The idea is not to redo the work every time for a new
> theorem. I understand new math is much more complex, and that's why
> we should be thinking of making this available in a theorem prover.
It's being done now, but the problem is that producing new work, new theorems, is not going to be done within the framework of the automated system, because that's not where the meaning lives. When I produce a new proof, the fastest thing to do is to make it readable by other mathematicians, not convert it painstakingly to a different notation for a machine to check. That can, and really should, only be done once it's understood conceptually by other mathematicians.
There are people working on this, and they are making great strides. I just get really frustrated when people think a) it's obvious that machine checking is the way to go, b) why don't mathematicians all work on producing their proofs in machine checkable form, c) I don't understand these proofs, so obviously machine checking is better, and d) it really can't be that hard - even I can see it's a good idea.
I have no doubt that this will change over the next 50 years, perhaps even over the next 20 years. Prediction is hard, especially about the future, and I'm not going to try. What I do know is that I honestly cannot see how I would work trying to use a machine readable form, or trying to use a proof assistant. So far they've not merely been unhelpful, they've actively stopped me from working at all. No doubt it will be different for people raised with and trained on the "modern" systems of 20 years from now.
> It's certainly a very complex work and maybe not doable today,
> but it would have a big impact.
Yes, yes it would. I don't know how much math you know, there's nothing in your profile, but if you have enough to have a go at contributing to one of the major pieces of work underway to make it happen, you could make your mark.
My math knowledge is certainly not very big, but maybe above average. Probably not enough to work on the state of the art of theorem provers today. Still, a fascinating subject.
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.
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...
> 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.
Argh. Always get proof, conjecture and theorem mixed about. I'm a baby mathematician - literally starting from scratch because I've realised that I missed a lot of concepts at school.
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.