HOW TO FORMALIZE ALL OF MATHEMATICS

Summary from the TLDR newsletter

It would be a terrible waste of resources to spend millions of dollars to formalize mathematics results in libraries nobody uses. Doing so could also disincentivize good research and productive use of AI, disrupt the social norms and practices research depends on, and set the field back decades. Several projects are now working to ensure formal libraries fulfill the community's mathematical goals. Within the next few years, most of mathematics will be able to be formalized in such a way that mathematicians can explore, build on, and make use of formal libraries. This will significantly extend their ability to develop and discover new mathematics.