Just got this from the library, it's a real page turner. Heard about it in this excellent interview: https://www.typetheoryforall.com/episodes/goedel-s-incomplet...