The formal proof of the Kepler conjecture was featured in an article “Quod Erat Demonstrandum” by Barry Cipra in the series What’s Happening the the Mathematical Sciences (volume 1) of the American Math Society. The article “presents two examples of perseverance in mathematicians’ pursuit of truth using, in particular, computers to verify their arguments.”

Our number’s up: Machines will do maths we’ll never understand, Aron Jacob, Aug 2015. This article mentions Mochizuki’s claimed proof of the ABC conjecture and claims that “software is already cracking theorems that humans have struggled to prove.”

A Spanish language Ted talk Math is Forever (with over a million views) by
Eduardo Saenz de Cabezon, uses the Pythagorean theorem, the honeycomb theorem, and the Kelvin problem as illustrations of the eternal nature of mathematics.

Die Kunst, Orangen zu stapeln. The radio station Deutschlandfunk aired a 30-minute feature by author Thomas Reintjes about Hales and the proof of the Kepler conjecture, April 2015.