Thanks for sharing that, that sounds like an interesting plan.

A while ago I was trying to think about potential ways to have large impact via formal verification (after reading this post). I didn’t give it much attention, but it looks like others and I don’t see a case for this career path to be highly impactful, but I’d to love be proven wrong. I would appreciate it if you could elaborate on your perspective on this. I should probably mention that I couldn’t find a reference to formal verification at agent foundations (but I didn’t really read it), and Vanessa seemed to reference it as a tangential point, but I might be wrong about both.

I’m interested in formal verification from a purely mathematical point of view. That is, I think it’s important for math (but I don’t think that formalizing [mainstream] math is likely to be very impactful outside of math). Additionally, I am interested in ideas developed in homotopy type theory, because of their connections to homotopy theory, rather than because I think it is impactful.

Thanks for cross-posting this, I probably wouldn’t hear about this otherwise.

I am very interested in Open Phil’s model regarding the best time to donate for such causes. If anyone is aware of similar models for large donors, I would love to hear about them.