15 ms·

I have a MSc in mathematics so I am by no means an expert in mathematics proofs but I get the gist of it. To me a proof is literally a logical argument that you

I have a MSc in mathematics so I am by no means an expert in mathematics proofs but I get the gist of it. To me a proof is literally a logical argument that you can follow to "believe" that a theorem is true. I do worry how many people actually understand or verify mathematics proofs. How many people have actually read and verified Perelman's or Wiles' proofs (I'm only singling them out because they're famous, not because they're particularly sketchy). We seem to think that once a proof is published in a reputable journal then it is definitely true, but really we should only think "a small number of qualified people have read it and think it is fine". The foundations actually seem a bit shakier to me than people seem to appreciate. Perhaps machine-verified proofs will be the answer one day.

bsder 8y ago
> We seem to think that once a proof is published in a reputable journal then it is definitely true, but really we should only think "a small number of qualified people have read it and think it is fine". The foundations actually seem a bit shakier to me than people seem to appreciate. I think you are understating the certainty of fundamental proofs like this. Once such a fundamental proof is considered "true", it almost always has applications beyond what the original proof was used for. It is often used to try to prove things that we already know are "true" in other ways. So, any "true" proof generally gets tested from multiple directions. Wile's proof is a good example of this. It doesn't just prove Fermat's Last Theorem. Quoting Wikipedia: "Wiles' path to proving Fermat's Last Theorem, by way of proving the modularity theorem for the special case of semistable elliptic curves, established powerful modularity lifting techniques and opened up entire new approaches to numerous other problems."
- Moodles 8y ago
  True, but even then, how large do you think the field is? And how many people verify these proofs? I have a PhD in an esoteric field myself. There's literally <50 people worldwide who write/verify proofs in it. I've spotted errors in my own work or other's work that got past peer review. And I don't think I'm particularly special. There's just not enough eyeballs, time and incentives sometimes.
  - bsder 8y ago
    > True, but even then, how large do you think the field is? And how many people verify these proofs? It only takes one to break it. And, for something so fundamental, it's a big deal if you are the one. This isn't physics, where you have to rule out all manner of confounding data before you can trust your conclusion.
    - fjsolwmv 8y ago
      The point you are missing that studying a proof can't proof it correct, only fail to disprove it.
      - bsder 8y ago
        That's incorrect. For example, given the axioms of Euclidean geometry, I can prove that the sum of the angles of a triangle add up to 180 degrees. That statement is true. Full stop. Now the starting axioms may not be correct (the parallel postulate, for example, is not required to be true). However, given the starting axioms, proofs are true. Period. In addition, there will be things in mathematics that you cannot prove--Godel's Incompleteness Theorem sits in this section. And, science has the problem that a hypothesis can only be disproven. Mathematics does not suffer from the same issue, though.
doitLP 8y ago
> We seem to think that once a proof is published in a reputable journal then it is definitely true, but really we should only think "a small number of qualified people have read it and think it is fine" This same could be said of many other professions, medicine and psychology to start. It seems a related manifestation of the Gells-Mann Amnesia.
- Moodles 8y ago
  Yup, not picking on mathematics at all :-)
- ericsoderstrom 8y ago
  Math is different in that one feels there should be something close to "absolute truth." That is, given a set of axioms, it is possible to verify with complete certainty whether a proof follows from those axioms or not. Though when proofs become so long and abstruse that only a handful of people can even read them, perhaps that's no longer true. In other fields, it's more clear that nothing is known with 100% certainty. That differences of opinion or experimental error could always lead to uncertainty.
  - atmanthedog 8y ago
    Unfortunately, math doesn't really permit this type of truth: if your axioms are strong enough to prove general statements about arithmetic, there is no effective procedure to determine whether an arbitrary proof follows from those axioms.
    - rocqua 8y ago
      Still, given a set of axioms, statements will fall into one of three categories. 1) Provably True, 2) Provably False, 3) Undecideable Claims that a statement is in category 1 are fully verifiable (by providing the proof). The same goes with claims that a statement is in category 2.
    - smadge 8y ago
      Did you mean to write “there is no effective procedure to determine whether an arbitrary formula follows from those axioms?” A proof is exactly how we demonstrate that a formula follows from the axioms.
