This is great work. But to be clear: a community effort by 20+ people, after 6 months of work, managed to make progress toward proving a theorem, including pro

This is great work. But to be clear: a community effort by 20+ people, after 6 months of work, managed to make progress toward proving a theorem, including proving some of the trickiest technical parts. As I said before, this is like 2 orders of magnitude more effort than the original plain-language (slightly sloppy/underspecified) proof. Scholze: > I cannot read the proofs at all — they are analogous to referring to theorems only via their LaTeX labels, together with a specification of the variables to which it gets applied; plus the names of some random proof finding routines.