Daniel Bergh and David Rydh: Functorial destackification and weak factorization of orbifolds shows how to reduce the destackification problem to the case of abelian stabilizers, which is covered by the earlier paper Functorial destackification and weak factorization of orbifolds by the first author. This is cool stuff, and I think (but I haven't checked carefully) it is also a necessary step in the geometricity proof for smooth and proper Deligne–Mumford stacks, which is a result I really like.
Lean perfectoid spaces by Kevin Buzzard, Johan Commelin and Patrick Massot is a formalisation of the notion of a perfectoid space. Also check out the accompanying blogpost, featuring a visualisation of how Lean sees the definition, in terms of the subfields we mathematicians recognise in the definition.
On a related note, Schemes in Lean is a rewritten-from-scratch / cleaned up version of the formalisation of the notion of a scheme. These are exciting times to live in (but I am very much an outside for these things, unfortunately).
Chances are that you have already seen it, given how popular it was last week, but Chalk of Champions is a mockumentary about the famous Japanese chalk.