Dude. You take money from Google. Really? All the people ranting about AI, but taking pay checks from Facebook, Amazon, Google, Microsoft, ... Hypocrisy much?

I for once enjoy that so much money is pumped into the automation of interactive theorem proving. Didn't think that anyone would build whole data centers for this! ;-)