Skip to content
DraconiticResearch
Search Sources API
197,768 studies31 sourcesUpdated 21 min ago
PreprintCC BY 4.0arXiv

An AI-Assisted Formalization of the Poincaré Conjecture

  • Zhiyuan Zhang
  • Axel Delaval
  • Leheng Chen
  • Jinxuan Chen
  • Jie Xu
  • Yuxuan Liao
  • Jiedong Jiang
  • Chunlei Liu
  • Bin Dong
Open at sourcePDFDOICite

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.

Related

  1. A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture
    Ziyang Qin, Yuan Liao, Ayush Khaitan +1
    arXivPreprintCC BY 4.0Full textGeometry & topologyarXiv
  2. A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture
    Yuan Liao, Ziyang Qin, Jui-Hui Chung +7
    arXivPreprintCC BY 4.0Full textGeometry & topologyarXiv
  3. Bridging Scales: Asymptotic Analysis and AI-Assisted Formalization
    Xu Yang
    arXivPreprintarXiv licenceFull textNumerical analysis & scientific computingarXiv
  4. Poincaré compactifications of pullbacks of parallel vector fields under counterexamples to the real Jacobian conjecture
    Francisco Braun, Paulo Machado
    arXivPreprintCC BY 4.0Full textDynamical systemsarXiv
  5. An independent computer-assisted proof of the Chen-Raspaud conjecture for k=4
    Marysia Nazarczuk
    arXivPreprintarXiv licenceFull textCombinatorics & discrete mathematicsarXiv

Cite

BibTeXRIS
BibTeX
@misc{zhang2026aiassisted,
  title = {{An AI-Assisted Formalization of the Poincaré Conjecture}},
  author = {Zhiyuan Zhang and Axel Delaval and Leheng Chen and Jinxuan Chen and Jie Xu and Yuxuan Liao and Jiedong Jiang and Chunlei Liu and Bin Dong},
  howpublished = {arXiv},
  year = {2026},
  month = oct,
  doi = {10.48550/arxiv.2610.08329},
  eprint = {2610.08329},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2610.08329},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - An AI-Assisted Formalization of the Poincaré Conjecture
AU  - Zhiyuan Zhang
AU  - Axel Delaval
AU  - Leheng Chen
AU  - Jinxuan Chen
AU  - Jie Xu
AU  - Yuxuan Liao
AU  - Jiedong Jiang
AU  - Chunlei Liu
AU  - Bin Dong
PY  - 2026
DA  - 2026/10/06
PB  - arXiv
DO  - 10.48550/arxiv.2610.08329
UR  - https://arxiv.org/abs/2610.08329
AB  - 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.
ER  -