In case anyone is curious, there is a discussion of AI in Section 5 (page 8 of the PDF). This direct link might work: https://arxiv.org/pdf/2511.14653#page=8
I think that (most) mathematicians were not that interested in formal proof until quite recently (as opposed to computer scientists), and most of the interest in lean has been self-reinforcing, namely there is a (relatively speaking) huge library of formally verified mathematics. So now basically anyone who cares about formal verification as a tool for mathematics is working in lean. There are of course numerous techincal differences which you can read about if you google coq vs lean.
It will take another few months at least, and the rest of the argument will comprise a fair few pages. But the hardest part is over.
When working toward a problem of this magnitude, it is natural to release papers stepwise to report progress toward the solution. Perelman did the same for the Poincare conjecture. Folks knew the problem was near a solution once the monotonicity proof of the W functional came out.
> Folks knew the problem was near a solution once the monotonicity proof of the W functional came out.
This isn't true, it was a major accomplishment but by far the easiest part of Perelman's papers and not actually even part of the proof of the Poincaré conjecture.
Interesting, this was the big 'a-ha' moment in the grad course I took on the subject. Surgery was clearly important too, but this seemed to be more apparent from Hamilton's work. The W functional was what provided the control needed. Also, calling it 'easy' feels like it dismisses the insights necessary to have developed the functional in the first place.
Happy to be corrected on this; I wasn't an active mathematician at the time, so everything I know comes from other accounts.
I called it the easiest part of his papers, not easy. Either way, it's actually not relevant to the proof. For example, I believe that Morgan and Tian's 500 page exposition of the proof doesn't mention it even once.
Moreover I'd strongly dispute that there was any particular point where it was clear that the problem was "near a solution." The W functional is an example where experts could very quickly verify that Perelman had made at least one major new discovery about the Ricci flow. But the proof of the Poincaré conjecture was on another order of complexity and required different (more complicated) new results about Ricci flow.
Citation based metrics are much more prevalent in physics than in math (at least in the US and most countries in Europe). When compared with physics, my impression is that mathematics has the tradition "slow, long term" over "rapid, incremental." Of course, it's not perfect.
It is an issue if a mathematician has to apply for grants. Often they are in the same competition as physicists, for instance, and then metrics do matter.
This article does not seem to quite convey the experience of a pure mathematician. Yes, citation fraud is happening on an apalling scale, but no it is not a serious issue for mathematicians.
The problem of AI generated papers is much more serious, although not happening on the same scale (yet!).
reply