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.  The book was published in 2006, and made an impression on me then.  The provers we have discussed so far all have a solution in the book, except for Lean, which was created after that year.  Happily, you can find a PDF of the book here, on Wiedijk's web site.