Formalizing Geometric Proof Schwabhäuser 4.6 in the Metamath Proof Explorer (using mmj2)
Channel: David A. Wheeler
Date: 2020-07-19

This presentation demonstrates how to formalize a specific geometry proof in the Metamath Proof Explorer (MPE). The proof is from the book Metamathematische Methoden in der Geometrie by Wolfram Schwabhäuser, Wanda Szmielew, and Alfred Tarski, 1983, specifically theorem 4.6. This MPE proof was originally formalized by Thierry Arnoux in MPE theorem tgbtwnxfr. We recreate this formalization using the mmj2 tool as a demonstration of how to create geometry-based proofs in MPE. This video is released under the Creative Commons Attribution (CC-BY) license version 3.0 or later.