In a previous post, I pointed out Peter Scholze’s liquid tensor challenge to the formalization community. I was lucky enough to hear a fantastic talk on the subject by Johan Commelin at a K-theory workshop organized by Oliver Braunling and Michael Groechenig. Basically, the community working on the project, led by Commelin, is half-way done and Scholze says they have verified the main thing he was worried about. This seems to be a tremendous achievement, although I am certainly not an expert. Scholze gives an auto-interview on Xena and there is a Blueprint for the project.