This post is inspired by Alex Engel’s post “Validity of results II” on incorrect results and computer proof checking. Before I get there, let me start with some background first and reveal the connection later.
Dustin Clausen and Peter Scholze have put forward the idea of “condensed mathematics” which aims at replacing topological spaces by “condensed sets”. Compactly generated weak Hausdorff spaces embed fully faithfully into the category of condensed sets, so we still have our favourite spaces. The advantage of condensed sets however is that the category of “condensed abelian groups” is in fact a nice abelian category which satisfies all properties needed to coveniently use homological algebra. On the other hand, homological algebra with “topological abelian groups” is a mess.
I will not attempt to define condensed sets here (a good starting point is the “Masterclass in Condensed Mathematics” thought in Copenhagen this year). . In a nutshell: Central objects in condensed mathematics are profinite sets. Roughly speaking, you replace a topological space X by the functor which takes a profinite set S to the maps from S to X. Underlying is a basic intruiging observation: For every compact Hausdorff space X there is a surjection from a profinite set onto X. For example, the decimal expansion is a surjection from the profinite set of sequences in {0,1,2,3,4,5,6,7,8,9} onto the interval [0,1].
What does this have to do with computer proof checking? Peter Scholze wrote a guest blog post for the xenaproject. The xenaproject blog is run by Kevin Buzzard who is advertising computer verification in order to put mathematics on a more solid ground. In his guest post Scholze puts up a challenge to formally verify a key fundamental result of Clausen-Scholze – a result he terms his “most important theorem to date.”
More details can be found in Scholzes very readable introductory blog post on condensed mathematics posted in the xenaproject.
I read the blog post by Scholze and noticed at the end of it the following statements (my own comments are in parenthesis):
— I spent much of 2019 obsessed with the proof of this theorem, almost getting crazy over it. In the end, we were able to get an argument pinned down on paper, but I think nobody else has dared to look at the details of this, and so I still have some small lingering doubts.
(Have you ever heard somebody, especially somebody famous, admit that he or she wrote down a proof and lectured already several times about it, but is still not completely sure if the proof is correct? I think this happens more often in mathematics than we would like to admit. I am glad that Peter Scholze is brave enough to say this out loud.)
— I have occasionally been able to be very persuasive even with wrong arguments. ([…] 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.)
(This shows how often, even for top mathematicians, it happens that one overlooks serious mistakes or gaps in proofs. In this case the wrong argument was eventually found, but it shows that relying solely on the word of very few famous persons with respect to the validity of an argument might still be dangerous. I am referring here mainly to the notion of ‘elders’ and the discussion surrounding them which are mentioned several times in the blog post on MathOverflow that I linked in my previous post ‘Validity of results, II’.)