Comment by krick

Thanks. It appears, however, that Dyson considers the whole approach a failure (referring to Gödel as a demolisher of it). So while he is saying it about a book, ironically, it seems hardly applicable in this context anymore. Because with this reasoning, any program in Lean (and the Lean programming language itself) should be seen as "a monumental failure".