An AI-Assisted Formalization of the Poincaré Conjecture

Zhiyuan Zhang, Axel Delaval, Leheng Chen +6

We present an AI-assisted Lean 4 formalization of the Poincaré conjecture. The project began with limited reusable formal infrastructure for the geometric analysis behind the proof…