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.