4 ms·

[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

[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
      blah blah blah type checkers blah blah blah can be run on different chipsets / OS's blah blah blah computers are several orders of magnitude more accurate blah blah blah not really the issue.
pfortuny 6y ago
Oh, many thanks for this explanation. Even more interesting. Yes, Voedovsky’s abd Scholze’s candidness is encouraging and liberating. And a great call to responsibility for us reviewers. And thanks for your work on formalization. Truly important in my view.
- Ericson2314 6y ago
  I feel like with 2 fields medalists on boards, the culture can finally shift. I'm really excited. [It's not just about math, see https://hapgood.us/2015/10/17/the-garden-and-the-stream-a-technopastoral/ https://hapgood.us/2015/10/17/the-garden-and-the-stream-a-te... for a great explanation of the type of labor that is mathlib is sorely lacking in just about every sector. I'm really hoping that mathematics can lead the way here.]

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
    blah blah blah type checkers blah blah blah can be run on different chipsets / OS's blah blah blah computers are several orders of magnitude more accurate blah blah blah not really the issue.

pfortuny 6y ago

Oh, many thanks for this explanation. Even more interesting. Yes, Voedovsky’s abd Scholze’s candidness is encouraging and liberating. And a great call to responsibility for us reviewers. And thanks for your work on formalization. Truly important in my view.

Ericson2314 6y ago
I feel like with 2 fields medalists on boards, the culture can finally shift. I'm really excited. [It's not just about math, see https://hapgood.us/2015/10/17/the-garden-and-the-stream-a-technopastoral/ https://hapgood.us/2015/10/17/the-garden-and-the-stream-a-te... for a great explanation of the type of labor that is mathlib is sorely lacking in just about every sector. I'm really hoping that mathematics can lead the way here.]