Now we can only hope some other crypto millionaire will step up and do the same for CS/software/hardware formalization (and Coq)...
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"
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