A mathematical formalisation challenge by Peter Scholze

Post by throwaway_pdp09 » Sun, Dec 06, 2020, 6:40 PM UTC

kevinbuzzard wrote: post #7

pfortuny wrote: post #6

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 judgme…

[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…

Post by pfortuny » Sun, Dec 06, 2020, 7:19 PM UTC

kevinbuzzard wrote: post #7

pfortuny wrote: post #6

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 judgme…

[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…

Post by pfortuny » Sun, Dec 06, 2020, 7:24 PM UTC

svara wrote: post #14

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?

Post by Ericson2314 » Sun, Dec 06, 2020, 7:29 PM UTC

pfortuny wrote: post #15

svara wrote: post #14

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?

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.

Post by Ericson2314 » Sun, Dec 06, 2020, 7:53 PM UTC

pfortuny wrote: post #13

kevinbuzzard wrote: post #7

Earlier quoted context omitted.

[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…

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.