The Annals Challenge

My team of post-docs funded by this Renaissance Philanthropy grant has constructed a dataset of 50 Lean statements, corresponding to 50 important recent mathematical theorems! The 50 theorems were all published in the Annals of Mathematics (a prestigious mathematical journal) in the 2020s. We build on mathlib, Lean’s mathematics library; my team has built many new definitions and got them merged into mathlib as part of this project. As well as the dataset, we would like to issue two challenges related to it. A challenge for humans — state more theorems We have formalized the statements of around 20 percent of the papers which have appeared in the Annals of Mathematics since 2020. However it seems to be a formidable challenge to get this percentage up to anywhere near 100 percent. A paper in the Annals might mention the Fukaya category associated to a symplectic manifold in the statement of its main theorem, or cuspidal automorphic representations for a connected reductive group, or…