I know it’s not the point of the article but OP is dead wrong about what makes a good proof. Yes, they inevitably include a surprising concept but that’s just because all the obvious ones are already taken. A proof that only contains obvious steps is, for the most part, already proven.

If someone proves the Reimann Hypothesis tomorrow, it’ll be a great achievement regardless of the fact that pretty much everyone already thinks it’s true.

Author here. That's exactly what I said in the article.

> Surprising proofs reach conclusions that the mathematical community assumed were wrong, or prove theorems in ways that we thought wouldn’t work, or prove conjectures that we thought might be impossible to prove.

Many smart people have tried for more than 150 years to prove the Reimann Hypothesis; it might be impossible to prove.

If it's proved tomorrow, I'll be very surprised, and so will you. I'll be surprised if it's proved this year, or this decade.

If you set to work trying to prove RH, you're gonna try some interesting approaches, looking for underexplored areas of math that you're optimistic will tie back to RH. (This is how Fermat's Last Theorem finally fell.)

If you hook an LLM up to Lean and set it to work, you'll find that it actively avoids novel techniques. It feels like it's actively trying not to write a publishable paper. It's trying to minimize surprises, which means avoiding proving anything publishable.