About Us

The Charles C. Hoskinson Center for Formal Mathematics at Carnegie Mellon University is dedicated to the use of formal computational methods and new technologies for mathematical research and education. Our goal is to support

• mathematical research, through the development of formal methods for the verification, communication, exploration, and discovery of mathematics;
• curation and dissemination of mathematical knowledge, through the development of online formal libraries, interfaces, and search tools;
• mathematics education, through the development of technology and teaching materials based on formal methods;
• mathematical applications of formal methods in computer science and engineering; and
• applications of automated reasoning and machine learning to mathematics.

Currently, most center activities make use of the Lean Programming Language and Proof Assistant. We work closely with the Lean community and support its efforts to develop the formal mathematical library, Mathlib.

The center was established in September 2021 by a gift from Charles Hoskinson. It is housed in the Department of Philosophy at Carnegie Mellon, with offices and a collaborative meeting space in Baker Hall 139. The center's endowment supports PhD students, postdoctoral fellows, undergraduate researchers, visitors, and meetings. It also provides build servers for the development and maintenance of Mathlib.