Four-Person Team Completes Lean Formalization of Poincaré Conjecture Proof with AI Assistance

On Sept. 28, 2026, a four-person team led by Ben Chow, a mathematics professor at UC San Diego and a former student of Shing-Tung Yau, said it had completed a full formalization of Hamilton and Perelman's proof of the Poincaré conjecture in the Lean proof assistant. The project comprises about 4.7 million lines of code, all of which pass Lean's kernel check, with no "sorry" placeholders left in the final repository.

The team includes Ziyang Qin, Yuan Liao, and Ayush Khaitan. Around 2.7 million lines were written in the final two weeks with assistance from AI tools such as ChatGPT and Claude. The formalization's dependency chain covers 14,197 files and about 4.02 million lines. Perelman's three papers correspond to roughly 660,000 lines, while the canonical neighborhood theorem accounts for about 2.72 million lines, around two-thirds of the dependency chain.

Ben Chow spent decades working on Ricci flow and began organizing a Lean study group in autumn 2025. Ziyang Qin, a recent Cornell graduate, and Yuan Liao first spent seven months writing about 2 million lines of foundation code. Khaitan joined in September 2026 for the final push. According to Khaitan, the main AI assistants were ChatGPT Astra and Claude Fable, with human members choosing definitions and statements and ensuring the verified theorem matches the intended mathematical claim.

The Poincaré conjecture, posed by Henri Poincaré in 1904, says every simply connected closed 3-manifold is homeomorphic to a 3-sphere. In Lean, the final statement occupies a 23-line file.