Proofs From the Book

Formally Verifying the most elegant proofs
Proofs From the Book
By Atticus Kuhn
Published 1/22/2021
Tags: proof, type theory, lean, proving

About

I am writing up all proofs given in the textbook "proofs from THE BOOK" by Aigner and Ziegler in the proof assistant Lean to check if the proofs are logically correct. If you want to see my current progress, go to chapter 1

Proofs From the Book

The mathematician Paul Erdős said "The Book" is where God keeps the most elegant proof of each mathematical theorem.

Lean

Lean is a formal theorem prover that checks that all proofs are logically consistent