BROADCASTS.com

b'

I discuss a book edited by Freek Wiedijk (pronounced "Frake Weedike"), which describes the solutions he received in response to a call for formalized proofs of the irrationality of the square root of 2.\\xa0 The book was published in 2006, and made an impression on me then.\\xa0 The provers we have discussed so far all have a solution in the book, except for Lean, which was created after that year.\\xa0 Happily, you can find a PDF of the book here, on Wiedijk's web site.