Jeremy Avigad, professor of philosophy and mathematics at Carnegie Mellon University (CMU), will be leading the new Charles C. Hoskinson Center for Formal Mathematics, funded by a $20 million donation from entrepreneur Charles C. Hoskinson.
Jeremy Avigad and Charles Hoskinson
An announcement from CMU describes the work that will be conducted at the center:
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 [software that automates parts of the mathematical process and facilitates the development and checking of mathematical proofs]) 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.
Hoskinson, according to the announcement, “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.”
Professor Avigad specializes in mathematical logic, proof theory, philosophy of mathematics, formal verification, automated reasoning, and the history of mathematics. Of software like Lean he says, “Computational proof assistants based on formal mathematics are a transformative technology. 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.”
Here’s a video of Professor Avigad speaking at the opening of the center:
Further information here.
"center" - Google News
September 23, 2021 at 07:13PM
https://ift.tt/3lOBX7i
$20 Million Donation for Philosopher-Led Center for Formal Mathematics at CMU - Daily Nous
"center" - Google News
https://ift.tt/3bUHym8
https://ift.tt/2zR6ugj
Bagikan Berita Ini
0 Response to "$20 Million Donation for Philosopher-Led Center for Formal Mathematics at CMU - Daily Nous"
Post a Comment