Abstract
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. To organize this work, we combined a proof blueprint prepared by mathematicians with explicit milestone statements. These milestones enabled parallel agent work and gave mathematicians clear points to locate blockers and provide effective mathematical guidance. Our analysis identifies the human interventions and organizational choices behind this workflow. The project provides a starting point toward reusable infrastructure for future formalization projects; such infrastructure, once developed, could eventually reduce the cost of verifying mathematical results in geometric analysis.
Keywords
Subject
Publication details
- Journal
- Not available
- Open access
- Green open access
Cite this article
APA 7
Zhang, Z., Delaval, A., Chen, L., Chen, J., Xu, J., Liao, Y., Jiang, J., Liu, C., & Dong, B. (2026). An AI-Assisted Formalization of the Poincaré Conjecture. https://omanscience.com/en/articles/an-ai-assisted-formalization-of-the-poincar-conjecture
MLA 9
Zhang, Zhiyuan, et al. "An AI-Assisted Formalization of the Poincaré Conjecture." https://omanscience.com/en/articles/an-ai-assisted-formalization-of-the-poincar-conjecture.
Chicago (author–date)
Zhang, Zhiyuan, Axel Delaval, Leheng Chen, Jinxuan Chen, Jie Xu, Yuxuan Liao, Jiedong Jiang, Chunlei Liu, and Bin Dong. 2026. "An AI-Assisted Formalization of the Poincaré Conjecture." https://omanscience.com/en/articles/an-ai-assisted-formalization-of-the-poincar-conjecture.
Harvard
Zhang, Z., Delaval, A., Chen, L., Chen, J., Xu, J., Liao, Y., Jiang, J., Liu, C. and Dong, B. (2026) 'An AI-Assisted Formalization of the Poincaré Conjecture', Available at: https://omanscience.com/en/articles/an-ai-assisted-formalization-of-the-poincar-conjecture.
Vancouver
Zhang Z, Delaval A, Chen L, Chen J, Xu J, Liao Y, et al. An AI-Assisted Formalization of the Poincaré Conjecture. https://omanscience.com/en/articles/an-ai-assisted-formalization-of-the-poincar-conjecture
IEEE
Z. Zhang, A. Delaval, L. Chen, J. Chen, J. Xu, Y. Liao, J. Jiang, C. Liu, and B. Dong, "An AI-Assisted Formalization of the Poincaré Conjecture," https://omanscience.com/en/articles/an-ai-assisted-formalization-of-the-poincar-conjecture.