Carnegie Mellon receives $20 million
to establish
Hoskinson Center for Formal Mathematics
Pictured above, from left to right: Richard Scheines, Farnam Jahanian, Hoskinson and Jeremy Avigad
Center aims to improve global access to mathematics,
improve the power of computational proof-assistants,
and increase collaboration among educators, researchers, learners
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.
■ Shilpa Bakre
Faculty Notes
Alissa Crans mentors mathematicians
After almost 20 years of teaching mathematics at Loyola Marymount in Los Angeles, California, Alissa Crans is spending this year at Carnegie Mellon University after she earned the Shelley Distinguished Professorship.
“I think it’s a wonderful opportunity,” Crans said. “I can talk to people outside of my own department, engage in everything that the department has to offer in terms of seminars, colloquia and graduate students.”
The Shelley Distinguished Professorship is an opportunity for experienced mathematics professors to teach at CMU for an academic year.
Crans has done extensive research in quantum algebra and geometric topology, and she said she hopes to inspire students to be as passionate about math as she is.
This fall semester, Crans taught Linear Algebra, an elective for junior and senior mathematical sciences majors, and she assisted with EUREKA!, a core curriculum class for all first-year students in the Mellon College of Science.
“The students are incredibly dedicated to their education, and as an instructor, it’s very rewarding to know that the students are motivated, curious, interested and hard working,” Crans said. “That leads to really great conversations in the classroom.”
Crans also has been mentoring three teaching postdoctoral fellows — a new program for the Department of Mathematical Sciences. Crans meets with the postdoctoral researchers regularly to offer advice on teaching and applying for tenure-track positions.
“We are thrilled with everything Alissa is bringing to the Shelley fellow position within such a short period of time, clearly setting a high bar for the future,” said Prasad Tetali, the Alexander M. Knaster Professor of Mathematical Sciences and department head. “Delivering effective instruction in mathematics to the CMU students has always been a top priority of our department; the creation of the new teaching postdoctoral fellowship positions, along with providing appropriate support and eventual placement of the fellows, is our effort to contribute to the national workforce in high-quality mathematics instruction.”
Outside of the classroom, Crans strives to make sure that mathematics is a welcoming place for students from all backgrounds. A member of the Association for Women in Mathematics, she has reached out to the students in the CMU chapter and has participated in lunches and teas, making sure that women in mathematical sciences know the resources available to them.
“Thanks to the AWM, I got involved in various activities as an undergraduate,” Crans said. “I was supported as a graduate student as a pre-tenured faculty member. Giving back to that community is something that I’ve worked very hard at over the course of my career.”
■ Kirsten Heuring
Staff News
Chagas engineers computing solutions
Nuno Chagas, the Linux Systems Administrator for the Department of Mathematical Sciences and the Mellon College of Science, assists with everything from hardware and software to suggesting ways that graduate students can improve their computational research.
“The most interesting thing about working with students is to see their take on the solution and how that may differ from our preconceptions,” Chagas said. “It goes back to their passion and naivete and exploration and novelty, and it’s just very creative.”
Chagas arrived at CMU in 2019 after a long career in engineering and is now an integral part of MCS.
“Engineers and mathematicians get along great,” Chagas said. “It’s the lingua franca of rationality.”
“Nuno has an uncanny ability to feel pulse of the department on many matters, not just IT related, likely because he serves all members of the department and many in the college. I am truly grateful for all the support and advice he provides,” said Prasad Tetali.
■ Kirsten Heuring
