alt Hacker News> I would generally expect this state to resolve quickly to "Proven and Verified" (the tendency in mathematics historically has been for complicated first-proofs of results, followed by significant reductions in proof complexity as new tools and definitions become available),
A bit of an oversimplification, I think. Definitely there are some simplifications, but I wouldn't say really significant to the point where "resolve quickly" follows, along the lines of what you said.
Most complicated math is still nearly as complicated as when it was invented. Simplifications to presentation maybe, and some reduction in the proof difficulty yes, but not to the point of being significant in the way you describe. Any modern result that has been around for 20 years likely hasn't undergone a serious simplification, for example.
Last I checked (a few weeks ago, but things have been moving faster lately), the four-color theorem remains "computer proved". There has been work done on it since the original proof that has successfully simplified it, in the sense that those proofs involve less grinding through cases than the original. But it still involves grinding through more cases than can be sensibly labelled a "human comprehensible" proof, with some sort of insight into the problem space. It's still just a big set of cases being checked, and a useful final result, but no insight given in the proof.
This seems like an interesting test case to build up for AI models.