I'm always surprised to see higher level mathematics on the front page here considering I doubt the majority of the people upvoting this would understand much of it, nevertheless given the state of how the average person views mathematics I guess more popularization can't be a bad thing regardless.

On the topic of document, quite a few times I've seen mathematicians say work on theorem provers and the sort are a waste of time and there's nothing to be learnt and blah blah blah and I think this is an excellent example of why this isn't the case. Kevin found a deficiency in his knowledge in algebraic geometry and upon spending some time on it related it to some wider topics in the foundations of mathematics (the notion of equality between set theory and homotopy type theory, for example see https://mathoverflow.net/questions/263024/does-equality-betw...). I would think there are many other things that we will discover that have been otherwise assumed or taken for granted when more mathematics is formalized by theorem provers and other tools.