4 ms·

This paragraph is paramount, coming from one of the youngest Fields Medalists and a truly trusted source. Truly honest and inspiring. “ I have occasionally bee

This paragraph is paramount, coming from one of the youngest Fields Medalists and a truly trusted source. Truly honest and inspiring. “ I have occasionally been able to be very persuasive even with wrong arguments. (Fun fact: In the selection exams for the international math olympiad, twice I got full points for a wrong solution. Later, I once had a full proof of the weight-monodromy conjecture that passed the judgment of some top mathematicians, but then it turned out to contain a fatal mistake.)”

kevinbuzzard 6y ago
[just to be clear here, I am the author of the Xena project blog and my current research is in formalising number theory; before formalisation I was working in Scholze's area.] Scholze's first application of the theory of perfectoid spaces was to prove weight-monodromy in many new cases (but not in all cases) -- this was his first breakthrough result really. Fun fact: in the first version of the post which he sent me, this weight-monodromy confession was not there. He then slept on it and sent a second version a day later, and it was only when I was converting the LaTeX into Wordpress format that I noticed that he had added this extra line. I quite agree that it is very rare for people, especially of his stature, to publically admit to errors, especially ones which never made it into print. Of course we will be working on this challenge in Lean, and we are currently optimistic, but who knows. It is certainly true that in the study group we had on the work at Imperial earlier this year, we did not work through the technical proof which Scholze is now challenging the formalization community to check. This is really Scholze's point I guess: once you have a Fields Medal it's very easy for other people to say "well this is a bit technical but let's face it, it's probably fine" (this is exactly what we did, for example). Voevodsky made similar comments around a decade ago -- and he managed to get false arguments published, perhaps partly because of his own Fields Medal. Scholze is flagging an explicit argument in his work which he believes needs to be carefully analysed, and I have seen with my own eyes that the academic system we have right now might not actually do it carefully enough. What is not at all clear, right now at least, is whether computer proof verification systems are up to the task. I think it will be interesting to see how this develops.
- throwaway_pdp09 6y ago
  When you get to the symbols, all becomes symbol manipulation, so why would computer proof verification systems not be up to the task?
  - tromoi57 6y ago
    Well, climbing Mt. Everest is also "just moving your arms and legs". But I'm not up to that task! It's certainly possible in principle, but whether it's possible in practice is part of the challenge. You need enough people that understand the details of the proof, and know how to turn that into a formally verified proof. Such proofs can also become slow, so to keep things practical, you also need to take speed into account.
    - Ericson2314 6y ago
      "Quantity has a quality all its own" Also, and perhaps easier to wrap one's head around, is issues of tooling. Already, there is a very heavy use of "tactics" (metaprograms, and ones with decent computational complexity (think "search" not just "expansion")). Mathematicians write lemmas so we can try to run the tactics on "mini problems" that do not grow even as the total body of work grows, but there's always a risk the that there's some sticking point one cannot break down enough.
  - pfortuny 6y ago
    Remember Pentium’s division bug (on mobile so cannot cooy-paste). We need some king of certificate of proof, not just some black-box which answers “OK”, “NOT-OK”.
    - Ericson2314 6y ago
      The theorem proves that are discussed here already do that.
      - kevinbuzzard 6y ago
cperciva 6y ago
To add another data point: I submitted a paper to a major mathematics journal which had a mistake in a proof. One of the referees flagged that I was making a claim without proving it, and asked for me to revise it. I submitted a revised version which still had a mistake in the same step and it was accepted. (Three years later, my doctoral supervisor pointed out the mistake to me, and we published another paper -- in the same journal -- filling the gap.)

kevinbuzzard 6y ago

[just to be clear here, I am the author of the Xena project blog and my current research is in formalising number theory; before formalisation I was working in Scholze's area.] Scholze's first application of the theory of perfectoid spaces was to prove weight-monodromy in many new cases (but not in all cases) -- this was his first breakthrough result really. Fun fact: in the first version of the post which he sent me, this weight-monodromy confession was not there. He then slept on it and sent a second version a day later, and it was only when I was converting the LaTeX into Wordpress format that I noticed that he had added this extra line. I quite agree that it is very rare for people, especially of his stature, to publically admit to errors, especially ones which never made it into print. Of course we will be working on this challenge in Lean, and we are currently optimistic, but who knows. It is certainly true that in the study group we had on the work at Imperial earlier this year, we did not work through the technical proof which Scholze is now challenging the formalization community to check. This is really Scholze's point I guess: once you have a Fields Medal it's very easy for other people to say "well this is a bit technical but let's face it, it's probably fine" (this is exactly what we did, for example). Voevodsky made similar comments around a decade ago -- and he managed to get false arguments published, perhaps partly because of his own Fields Medal. Scholze is flagging an explicit argument in his work which he believes needs to be carefully analysed, and I have seen with my own eyes that the academic system we have right now might not actually do it carefully enough. What is not at all clear, right now at least, is whether computer proof verification systems are up to the task. I think it will be interesting to see how this develops.

throwaway_pdp09 6y ago
When you get to the symbols, all becomes symbol manipulation, so why would computer proof verification systems not be up to the task?
- tromoi57 6y ago
  Well, climbing Mt. Everest is also "just moving your arms and legs". But I'm not up to that task! It's certainly possible in principle, but whether it's possible in practice is part of the challenge. You need enough people that understand the details of the proof, and know how to turn that into a formally verified proof. Such proofs can also become slow, so to keep things practical, you also need to take speed into account.
  - Ericson2314 6y ago
    "Quantity has a quality all its own" Also, and perhaps easier to wrap one's head around, is issues of tooling. Already, there is a very heavy use of "tactics" (metaprograms, and ones with decent computational complexity (think "search" not just "expansion")). Mathematicians write lemmas so we can try to run the tactics on "mini problems" that do not grow even as the total body of work grows, but there's always a risk the that there's some sticking point one cannot break down enough.
- pfortuny 6y ago
  Remember Pentium’s division bug (on mobile so cannot cooy-paste). We need some king of certificate of proof, not just some black-box which answers “OK”, “NOT-OK”.
  - Ericson2314 6y ago
    The theorem proves that are discussed here already do that.
    - kevinbuzzard 6y ago

cperciva 6y ago

To add another data point: I submitted a paper to a major mathematics journal which had a mistake in a proof. One of the referees flagged that I was making a claim without proving it, and asked for me to revise it. I submitted a revised version which still had a mistake in the same step and it was accepted. (Three years later, my doctoral supervisor pointed out the mistake to me, and we published another paper -- in the same journal -- filling the gap.)