[qguv]

I think this is AI generated; the Lean snippet on page 33 is full of LaTeX syntax.