A Dataset of Modern Formalized Theorem Statements

This project creates a public dataset of hundreds of formalized statements of recent theorems from top journals, such as the Annals of Mathematics. In doing so, it will address a key lack of formalization at the frontier of mathematical research. Through dedicated expert formalization, this project will significantly expand formalized mathematics libraries and provide clear targets for AI systems on a wide range of tasks, including auto-formalizing proofs and assisting humans in proof formalization.