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 https://github.com/eulerthedestroyer/proofs-from-the-book/blob/master/chapters/chapter_1.lean
The mathematician Paul Erdős said "The Book" is where God keeps the most elegant proof of each mathematical theorem.
Lean is a formal theorem prover that checks that all proofs are logically consistent