Karl Palmskog (Sep 22 2021 at 21:54): Karl Palmskog (Sep 22 2021 at 21:54):Now we can only hope some other crypto millionaire will step up and do the same for CS/software/hardware formalization (and Coq)...
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"
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: Jun 10 2023 at 06:31 UTC