Computer assisted verification of contemporary mathematics

Half a year ago Steffen Kionke wrote a blog post on condensed mathematics wherein he mentioned that Peter Scholze put up a challenge to formally verify a key fundamental result of a joint paper with Clausen: a result Scholze terms his most important theorem to date.

Today I want to inform you that the mentioned challenge of Scholze was beaten: The entire part of the argument that Scholze was unsure about was successfully computer verified!

(link to more information, link to another blog about this topic)