We present a Lean 4 formalization of the Poincaré conjecture that is assisted by AI throughout the development. At the outset the project lacked reusable formal infrastructure for the geometric analysis underlying the proof, so we first built a low‑level library. Then mathematicians supplied a detailed proof blueprint and broke it down into explicit milestone statements. Each milestone served as a target for parallel AI agents and gave the mathematicians clear locations of potential blockers, enabling timely and effective guidance. Our analysis identifies the concrete human interventions and organizational choices that made this workflow possible, offering insights for future large‑scale formalization efforts. The project thus provides an initial reusable infrastructure for geometric analysis; once matured, it could substantially reduce the cost of verifying mathematical results.
Review