Kotlopou an hour ago
It's also all charmingly tiny. I was surprised at the quality of the LaTeX generated from a network trained on a single book -- it looks like a proof, has sequential lemmas, closes all brackets...
Also interesting to read the original discussion with a decade of hindsight: https://news.ycombinator.com/item?id=9584325