This is, as always from Grant Sanderson, thought provoking and opens new insights.

It occurs to me on reading this that there’s a connection to other computerized mathematical activities.

Occasionally some computer lab in the past would announce that they have computed pi to more digits than ever before; or a new Mersenne prime will be found.

These count as ‘math news’ but they’re of little interest to mathematicians. These computational efforts demonstrate the great power of computers but they do nothing to advance mathematical understanding. Finding a larger Mersenne prime is not surprising to anyone; we’re pretty sure there’s an infinite number of them. Finding the largest Mersenne prime would be the surprise.

So it is with proofs. An LLM might prove some conjecture - Riemann, say or P≠NP. But in general we know that things can be proven and we think those things are probably true, so the existence of a proof doesn’t do much more than producing a new Mersenne prime does.

It’s only if in proving the thing we learned something that there’s actual value in the proof.