| Résume | Formalization of mathematics began in the 1970s with various goals. Verifying the correctness of proofs was only one of them and, for most researchers, not the most important. With the rise of AI-assisted and AI-generated proofs, however, the need for reliable verification tools has become increasingly important. In this talk, we will use examples from differential geometry and other areas to explain what it means for a proof to be formalized, whether by a human or by a large language model. We will explain which problems formalization can, and cannot, solve. Finally, we will discuss its role in recent announcements, including the claimed solution to the Navier–Stokes problem. |
