Stream: Miscellaneous

Topic: 20M USD for Lean and Mathlib


view this post on Zulip Karl Palmskog (Sep 22 2021 at 21:54):

https://www.cmu.edu/news/stories/archives/2021/september/hoskinson-center-for-formal-mathematics.html

Now we can only hope some other crypto millionaire will step up and do the same for CS/software/hardware formalization (and Coq)...

view this post on Zulip Karl Palmskog (Sep 23 2021 at 07:55):

unfortunately, formalized can nowadays mean everything from "we used some mathy symbols" to "we did checking down to PNP transistor axioms using a self-verified tool".

Advice to potential billionaire benefactors: use machine checked in your center name, e.g., "The I. M. Rich Center for Machine Checked Proofs"

view this post on Zulip Karl Palmskog (Oct 06 2021 at 15:15):

I guess this settles the question of spillovers:

The center's mission is to support the work being done by the Lean community, to promote the use of Lean and its libraries


Last updated: Aug 19 2022 at 21:02 UTC