Carnegie Mellon Receives $20 Million to Establish Hoskinson Center for Formal Mathematics in Dietrich College

Center aims to improve global access to mathematics, improve the power of computational proof-assistants, and increase collaboration among educators, researchers, learners

News provided by

Carnegie Mellon University

Sep 22, 2021, 10:05 ET

PITTSBURGH, Sept. 22, 2021 /PRNewswire/ -- Entrepreneur Charles C. Hoskinson has made a $20 million gift to Carnegie Mellon University to establish the Hoskinson Center for Formal Mathematics, the university announced today. The center will advance mathematical research by improving global access to knowledge and resources for mathematics researchers, educators and learners.

"This generous commitment from blockchain pioneer Charles Hoskinson will allow CMU to pursue new collaborations at the intersection of mathematics, logic and computation," CMU President Farnam Jahanian said. "By enabling a new way of doing math and creating collaborative digital libraries for mathematical tools, we can accelerate discoveries in a broad range of disciplines. This center is a distinct expression of our strengths in collaboration and technology-driven experimentation, and I am tremendously excited by its potential."

Sitting at the intersection of philosophy, mathematics and computer science, "formal mathematics" works on mathematical theorems and proofs after they are stated in a formal language, which in turn allows us to develop computer programs to assist in discovering proofs, verifying the steps humans enter, and certifying the correctness of any proof that can be so formalized. The Hoskinson Center will develop the technology (via the Lean platform) and techniques needed to increase world-wide access to the power of formal mathematics. The center will support the development of Lean's digital library, develop new tools to help convert mathematical statements from natural language to a formal language, and create educational resources to make these tools widely available. Used widely, these tools have the potential to super-charge mathematics, which in turn has the power to super-charge computer science, physics and any other discipline that uses mathematics.

"Carnegie Mellon has the resources and experts to take the study of formal mathematics and disseminate it in a meaningful way," Hoskinson said. "We can bring together the best minds in mathematics, computer science and machine learning to create an infrastructure for using formal mathematics as a core educational tool. I am honored to be part of the creation of such an important center where collaboration, exploration and discovery opens the door to incentivizing and supporting mathematical activity and giving it the resources for advanced methods of automation."

Hoskinson founded the Bitcoin Education Project in 2013, before joining the blockchain-based software platform Ethereum founding team. He went on to found Cardano, a public blockchain and smart-contract platform, and Input Output (IOHK), an engineering company that builds cryptocurrencies and blockchain with more than 400 employees in over 50 countries.

With extensive experience with mathematics and technology, Hoskinson sees the global potential of formal methods — including the development of a communal digital mathematical library — in making mathematics accessible to a broader community.

The new center will be led by Jeremy Avigad, professor of philosophy in CMU's Dietrich College of Humanities & Social Sciences and professor of mathematical sciences in the Mellon College of Science, who will provide mentorship and guidance to direct research contributions and collaboration. Avigad's research areas include mathematical logic, automated reasoning and philosophy of mathematics. The center will include joint postdoctoral positions between the Dietrich College and Mellon College of Science.

"Computational proof assistants based on formal mathematics are a transformative technology," Avigad said. "They not only help us ensure that the mathematics we do is correct, but also provide powerful new tools for communication, collaboration, education and mathematical discovery."

Avigad, his students and his colleagues have been working with Lean, a software platform developed by Microsoft Research. Lean automates parts of the mathematical process and facilitates the development of mathematical proofs that are fully checked by the software. The center will develop ways of making Lean accessible to newcomers with limited background and computing power, in a manner that can scale to expert use.

"The Department of Philosophy is a recognized world leader in formal logic and the foundations of mathematics, and this center brings together areas of strength in mathematics, logic, computation, computer science and philosophy," said Richard Scheines, Bess Family Dean, Dietrich College of Humanities and Social Sciences. "Charles' generosity is helping us to make it possible for Lean mathematics to be more predominantly studied and to make it more accessible as an educational tool."

"Mathematics is essential to scientific discovery and analysis. Bringing the latest technology-enabled tools to our researchers and students will further our vision for creating the future of science," said Rebecca W. Doerge, the Glen de Vries Dean of the Mellon College of Science. "The Mellon College of Science community, including our highly ranked Department of Mathematical Sciences, is excited to collaborate on this center as we continue to move forward the field of mathematics in a truly interdisciplinary fashion."

The gift is the most recent commitment to be announced as part of Make Possible: The Campaign for Carnegie Mellon University. The campaign's supporters are accelerating the university's ambitious strategic priorities, with a goal of raising $2 billion in private philanthropy for initiatives across its seven colleges and schools. To date, more than 52,000 supporters have contributed more than $1.75 billion.

SOURCE Carnegie Mellon University