A team drawn from Peking University, Beijing Normal University, Capital Normal University, Great Bay University and the Zhongguancun Academy has published an AI-assisted formalisation of the Poincaré conjecture in Lean 4, the proof assistant that checks every step of an argument mechanically. The paper went up on arXiv on 6 October. It proves both the topological and the smooth versions of the theorem and passes a full Lean build.
The figures are the useful part. Mathematicians first spent several months writing a proof blueprint and cutting it into milestones agents could work on in parallel. The formalisation phase itself then took a little more than two weeks, using what the authors describe only as publicly available commercial models, for about $25,000 in subscriptions and server rentals. Roughly 48% of the Lean source is background theory rather than the proof.
Two things are worth holding on to. The authors are explicit that the scope and the unblocking were human work, unusual candour in a field that tends to report only the finished artefact. And they are not alone: a separate team posted its own Lean formalisation of the same result on 27 September. Neither has been reviewed from outside yet, and the Lean build is a check on the formal statements, not on whether those statements say what mathematicians mean.
Source: Zhang and others, An AI-Assisted Formalization of the Poincaré Conjecture, arXiv:2610.08329.