$20 Million Donation for Philosopher-Led Center for Formal Mathematics at CMU


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.

guest
11 Comments
Oldest
Newest Most Voted
Inline Feedbacks
View all comments
Richard Russell Wood
23 days ago

CMU is to be congratulated for this. Speaking as an interested outside observer, who will be using “formalized” languages and methods in mathematical praxis?

Professional mathematicians? Or a separate class of knowledge worker and pedagogues who “formalize” proofs and maintains the library (-ies)? Or did I just miss the entire point and reason for this project?

Sounds like “a chore”. Good luck with the fun part.Report

Crypto
Crypto
Reply to  Richard Russell Wood
23 days ago

A large part of the reason for the project from one side is almost certainly to legitimate Cardano as a project by connecting it with CMU, and thus raise the price of the ADA token, enriching the holders of ADA. Hoskinson and his company own about 6% of the ADA.

It will be interesting to see whether Professor Avigad ends up saying nice things about ADA, and in what other ways Hoskinson tries to leverage this relationship.Report

Matthew Capps
Reply to  Crypto
23 days ago

I work for Input Output (Charles’ company) and was philosophy undergrad, so I’d like to address this aspersion.

Cardano already has legitimacy through 117 pieces academic research by Input Output. The majority of them are published in peer-reviewed academic journals: Financial Cryptography and ISOLA are frequent venues.

Also through Input Output, Cardano has connections with research labs and individual researchers at Edinburgh U, U Athens, Oxford U, U Wyoming, as well as many others.

Input Output is a R&D company focusing on blockchain and specializing in (you guessed it) formal methods. So my guess is that our researchers are also hoping to collaborate with researchers at the center.

But take the counterfactual, that this is all a ploy to boost the price of Ada (Cardano’s currency). Surely $20m from Charles’ personal fortune just to further ‘legitimize’ Ada gives diminishing returns at this point?

Honestly, I think Cardano has more legitimacy in Academia than in the crypto industry precisely because its core developers have followed the standards of rigorous academic research, and insist on using purely functional languages like Haskell to write the codebase.

PS– it’s ‘Ada’ like ‘Ada Lovelace,’ the computer scientist the currency is named for. Lovelace is to Ada as pennies are to dollars a sub-denomination.Report

Last edited 23 days ago by Matthew Capps
Crypto
Crypto
Reply to  Matthew Capps
23 days ago

Cardano has 2.5 billion ADA. If this Center causes ADA to go up $0.01, that’s $25 million.

Hoskinson left Ethereum because Buterin wanted to go the non-profit route and Hoskinson wanted to make money.

There may well be other reasons, but this is sure to be one of them.Report

Matthew Capps
Reply to  Crypto
23 days ago

The price of Ada fluctuates by at least several percent every day, like the price of all crypto tokens apart from stablecoins.

In the past year, Ada has increased in value from $0.02 to $2.30 (though it has fluctuated between $2.90 and $2 just this month).

I just don’t think this argument holds water.

PS– Apologies, but one other correction: Cardano is the blockchain for which Ada is a native currency. In the sense that Cardano has Ada it has 45b, which is the supply limit. I think you mean Input Output.Report

Matthew Capps
Reply to  Crypto
23 days ago

I offered something of a rebuttal earlier, but I also realize that unless you understand blockchain and cryptocurrency theoretically, it is difficult for to imagine that anything but token price could be important to people in the field.

I think that understanding these technologies involves a philosophical shift our concept of humans, and a revolution in politics and economics (not right/left valenced).

People who see these technologies with that lens get peeved when others confidently declare that we are ‘almost certainly’ out to make a quick buck.Report

Last edited 23 days ago by Matthew Capps
Andrew M. Bailey
Reply to  Matthew Capps
20 days ago

I’m a philosopher who specialises in this field. I understand cryptocurrencies and blockchains both practically and theoretically; I use this stuff every day and publish on it too. And I don’t think Crypto is wrong here. Because there is so much money to be made in selling crypto tokens, many of which have no real use, nearly everything in the space rightly falls under suspicion.

The most obvious way to dispel that suspicion is not selling something — no ICO, pre-mine, or pre-sale, in other words. Because Cardano does not meet that condition (there was an ICO netting hundreds of millions of dollars), its proponents face an uphill battle.Report

Matthew Capps
Reply to  Andrew M. Bailey
19 days ago

Hi Andrew! I’m familiar with you through Twitter, though I haven’t engaged with any of your work yet. I am really glad, however, that Resistance Money is doing this work, and I hope you’ll publish a guest piece here at Daily Nous.

To your comment… if I was in danger of throwing the baby out with the bath water, you are in danger of drowning it. Hopefully you see the conceptual inversion through the rhetorical flourish 🙂

To substantiate…

