21–30 of 275 posts
> Definitions went on for pages, followed by theorems whose statements were similarly long, but whose proofs only said, essentially, “this follows immediately from the definitions.”
This sounds perfect for machine checked proofs, but I guess the proofs are actually a lot more involved than they are presented.
Earlier quoted context omitted.
> 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 al…
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.
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.
https://galoisrepresentations.wordpress.com/2017/12/17/the-a... Terence Tao and Peter Scholze (and others) join the discussion in the comments section.
Tao's commentary is especially interesting for me as a non-mathematician: >It seems bizarre to me that there would be an entire self-contained theory whose only external application is to prove the abc conjecture after 300+ pages of set up, with no smaller fragment of this setup having any non-trivial external consequence whatsoever. Likely such is the understatement-ish way of a mathematician to say "This is clearly…
Apart from that, the article makes me curious about the state of automated mathematical proof. I remember having read an article posted here about a mathematician (I think he was a Field medalist) who was claiming that automated proof were the future of mathematics as they would enable mathematicians to collaborate much more easily, removing problems of trust in others' proof.
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 be…
This same could be said of many other professions, medicine and psychology to start. It seems a related manifestation of the Gells-Mann Amnesia.
Mathematicians should do more computer verifiable proofs to avoid discussions like this. > Definitions went on for pages, followed by theorems whose statements were similarly long, but whose proofs only said, essentially, “this follows immediately from the definitions.” This sounds perfect for machine checked proofs, but I guess the proofs are actually a lot more involved than they are presented.
>One final point: I get very annoyed by all references to computer-verification (that came up not on this blog, but elsewhere on the internet in discussions of Mochizuki’s work). The computer will not be able to make sense of this step either. The comparison to the Kepler conjecture, say, is entirely misguided: In that case, the general strategy was clear, but it was unclear whether every single case had been taken care of. Here, there is no case at all, just the claim “And now the result follows”.
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 be…
https://galoisrepresentations.wordpress.com/2017/12/17/the-a... Terence Tao and Peter Scholze (and others) join the discussion in the comments section.
Tao's commentary is especially interesting for me as a non-mathematician: >It seems bizarre to me that there would be an entire self-contained theory whose only external application is to prove the abc conjecture after 300+ pages of set up, with no smaller fragment of this setup having any non-trivial external consequence whatsoever. Likely such is the understatement-ish way of a mathematician to say "This is clearly…
This is a statement of "If this thing has no other application, it isn't worth my time to dig through what is likely an impenetrable pile of garbage."
Basically, proof of the abc conjecture should have a bunch of follow on consequences. If those aren't materializing, that makes taking the time to understand the proof quite a bit less enticing (ie. the Bayesian prior on "true" goes down a lot).
Earlier quoted context omitted.
Tao's commentary is especially interesting for me as a non-mathematician: >It seems bizarre to me that there would be an entire self-contained theory whose only external application is to prove the abc conjecture after 300+ pages of set up, with no smaller fragment of this setup having any non-trivial external consequence whatsoever. Likely such is the understatement-ish way of a mathematician to say "This is clearly…
I think it might be more akin to a programmer complaining about a monolithic/black-box chunk of code that can't easily be split into understandable and/or unit-testable functions.
I wonder if language is a factor in this at all? I know mathematics is written entirely in English but most likely discussions still happen in local languages. Could part of the proof be lost in translation?