No one is going to get tenure by spending 24 years on a problem with no results. The profs who have that much free time on their hands are already in the later stages of their careers with records of impactful results. By that time, a problem like that is more of a curiosity than sometimes expected to have broad concrete impact.

I'm no mathematician, but (1) seems like a bad situation to be in. I can't speak to the practical usefulness of potential mathematical solutions like proposed here, but it seems useless to have an individual professionally spend 24 years on a single problem only to make little progress and eventually retire so the next person can stare at it.

That's how most other fields progressed most of the time, isn't it?

>> virtually none of this stuff is possible with technology any normal citizen has access to.

Initially, yes. Long term, however? Perhaps still yes.

> 5) professors are left to rewrite the AI Lean slop into real human-readable math?

6) AI writes the proof into something easier to follow than a PDF document.

Hmm. Oh shit.