alt Hacker NewsTerence Tao had a nice talk from the Future of Mathematics conference posted yesterday [0] that shapes a lot of my own feelings on this matter.
The short of it is he argues how first to correctness shouldn't be the only goal / isn't a great optimisation incentive. Presentation and digestibility of correct results is a missing 1/3 when you've finished generation and verification. I completely agree with him. You don't just need an AI generated proof of the Reimann Hypothesis. You would really like it to be intentional and structured for others to understand.
A really beautiful quote I learned of in the talk is this:
> "We are not trying to meet some abstract production quota of definitions, theorems, and proofs. The measure of our success is whether what we do enables people to understand and think more clearly and effectively about math." - William Thurston
Ya, I think this totally makes sense. Just to be clear though, I don’t think we’re actually disagreeing. A proof of the Riemann hypothesis that’s obtuse and basically unreadable is a great step on the path to a proof that is enlightening and clear. If ai provides correct-but-annoying results, I’m confident humans can still learn benefit from that marginal result.