Comment by c7b

I mean, there's centuries' worth of mathematical prose to train on. But that's presumably already in the training data, so if it isn't good enough today, it might not get better fast enough to keep track with how fast they'll get better by training on formally verified math. But then again, the prose in Terry's conversation I linked above seemed pretty useful. But it's also a problem requiring famously little advanced mathematics.