AI helps formalize complex geometry proof in Lean 4 language
An AI-Assisted Formalization of the Poincaré Conjecture
Artificial Intelligence
Summary
The Poincaré conjecture is a famous geometry problem that mathematicians have proved, but turning that proof into a fully checked computer version is very hard. The authors used artificial intelligence to help organize and build this formal proof in Lean 4, a language for verifying math precisely. They set clear milestones and combined human guidance with AI work to manage the project efficiently. This effort could make it easier and cheaper to check other complicated math proofs in the future.
What this means in practice
- •For formal verification engineers: Use AI-assisted milestone organization to streamline constructing complex formal proofs in proof assistants like Lean 4.
- •For software development teams: Integrate reusable formal infrastructure from geometric analysis to reduce time and errors during formal verification of algorithms involving geometry.
Authors
Zhiyuan Zhang, Axel Delaval, Leheng Chen, Jinxuan Chen, Jie Xu, Yuxuan Liao, Jiedong Jiang, Chunlei Liu, Bin Dong
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.