> had released a blob of 722 mathematical papers produced by a “frontier model”

I prefer to call them PDF instead of papers and preprints :)

Anyway, like 1/3 or 1/2 have a Lean proof and I guess they are absolutely right. The other is more complicated. I guess most are right too, but there may be surprises.

AI is better than me in short and well specified problems, like IMO or research problems with a solution of 3 or 4 pages. For longer problems or fuzzy objectives, I've seen AI making mistakes or misleading conclusions.

>> proofs, which are easily counted by academic administrators, were only ever a proxy.

That's the real problem. Papers published in serious peer review journals is an easy metric, so everybody adopted it, in spite it's not easy at all.

Anyway, it's strange that nobody is talking about applied math. People in other arrea care about the results (and perhaps the hypothesis to verify before using it), not about how mathematicians keep the score.