salty_biscuits 8y ago
The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.
- vbezhenar 8y ago
  I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that proof.
  - _Microft 8y ago
    Some mathematicians are concerned that the possibility of an error in a computer program or a run-time error in its calculations calls the validity of such computer-assisted proofs into question. (This might be one reason, from https://en.wikipedia.org/wiki/Mathematical_proof#Computer-assisted_proofs https://en.wikipedia.org/wiki/Mathematical_proof#Computer-as... )
    - fjsolwmv 8y ago
      That's silly, because humans have been repeatedly proven to be full of errors.
  - salty_biscuits 8y ago
    It is actually surprisingly fussy to set up a formal proof for anything complex enough to be interesting to a mathematician (for computer assisted verification). People take big leaps that are often quite awful to actually prove. I think you are right though, this area will definitely be very important and make big strides.
  - deleted 8y ago
    [deleted]
Jach 8y ago
How to Write a 21st Century Proof: https://lamport.azurewebsites.net/pubs/proof.pdf https://lamport.azurewebsites.net/pubs/proof.pdf From page 6 with figure 1, to page 10 with figure 3, it's clear that even just changing to structured proofs over prose proofs can be helpful in catching errors. Of course the rest of the paper goes into detail about going even further... I don't know if Lamport's ideas have gained any more acceptance in the mathematics communities, but I'm doubtful. At least if memory serves the ABC papers were classic prose-style...
- codethief 8y ago
  Here's a video of an excellent presentation Lamport gave on "21st-century proofs" last year: https://www.heidelberg-laureate-forum.org/blog/video/lecture-tuesday-september-26-2017-leslie-lamport/ https://www.heidelberg-laureate-forum.org/blog/video/lecture...
jackfoxy 8y ago
Wasn't this very issue what inspired Voevodsky to work on a Univalent foundations of mathematics, resulting in the HoTT Book (in collaboration with others)?
barbecue_sauce 8y ago
You have an MSc in mathematics but don't consider yourself an expert?
- dagw 8y ago
  I've also got an MSc in mathematics, I and feel that that was barely enough time to just start scratching the surface.
- pmiller2 8y ago
  Trust me, an MS in math doesn't even get you to the fun part. :)
- deleted 8y ago
  [deleted]
- Moodles 8y ago
  Haha not at all. My MSc project was about splitting graphs into other types of graphs and some generalizations of graphs into hypergraphs. I don't even consider myself an expert on graphs, let alone number theory.
- Smaug123 8y ago
  Where high-school mathematics was analogous to learning to form letters with a pencil, undergraduate BSc mathematics is analogous to learning to form words and short sentences. By the end of your BSc in the analogy, you can look at a sentence and recognise at least what sort of genre it might be part of, and you can write down many of the most common words as well as a number of rehearsed useful sentences. An MSc is like reading some examples of long sentences and short paragraphs, and being shown some long paragraphs or even chapters of books (which you have no hope of understanding, but you try, and the experience is salutary). If you're lucky, you did a research project in which you perhaps rewrote a certain very specific short paragraph in your own words. The job of a research mathematician is analogously then to read and write books.
  - tandr 8y ago
    This is beautiful. Thank you.
man-and-laptop 8y ago
Lamport suggests hierarchical proofs as a possible remedy. They're somewhere in between computer verification and the current prevalent style. Lamport acknowledges it would make writing proofs harder, while reading them easier. The style doesn't help to communicate the intuition behind a proof particularly well; it's more useful for verification. Mochizuki, for one, would have to work harder to write his proof (?) in that style.
- thanatropism 8y ago
  I once tried proving the very first theorem in Cannas da Silva's book of symplectic geometry in this style. Screw that. The proof that I eventually used in my dissertation is even wordier and with less display-mode equations than the one in the book (I became very influenced by the prose in old topology books). Most of the time, the point of proofs isn't to establish something is true, but to communicate something about the internal structure of a piece of mathematics. The problem with Mochizuki is that he did his work isolated from the rest of the world, so the internal structure of the kind of maths he invented is opaque. Accordingly, what mathematicians are really trying to do is to examine what makes this new maths tick; the books that make this accessible to mathematicians worldwide will not be fully-verifiable proofs of a statement, but webs of separate propositions whose statements are illuminating and whose proofs are easy to understand. If they're really successful, some may even be left as an exercise to the reader.
  - jedharris 8y ago
    If you are right then calling them "proofs" is misleading. The results aren't proven, just made convincing. So I guess they are "arguments" -- only detailed enough to convince others who already know enough about the entities being discussed. Automated proofs by contrast really are proofs but as many of these comments show are not arguments. So maybe the problem to be solved is to appropriately connect mathematical arguments (what mathematicians call proofs) to proofs, while recognizing that they are actually two entirely separate families -- as different as plants and animals.
    - 8y ago
konschubert 8y ago
I just have a Master in Physics, but here is my take: The thing is that mathematic proofs work on different levels of "zoom", ranging from just stating "it follows trivially" to formal proofs. And this is a normal process, that's how Mathematicians boil down long proofs to simple lines of reasoning. I think what happens here I that the author of the original proof is arguing on a high "it's obvious" level and seems to be unwilling to go into detail.
nutanc 8y ago
Agree with this. Don't think there are too many mathematicians who can really argue for or against a really important theorem. My prof has come up with one for Riemann hypothesis[1], but he is not finding anyone willing to engage in a discussion. Most mathematicians seem to believe that the Riemann hypothesis is unsolvable and I don't think it helps that my prof is currently not associated with any reputable university. It's as if proofs can come from only reputable universities and reputable mathematicians. [1]https://medium.com/@nutanc/the-final-and-exhaustive-proof-of-the-riemann-hypothesis-from-first-principles-348ead3cd2a4 https://medium.com/@nutanc/the-final-and-exhaustive-proof-of...
- nerdponx 8y ago
  It appears your professor's work has gotten the attention of at least one other researcher -- a Matthew Watkin at the University of Exeter. He seems to believe that it can be disproven by a student of analytic number theory [0]. [0]: https://empslocal.ex.ac.uk/people/staff/mrwatkin//zeta/RHproofs.htm https://empslocal.ex.ac.uk/people/staff/mrwatkin//zeta/RHpro...
- masterjack 8y ago
  Unfortunately way more often than not attempted proofs of hard problems end up flawed, especially if there are certain warning signs: https://www.scottaaronson.com/blog/?p=304 https://www.scottaaronson.com/blog/?p=304 That said, I’d be happy to go over this as an analytic number theorist rfurman@alumni.stanford.edu
  - nutanc 8y ago
    Thanks. Will share the details with my prof.
deleted 8y ago
[deleted]
msmith10101 8y ago
\
- striking 8y ago
  I don't see the parent poster making any claims about the straightforwardness of proving worthwhile things.
  - deleted 8y ago
    [deleted]
- gnulinux 8y ago
  This is such a shallow comment, very surprising its up there. (Did I miss a joke?) Mathematics is written in a language that is not only precise enough to make it easier to follow logical arguments, but also optimized for human readability. Mysql is written in C, which is optimized in the early days of computing for portability between machines, which is an irrelevant goal to provability. C does not give enough guarantees to prove anything worthwhile, whereas the language of mathematics has been evolving since the 19th century to give as much guarantees as possible. If mysql would be written in agda, it'd be so much more easier to prove it compared to Wiles' proof of Fermat's or whatever. As far as any programming language go, C is probably the worst language you can prove anything let alone mysql. OP comment wasn't implying proving is supposed to be easy. Mathematics is not written for machines, it's written for humans. Ultimately, the act of writing mathematical papers is not that much different than act of writing sociology papers. A mathematical proof is written so that it convinces a human. Once you start writing those proofs into Coq or agda or whatever, you start seeing how much handwaving is going in mathematics. This is because being experienced in mathematics gives one the ability and confidence to operate on higher levels of abstraction which doesn't need as much precision/rigor as a programming language as context signals the tactic, argument etc...
  - just123cation 8y ago
    Ugh, you are an idiot. I feel sorry for your friends, assuming you have any (which is a stretch bet, to be sure). You have totally missed the point. This had nothing to do with the C programming language you moronic twit.
n_t 8y ago
Usually grad level courses were about reading research papers. And many times the exercise is to read the paper, try to predict what next para or page will be about and even try to find faults, even though there might be none. I assume Math department does the same.
jamesrcole 8y ago
The term "proof" seems to be a lot of the problem, because it implies something definitive.
- jedharris 8y ago
  Excellent point. What mathematicians write to each other are arguments not proofs. Machine checkable proofs are really proofs. This should not be embarrassing to mathematicians. It opens up potential for a lot of progress in several directions. Arguments can become better ways to communicate with humans. Proofs can be developed where needed to resolve questions about arguments. The relationships between arguments and proofs can be improved. Tools for each can be developed without having to support both.
  - m00n 8y ago
    What is the philosophical difference between an 'argument' that human minds following the laws of logic agree on "is correct" and a machine built by these minds flashing a "correct light"? IMO the only advantage to be gained by introducing physical computers in the picture is lightning-fast book keeping. Why would you trust an Intel CPU, a Samsung SSD and a linux fs driver running some verifying framework more than the human brains designing, writing and executing said framework?
mikorym 8y ago
There is an alternative way (but not a replacement) to go about it as well. Rather than reverifying proofs (I mean now ones that have been proved in the literature) one could study central features. And whenever a feature breaks, then one can stop to think whether the theorems themselves hold water or not.
Fri21Sep 8y ago
The most definitive version of a proof one can imagine is when the proof has been expressed via a formal language and a proof assistant checks that each step of the proof complies with axioms or already proven theorems from a library (which, in this case, are simple rewrite rules in the formal grammar). The [Mizar System](https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system) is an example of that. The question of formally proving Wiles' theorem is [discussed here](http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html). Currently there exists no tool powerful enough to formalize such proof. It's considered a challenging problem in computer science.
m00n 8y ago
To take one of your examples that I happen to be familiar with: Wiles' proof of FLT. I can assure you that in the >20 years that this proof has been out, thousands of professors, postdocs and grad students have read and reread every line of the two Annals papers. They have been the foundation of hundreds of Phd projects and the scientific merit and public fame to be gained by finding a gap in the argument is clear. Actually I think breakthrough papers are least problematic when it comes to unverified claims in math.
rofo1 8y ago
Here's another "not sure if correct proof": Jordan's theorem! Seemingly "evident" result, extremely difficult to prove in some cases (e.g. continuous, nowhere differentiable function etc.)

bsder 8y ago

> We seem to think that once a proof is published in a reputable journal then it is definitely true, but really we should only think "a small number of qualified people have read it and think it is fine". The foundations actually seem a bit shakier to me than people seem to appreciate. I think you are understating the certainty of fundamental proofs like this. Once such a fundamental proof is considered "true", it almost always has applications beyond what the original proof was used for. It is often used to try to prove things that we already know are "true" in other ways. So, any "true" proof generally gets tested from multiple directions. Wile's proof is a good example of this. It doesn't just prove Fermat's Last Theorem. Quoting Wikipedia: "Wiles' path to proving Fermat's Last Theorem, by way of proving the modularity theorem for the special case of semistable elliptic curves, established powerful modularity lifting techniques and opened up entire new approaches to numerous other problems."

Moodles 8y ago
True, but even then, how large do you think the field is? And how many people verify these proofs? I have a PhD in an esoteric field myself. There's literally <50 people worldwide who write/verify proofs in it. I've spotted errors in my own work or other's work that got past peer review. And I don't think I'm particularly special. There's just not enough eyeballs, time and incentives sometimes.
- bsder 8y ago
  > True, but even then, how large do you think the field is? And how many people verify these proofs? It only takes one to break it. And, for something so fundamental, it's a big deal if you are the one. This isn't physics, where you have to rule out all manner of confounding data before you can trust your conclusion.
  - fjsolwmv 8y ago
    The point you are missing that studying a proof can't proof it correct, only fail to disprove it.
    - bsder 8y ago
      That's incorrect. For example, given the axioms of Euclidean geometry, I can prove that the sum of the angles of a triangle add up to 180 degrees. That statement is true. Full stop. Now the starting axioms may not be correct (the parallel postulate, for example, is not required to be true). However, given the starting axioms, proofs are true. Period. In addition, there will be things in mathematics that you cannot prove--Godel's Incompleteness Theorem sits in this section. And, science has the problem that a hypothesis can only be disproven. Mathematics does not suffer from the same issue, though.

doitLP 8y ago

> We seem to think that once a proof is published in a reputable journal then it is definitely true, but really we should only think "a small number of qualified people have read it and think it is fine" This same could be said of many other professions, medicine and psychology to start. It seems a related manifestation of the Gells-Mann Amnesia.

Moodles 8y ago
Yup, not picking on mathematics at all :-)
ericsoderstrom 8y ago
Math is different in that one feels there should be something close to "absolute truth." That is, given a set of axioms, it is possible to verify with complete certainty whether a proof follows from those axioms or not. Though when proofs become so long and abstruse that only a handful of people can even read them, perhaps that's no longer true. In other fields, it's more clear that nothing is known with 100% certainty. That differences of opinion or experimental error could always lead to uncertainty.
- atmanthedog 8y ago
  Unfortunately, math doesn't really permit this type of truth: if your axioms are strong enough to prove general statements about arithmetic, there is no effective procedure to determine whether an arbitrary proof follows from those axioms.
  - rocqua 8y ago
    Still, given a set of axioms, statements will fall into one of three categories. 1) Provably True, 2) Provably False, 3) Undecideable Claims that a statement is in category 1 are fully verifiable (by providing the proof). The same goes with claims that a statement is in category 2.
  - smadge 8y ago
    Did you mean to write “there is no effective procedure to determine whether an arbitrary formula follows from those axioms?” A proof is exactly how we demonstrate that a formula follows from the axioms.

