Mixed feelings as usual: It's amazing and wonderful to see proof assistants get this much coverage, but I still really wish any of these articles would pay better homage to the history of the field, the mathematicians using other proof assistants, and so on.