“A large part of the reason for the project from one side is almost certainly to legitimate Cardano as a project by connecting it with CMU and thus raise the price of the ADA token, enriching the holders of ADA.

It will be interesting to see whether Professor Avigad ends up saying nice things about ADA, and in what other ways Hoskinson tries to leverage this relationship.”

  1. Crypto is claiming near certainty that a large part of the reason for funding the center is to enrich holders of Ada (stakeholders in the Cardano blockchain).
  2. He is implying that Cardano is not legitimate as a project in some sphere in which it could be legitimated if only it was connected with CMU in this way.
  3. And he suggests it is probable (enough to be an interesting item of attention) this relationship will corrupt CMU to the purpose of legitimating Cardano for the enrichment of Ada holders (like Charles, and to a far lesser extent, like myself).

There is something Crypto is not wrong about here: we should be attuned to probabilities of profitable deception such that we respond with appropriate caution when such probabilities become apparent. What makes caution appropriate? Proportion to the evidence of risk for us in a given story (weighted differently by the seriousness of the risk).

So, here’s the story: a newly wealthy and famous man– wealthy and famous through stake in a volatile and widely mistrusted asset– invests a portion of his new power into a prestigious, conservative, and widely trusted institution. He is allowed to do so on the overt proposition that his interests are aligned with this institution (and us, as devotees of the discipline it extends).

Given what some experience of humans provides us, that story in the abstract has some probability of indicating a profitable deception on Charles’ part. Hence, we should take caution.

That’s the baby.

But to drain the bath water: the story is not that abstract.

Take it point by point…

#1
I don’t know how Crypto comes by his near certainty, except perhaps through a familiarity with crypto (the industry/culture) and– I would guess– ignorance of Cardano. There is strong evidence for primarily non-financial reasons that Charles– and less importantly, the Cardano project and its stakeholders– would benefit from the Center.

Two of the biggest lane of IOHK’s research and innovation, the special basis of its wealth, is formal methods programming in open-source software. Formal methods programming in open-source software is also the essential medium of the Center’s research (check this by reading the press release).

But this isn’t a strategic investment by Input Output. It’s a personal donation by Charles himself. who is mathematician of graduate-level training, interested in the philosophy of mathematics.

#2
I can specify (and have above specified) the abstract story given in the headline by telling you that the Cardano ecosystem, IOHK, and Charles already have a deep relationship with academia, proved out through the same mechanisms of trust that academics rely on: peer review, professional reputation, reproducibility, and scholarly impact, etc… It already has these connections in the highest degree– researchers from Oxford, Labs at Edinburgh, Athens, and Wyoming, tens of papers in Financial Cryptography and ISOLA.

Long before this center was created, Cardano was lambasted in the crypto industry (amongst the worshipers of ‘disruption’) for its strong ties to the academic world… for being institutionally legitimated.

#3
So, in fact, Cardano’s ecosystem has little to gain in legitimacy from further work with academia, but much to lose if it damages that reputation by corrupting academia.

Beyond that, I think Crypto is also wrong to sow mistrust about a community, a project, and an individual person who Crypto is evidently ignorant of.

There is a distinction, e.g. between on the one hand warning a female student that it’s risky to leave her drink alone with strangers at a bar, and on the other hand telling her such and such a fellow in particular almost certainly wants to roofie her.

(I’m using that example to make the distinction vivid, exaggerating the degree to make the kind clear).

So, if we do away with the bath water, I’m happy to keep the baby. 🙂

—–

Ah, and on your point about Cardano having an initial sale, you are certainly right. Having utilization-based or maintenance-based distribution & funding (as with bitcoin) is symbolically, and in more cases than not, substantially more pure than non-intrinsic distribution & funding mechanisms, like presales.

However, this is a whole ‘nother conversation 🙂Report

Last edited 19 days ago by Matthew Capps
Matthew Capps
Reply to  Andrew M. Bailey
19 days ago

Additionally Andrew, I’ll one up your audacity by asking, with socratic demur, whether you really understand cryptocurrencies and blockchains. If you do, you will have to explain them to me sometime 😉Report

Last edited 19 days ago by Matthew Capps
David Wallace
Reply to  Richard Russell Wood
23 days ago

As I understand these projects, the idea is to have a manageable enough formal system that mathematicians can use it directly in writing up their work (and then the journal can check the correctness of the work automatically).
Way back when, that was what Frege invented the Begriffschrift for, but it was way too clunky and unreadable. The hope is that a combination of computer assistance and radically better languages actually achieves Frege’s dream (and in doing so ameliorates an increasingly serious problem in modern mathematics whereby specialization is making it hard to reliably check results and rely on them).Report

Richard Russell Wood
Reply to  David Wallace
23 days ago

Ambitious.

As I said, Good luck.Report