On September 22, 2021, Carnegie Mellon University announced that a $20 million gift from blockchain entrepreneur Charles C. Hoskinson will be used to establish the Hoskinson Center for Formal Mathematics, housed in the Department of Philosophy. You can read the university press release and watch Hoskinson's YouTube announcement. You can also watch Hoskinson's presentation and my presentation at an inauguration ceremony that was held at Carnegie Mellon the day before. The slides I used for the presentation are here.

The center's mission is to support the work being done by the Lean community, to promote the use of Lean and its libraries, and to seek out ways of using the technology to make mathematics accessible and enjoyable to as wide an audience as possible.

The initial endowment will be used to support postdoctoral researchers and graduate students, as well as occasional meetings and visitors. In the near future, the center will focus on supporting the port of mathlib to Lean 4, developing automation and the user interface, and, perhaps most importantly, preparing textbooks and educational materials based on Lean.