Comment by c7b
1 day ago
> we might imagine what it could look like to have an analog of the Millennium Prize Problems for open exposition problems
The core idea seems to me that we should shift the standards for professional evaluation from generating proofs to generating explanations. Makes sense that such a proposal would come from the 3B1B guy, and I actually agree with it, irrespective of AI. But what eludes me is how that could be a defensive mechanism against AI automating humans out of mathematics. AI is likely no less good at producing natural language explanations as it is at generating rigorous proofs. It's telling that even Terrence Tao turned to AI to understand AI-generated results [0]. It seems that the essay doesn't address that issue at all.
It’s a task much harder to RL and much more subjective. I don’t want to say we won’t get there, but let’s just say that LLMs could “write” well enough since gpt3.5 era and I don’t think the pleasantness of the prose improved dramatically since then.
And subjectively the explanation LLMs currently provide are usually horrible, horrible enough that I usually just instruct them to provide me human written literature I can read.
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.