salty_biscuits 8y ago

The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.

vbezhenar 8y ago
I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that proof.
- _Microft 8y ago
  Some mathematicians are concerned that the possibility of an error in a computer program or a run-time error in its calculations calls the validity of such computer-assisted proofs into question. (This might be one reason, from https://en.wikipedia.org/wiki/Mathematical_proof#Computer-assisted_proofs https://en.wikipedia.org/wiki/Mathematical_proof#Computer-as... )
  - fjsolwmv 8y ago
    That's silly, because humans have been repeatedly proven to be full of errors.
- salty_biscuits 8y ago
  It is actually surprisingly fussy to set up a formal proof for anything complex enough to be interesting to a mathematician (for computer assisted verification). People take big leaps that are often quite awful to actually prove. I think you are right though, this area will definitely be very important and make big strides.
- deleted 8y ago
  [deleted]

Jach 8y ago

How to Write a 21st Century Proof: https://lamport.azurewebsites.net/pubs/proof.pdf https://lamport.azurewebsites.net/pubs/proof.pdf From page 6 with figure 1, to page 10 with figure 3, it's clear that even just changing to structured proofs over prose proofs can be helpful in catching errors. Of course the rest of the paper goes into detail about going even further... I don't know if Lamport's ideas have gained any more acceptance in the mathematics communities, but I'm doubtful. At least if memory serves the ABC papers were classic prose-style...

codethief 8y ago
Here's a video of an excellent presentation Lamport gave on "21st-century proofs" last year: https://www.heidelberg-laureate-forum.org/blog/video/lecture-tuesday-september-26-2017-leslie-lamport/ https://www.heidelberg-laureate-forum.org/blog/video/lecture...

jackfoxy 8y ago

Wasn't this very issue what inspired Voevodsky to work on a Univalent foundations of mathematics, resulting in the HoTT Book (in collaboration with others)?

barbecue_sauce 8y ago

You have an MSc in mathematics but don't consider yourself an expert?

dagw 8y ago
I've also got an MSc in mathematics, I and feel that that was barely enough time to just start scratching the surface.
pmiller2 8y ago
Trust me, an MS in math doesn't even get you to the fun part. :)
deleted 8y ago
[deleted]
Moodles 8y ago
Haha not at all. My MSc project was about splitting graphs into other types of graphs and some generalizations of graphs into hypergraphs. I don't even consider myself an expert on graphs, let alone number theory.
Smaug123 8y ago
Where high-school mathematics was analogous to learning to form letters with a pencil, undergraduate BSc mathematics is analogous to learning to form words and short sentences. By the end of your BSc in the analogy, you can look at a sentence and recognise at least what sort of genre it might be part of, and you can write down many of the most common words as well as a number of rehearsed useful sentences. An MSc is like reading some examples of long sentences and short paragraphs, and being shown some long paragraphs or even chapters of books (which you have no hope of understanding, but you try, and the experience is salutary). If you're lucky, you did a research project in which you perhaps rewrote a certain very specific short paragraph in your own words. The job of a research mathematician is analogously then to read and write books.
- tandr 8y ago
  This is beautiful. Thank you.

man-and-laptop 8y ago

Lamport suggests hierarchical proofs as a possible remedy. They're somewhere in between computer verification and the current prevalent style. Lamport acknowledges it would make writing proofs harder, while reading them easier. The style doesn't help to communicate the intuition behind a proof particularly well; it's more useful for verification. Mochizuki, for one, would have to work harder to write his proof (?) in that style.

thanatropism 8y ago
I once tried proving the very first theorem in Cannas da Silva's book of symplectic geometry in this style. Screw that. The proof that I eventually used in my dissertation is even wordier and with less display-mode equations than the one in the book (I became very influenced by the prose in old topology books). Most of the time, the point of proofs isn't to establish something is true, but to communicate something about the internal structure of a piece of mathematics. The problem with Mochizuki is that he did his work isolated from the rest of the world, so the internal structure of the kind of maths he invented is opaque. Accordingly, what mathematicians are really trying to do is to examine what makes this new maths tick; the books that make this accessible to mathematicians worldwide will not be fully-verifiable proofs of a statement, but webs of separate propositions whose statements are illuminating and whose proofs are easy to understand. If they're really successful, some may even be left as an exercise to the reader.
- jedharris 8y ago
  If you are right then calling them "proofs" is misleading. The results aren't proven, just made convincing. So I guess they are "arguments" -- only detailed enough to convince others who already know enough about the entities being discussed. Automated proofs by contrast really are proofs but as many of these comments show are not arguments. So maybe the problem to be solved is to appropriately connect mathematical arguments (what mathematicians call proofs) to proofs, while recognizing that they are actually two entirely separate families -- as different as plants and animals.
  - 8y ago

konschubert 8y ago

I just have a Master in Physics, but here is my take: The thing is that mathematic proofs work on different levels of "zoom", ranging from just stating "it follows trivially" to formal proofs. And this is a normal process, that's how Mathematicians boil down long proofs to simple lines of reasoning. I think what happens here I that the author of the original proof is arguing on a high "it's obvious" level and seems to be unwilling to go into detail.

nutanc 8y ago

Agree with this. Don't think there are too many mathematicians who can really argue for or against a really important theorem. My prof has come up with one for Riemann hypothesis[1], but he is not finding anyone willing to engage in a discussion. Most mathematicians seem to believe that the Riemann hypothesis is unsolvable and I don't think it helps that my prof is currently not associated with any reputable university. It's as if proofs can come from only reputable universities and reputable mathematicians. [1]https://medium.com/@nutanc/the-final-and-exhaustive-proof-of-the-riemann-hypothesis-from-first-principles-348ead3cd2a4 https://medium.com/@nutanc/the-final-and-exhaustive-proof-of...

nerdponx 8y ago
It appears your professor's work has gotten the attention of at least one other researcher -- a Matthew Watkin at the University of Exeter. He seems to believe that it can be disproven by a student of analytic number theory [0]. [0]: https://empslocal.ex.ac.uk/people/staff/mrwatkin//zeta/RHproofs.htm https://empslocal.ex.ac.uk/people/staff/mrwatkin//zeta/RHpro...
masterjack 8y ago
Unfortunately way more often than not attempted proofs of hard problems end up flawed, especially if there are certain warning signs: https://www.scottaaronson.com/blog/?p=304 https://www.scottaaronson.com/blog/?p=304 That said, I’d be happy to go over this as an analytic number theorist rfurman@alumni.stanford.edu
- nutanc 8y ago
  Thanks. Will share the details with my prof.

deleted 8y ago

[deleted]

msmith10101 8y ago

striking 8y ago
I don't see the parent poster making any claims about the straightforwardness of proving worthwhile things.
- deleted 8y ago
  [deleted]
gnulinux 8y ago
This is such a shallow comment, very surprising its up there. (Did I miss a joke?) Mathematics is written in a language that is not only precise enough to make it easier to follow logical arguments, but also optimized for human readability. Mysql is written in C, which is optimized in the early days of computing for portability between machines, which is an irrelevant goal to provability. C does not give enough guarantees to prove anything worthwhile, whereas the language of mathematics has been evolving since the 19th century to give as much guarantees as possible. If mysql would be written in agda, it'd be so much more easier to prove it compared to Wiles' proof of Fermat's or whatever. As far as any programming language go, C is probably the worst language you can prove anything let alone mysql. OP comment wasn't implying proving is supposed to be easy. Mathematics is not written for machines, it's written for humans. Ultimately, the act of writing mathematical papers is not that much different than act of writing sociology papers. A mathematical proof is written so that it convinces a human. Once you start writing those proofs into Coq or agda or whatever, you start seeing how much handwaving is going in mathematics. This is because being experienced in mathematics gives one the ability and confidence to operate on higher levels of abstraction which doesn't need as much precision/rigor as a programming language as context signals the tactic, argument etc...
- just123cation 8y ago
  Ugh, you are an idiot. I feel sorry for your friends, assuming you have any (which is a stretch bet, to be sure). You have totally missed the point. This had nothing to do with the C programming language you moronic twit.

n_t 8y ago

Usually grad level courses were about reading research papers. And many times the exercise is to read the paper, try to predict what next para or page will be about and even try to find faults, even though there might be none. I assume Math department does the same.

jamesrcole 8y ago

The term "proof" seems to be a lot of the problem, because it implies something definitive.

jedharris 8y ago
Excellent point. What mathematicians write to each other are arguments not proofs. Machine checkable proofs are really proofs. This should not be embarrassing to mathematicians. It opens up potential for a lot of progress in several directions. Arguments can become better ways to communicate with humans. Proofs can be developed where needed to resolve questions about arguments. The relationships between arguments and proofs can be improved. Tools for each can be developed without having to support both.
- m00n 8y ago
  What is the philosophical difference between an 'argument' that human minds following the laws of logic agree on "is correct" and a machine built by these minds flashing a "correct light"? IMO the only advantage to be gained by introducing physical computers in the picture is lightning-fast book keeping. Why would you trust an Intel CPU, a Samsung SSD and a linux fs driver running some verifying framework more than the human brains designing, writing and executing said framework?

mikorym 8y ago

There is an alternative way (but not a replacement) to go about it as well. Rather than reverifying proofs (I mean now ones that have been proved in the literature) one could study central features. And whenever a feature breaks, then one can stop to think whether the theorems themselves hold water or not.

Fri21Sep 8y ago

The most definitive version of a proof one can imagine is when the proof has been expressed via a formal language and a proof assistant checks that each step of the proof complies with axioms or already proven theorems from a library (which, in this case, are simple rewrite rules in the formal grammar). The [Mizar System](https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system) is an example of that. The question of formally proving Wiles' theorem is [discussed here](http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html). Currently there exists no tool powerful enough to formalize such proof. It's considered a challenging problem in computer science.

m00n 8y ago

To take one of your examples that I happen to be familiar with: Wiles' proof of FLT. I can assure you that in the >20 years that this proof has been out, thousands of professors, postdocs and grad students have read and reread every line of the two Annals papers. They have been the foundation of hundreds of Phd projects and the scientific merit and public fame to be gained by finding a gap in the argument is clear. Actually I think breakthrough papers are least problematic when it comes to unverified claims in math.

rofo1 8y ago

Here's another "not sure if correct proof": Jordan's theorem! Seemingly "evident" result, extremely difficult to prove in some cases (e.g. continuous, nowhere differentiable function etc.)