6 ms·

A mathematical formalisation challenge by Peter Scholze

75 points by alimw 6y ago

berndi 6y ago
I just hope NeuraLink pans out so I have a chance of understanding any of this in this life
- soVeryTired 6y ago
  I'm not a mathematician and I'm generally unqualified to comment on any of this but I'll have a stab anyway. The TLDR is that Peter Scholze, one of modern mathematics' most accomplished theory builders, has a concept called a 'condensed set' that he thinks can act as a drop-in replacement for topological spaces in most of mathematics. Topological spaces are perhaps one of the least restrictive models of 'space' is in mathematics. Peter thinks his definition will allow mathematicians to bring algebraic techniques to bear on problems that were previously not amenable to such methods. The problem is that everything rests on one theorem, whose proof is difficult. Because the proof is so foundational, he'd like to get it checked by computer instead of relying on the opinion of a handful of mathematicians, who may be sloppy in their checking.
- deleted 6y ago
  [deleted]
robinhouston 6y ago
The mathematics being discussed here is very new, as well as very technical, and I would guess the number of people who really understand it at the moment is at most dozens; certainly fewer than hundreds. I am certainly not one of those people. Nevertheless, I find this enormously exciting. Formalisation of mathematics has long been the preserve of a handful of logicians and type theorists. What we’re seeing here is one of the world’s leading mathematicians, whose work is situated squarely at the centre of what is today considered mainstream mathematics, advocating the importance of formalisation. If, like me, you believe that formalisation will be an essential part of the mathematics of the future, this is a very encouraging development.
pfortuny 6y ago
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
AcademicHamster 6y ago
What are good beginner resources to learn Lean?
- tromoi57 6y ago
  See the resources over at https://leanprover-community.github.io/learn.html https://leanprover-community.github.io/learn.html and the youtube playlist of the Lean for the Curious Mathematician workshop: https://www.youtube.com/playlist?list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N https://www.youtube.com/playlist?list=PLlF-CfQhukNlxexiNJErG...
- ocfnash 6y ago
  The Lean Community website [1] is a great place to start. Depending on your background you might like to dive right into the Natural Number Game [2] or the Theorem Proving in Lean [3] (both linked from the Community site). 1. https://leanprover-community.github.io/ https://leanprover-community.github.io/ 2. http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game... 3. https://leanprover.github.io/theorem_proving_in_lean/ https://leanprover.github.io/theorem_proving_in_lean/
- Ericson2314 6y ago
  An addictive personality :). Theorem proving can be a fun open-world videogame, and I do hope these aspects can be refined overtime to make real mathematics a lot more accessible.
svara 6y ago
Not sure if this question even makes sense, or if it sounds hopelessly naive to someone in the know, my maths education ended in undergrad - can this type of push towards formalizing mathematical proofs be seen as a sort of continuation of Hilbert's program? If no, what's the difference? If yes, how are the fatal issues in that program avoided?
- pfortuny 6y ago
  It is essentially “the most one can do with Hilbert’s Programme”. Actually Hilbert’s Programme was shattered when his great hope (the proof of the consistency and completeness of Mathematics FINITISTICALLY) was proved impossible (actually inconsistent). But from the point of view of mechanizing Maths, it is more or less equivalent.
  - Ericson2314 6y ago
    Yeah Hilbert’s Program wasn't actually set back by the incompleteness theorems in the first place, it was all FUD.
    - pfortuny 6y ago
      Not sure what you mean by that: after Gödel, Hilbert essentially became hopeless.
      - Ericson2314 6y ago
        Hilbert misunderstood his own program :D
tpoacher 6y ago
"Liquid tensor experiment" <-- great pun in the title. Now if you'll excuse me, I'll go put on the amazing CD this is referencing.

75 points by alimw 6y ago

berndi 6y ago

I just hope NeuraLink pans out so I have a chance of understanding any of this in this life

soVeryTired 6y ago
I'm not a mathematician and I'm generally unqualified to comment on any of this but I'll have a stab anyway. The TLDR is that Peter Scholze, one of modern mathematics' most accomplished theory builders, has a concept called a 'condensed set' that he thinks can act as a drop-in replacement for topological spaces in most of mathematics. Topological spaces are perhaps one of the least restrictive models of 'space' is in mathematics. Peter thinks his definition will allow mathematicians to bring algebraic techniques to bear on problems that were previously not amenable to such methods. The problem is that everything rests on one theorem, whose proof is difficult. Because the proof is so foundational, he'd like to get it checked by computer instead of relying on the opinion of a handful of mathematicians, who may be sloppy in their checking.
deleted 6y ago
[deleted]

robinhouston 6y ago

The mathematics being discussed here is very new, as well as very technical, and I would guess the number of people who really understand it at the moment is at most dozens; certainly fewer than hundreds. I am certainly not one of those people. Nevertheless, I find this enormously exciting. Formalisation of mathematics has long been the preserve of a handful of logicians and type theorists. What we’re seeing here is one of the world’s leading mathematicians, whose work is situated squarely at the centre of what is today considered mainstream mathematics, advocating the importance of formalisation. If, like me, you believe that formalisation will be an essential part of the mathematics of the future, this is a very encouraging development.

pfortuny 6y ago

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

AcademicHamster 6y ago

What are good beginner resources to learn Lean?

tromoi57 6y ago
See the resources over at https://leanprover-community.github.io/learn.html https://leanprover-community.github.io/learn.html and the youtube playlist of the Lean for the Curious Mathematician workshop: https://www.youtube.com/playlist?list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N https://www.youtube.com/playlist?list=PLlF-CfQhukNlxexiNJErG...
ocfnash 6y ago
The Lean Community website [1] is a great place to start. Depending on your background you might like to dive right into the Natural Number Game [2] or the Theorem Proving in Lean [3] (both linked from the Community site). 1. https://leanprover-community.github.io/ https://leanprover-community.github.io/ 2. http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game... 3. https://leanprover.github.io/theorem_proving_in_lean/ https://leanprover.github.io/theorem_proving_in_lean/
Ericson2314 6y ago
An addictive personality :). Theorem proving can be a fun open-world videogame, and I do hope these aspects can be refined overtime to make real mathematics a lot more accessible.

svara 6y ago

Not sure if this question even makes sense, or if it sounds hopelessly naive to someone in the know, my maths education ended in undergrad - can this type of push towards formalizing mathematical proofs be seen as a sort of continuation of Hilbert's program? If no, what's the difference? If yes, how are the fatal issues in that program avoided?

pfortuny 6y ago
It is essentially “the most one can do with Hilbert’s Programme”. Actually Hilbert’s Programme was shattered when his great hope (the proof of the consistency and completeness of Mathematics FINITISTICALLY) was proved impossible (actually inconsistent). But from the point of view of mechanizing Maths, it is more or less equivalent.
- Ericson2314 6y ago
  Yeah Hilbert’s Program wasn't actually set back by the incompleteness theorems in the first place, it was all FUD.
  - pfortuny 6y ago
    Not sure what you mean by that: after Gödel, Hilbert essentially became hopeless.
    - Ericson2314 6y ago
      Hilbert misunderstood his own program :D

tpoacher 6y ago

"Liquid tensor experiment" <-- great pun in the title. Now if you'll excuse me, I'll go put on the amazing CD this is referencing.