Comment by jey

Shrug. It's how I do my research now. There were too many mathematical errors when I had agents writing LaTeX directly, even with adversarial reviews, so now I only read stuff that's been formalized, with whatever kinks worked out along the way.