Formal proofs from THE BOOK Blog

I’m happy to announce that I’ll be working with Christoph Spiegel on a blog about implementing beautiful proofs, in the sense of “Formal proofs from THE BOOK”, in Lean 4. The blog is availble here.

I implemented a few chapters of the latter source in the context of a Master thesis at FU Berlin, in Lean 3. You can check out the corresponding repository, though most of it’s content will be ported to Lean 4, polished and improved, and also documented in more detail on the blog.

It’ll be great!