Bin Dong

The FrenzyMath team at Peking University's Beijing International Center for Mathematical Research completed a full Lean 4 formalization of the Poincaré conjecture: about 3.2 million lines of code and more than 76,000 theorems and lemmas. Three math-trained AI developers, with postdocs and doctoral students, used public commercial large models and a self-developed agent workflow to port the 500-plus-page Morgan–Gang Tian monograph into Lean across 83 milestones.

The work took about half a month and cost under $30,000 in model API calls and server overhead. The team built Mathlib prerequisites in Riemannian geometry, Ricci flow, and topology from scratch. It says this is the first Poincaré formalization to pass both Lean build and Comparator checks, with independent nanoda kernel verification and no sorry or extra axioms.